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