On 14 August 2015 at 10:54, Andrey Semashev <andrey.semas...@gmail.com> wrote: > On 14.08.2015 11:51, Jonathan Wakely wrote: >> >> On 14 August 2015 at 01:37, Andrey Semashev wrote: >>> >>> 1. Is my test valid or is there a flaw that I'm missing? >> >> >> The cppmem tool at http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/ shows >> that there are consistent executions where (x==0 && y==0) is true. I >> used this code: >> >> int main() { >> atomic_int a = 0; >> atomic_int b = 0; >> int x, y; >> {{{ >> { >> a.store(1,mo_seq_cst); >> a.load(mo_relaxed); >> x = b.load(mo_relaxed); >> } >> ||| >> { >> b.store(1, mo_seq_cst); >> b.load(mo_relaxed); >> y = a.load(mo_relaxed); >> } >> }}} >> return 0; >> } > > > I'm not familiar with that tool and not sure how to interpret its output,
Then you should study it :-) > but I think it misses one point that is present in the original test and I > failed to mention. The Boost.Atomic test uses Boost.Thread barriers to > ensure that both threads have executed the store-load-load region before > checking for x and y. You can add int xx = x; int yy = y; just before the return from main(), which executes after joining both threads doing the store-load-load. You will still see that xx==0 && yy==0 is possible. > Otherwise I cannot see how (x==0 && y==0) could happen. The last load in > each thread is sequenced after the first seq_cst store and both stores are > ordered with respect to each other, so one of the threads should produce 1. The tool evaluates the possible executions according to a formal model of the C++ memory model, so is invaluable for answering questions like this. It shows that there is no sychronizes-with (shown as "sw") relationship between the seq_cst store and the relaxed load for each atomic object. There is a total order of sequentially consistent operations, but the loads are not sequentially consistent and do not synchronize with the stores.
