C C-IRIW+rel+rel+acq-o+acq-o.litmus { } P0(int *x) { smp_store_release(x, 1); } P1(int *y) { smp_store_release(y, 1); } P2(int *x, int *y) { int r1; int r2; r1 = smp_load_acquire(x); r2 = READ_ONCE(*y); } P3(int *x, int *y) { int r1; int r2; r1 = smp_load_acquire(y); r2 = READ_ONCE(*x); } exists (2:r1=1 /\ 2:r2=0 /\ 3:r1=1 /\ 3:r2=0)