C C-MP2+o-o-wmb-o-o+o-rmb-o+o-rmb-o.litmus { } P0(int *a, int *b, int *c, int *d) { WRITE_ONCE(*a, 1); WRITE_ONCE(*c, 1); smp_wmb(); WRITE_ONCE(*b, 1); WRITE_ONCE(*d, 1); } P1(int *a, int *b) { int r1; int r2; r1 = READ_ONCE(*b); smp_rmb(); r2 = READ_ONCE(*a); } P2(int *c, int *d) { int r1; int r2; r1 = READ_ONCE(*d); smp_rmb(); r2 = READ_ONCE(*c); } exists (1:r1=1 /\ 1:r2=0) \/ (2:r1=1 /\ 2:r2=0)