Hi,
[...]
Placing a sync (i.e., the strongest Power barrier) accordingly would,
however,
still be insufficient for the second problem, as it would only fix the
reordering of read-read pairs by Worker 1 and the store atomicity issue from
Worker 0. But the writes on Worker 0 could still
Hi again,
[...]
However, your example is enough unlike the actual code that the
conclusion you state following the word clearly isn't actually clear
to me. According to latch.h, the correct method of using a latch is
like this:
* for (;;)
* {
* ResetLatch();
* if
of potential fixes!
Best,
Michael
(on behalf of the team: Jade Alglave, Daniel Kroening, Vincent Nimal, Michael
Tautschnig, as CC'ed)
pgpplvVgeFxPl.pgp
Description: PGP signature