C WRC-release-acquire {} P0(int *x) { WRITE_ONCE(*x, 1); } P1(int *x, int *y, int *s) { int r0; int r1; r0 = READ_ONCE(*x); smp_store_release(s, 1); r1 = smp_load_acquire(s); WRITE_ONCE(*y, 1); } P2(int *x, int *y) { int r0; int r1; r0 = READ_ONCE(*y); smp_rmb(); r1 = READ_ONCE(*x); } Observed 2:r1=0; 2:r0=1; 1:r0=1;