C C-W+WRC+o-rel+acq-o+o-mb-o.litmus { } P0(int *a, int *b) { WRITE_ONCE(*a, 1); smp_store_release(b, 1); } P1(int *b, int *c) { int r1; int r2; r1 = smp_load_acquire(b); r2 = READ_ONCE(*c); } P2(int *c, int *a) { int r3; WRITE_ONCE(*c, 1); smp_mb(); r3 = READ_ONCE(*a); } exists (1:r1=1 /\ 1:r2=0 /\ 2:r3=0)