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