C C-2+2W+o-wmb-o+o-wmb-o.litmus { } P0(int *a, int *b) { WRITE_ONCE(*a, 2); smp_wmb(); WRITE_ONCE(*b, 1); } P1(int *a, int *b) { WRITE_ONCE(*b, 2); smp_wmb(); WRITE_ONCE(*a, 1); } exists (b=2 /\ a=2)