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