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