C C-MP+o-wmb-o+o-rmb-o.litmus { } P0(int *a, int *b) { WRITE_ONCE(*a, 1); smp_wmb(); WRITE_ONCE(*b, 1); } P1(int *a, int *b) { int r1; int r2; r1 = READ_ONCE(*b); smp_rmb(); r2 = READ_ONCE(*a); } exists (1:r1=1 /\ 1:r2=0)
C11 equivalent: c11-prop-src/C-MP+o-wmb-o+o-rmb-o.litmus