38 lines · plain
1C ISA2+poonceonces2 3(*4 * Result: Sometimes5 *6 * Given a release-acquire chain ordering the first process's store7 * against the last process's load, is ordering preserved if all of the8 * smp_store_release() invocations are replaced by WRITE_ONCE() and all9 * of the smp_load_acquire() invocations are replaced by READ_ONCE()?10 *)11 12{}13 14P0(int *x, int *y)15{16 WRITE_ONCE(*x, 1);17 WRITE_ONCE(*y, 1);18}19 20P1(int *y, int *z)21{22 int r0;23 24 r0 = READ_ONCE(*y);25 WRITE_ONCE(*z, 1);26}27 28P2(int *x, int *z)29{30 int r0;31 int r1;32 33 r0 = READ_ONCE(*z);34 r1 = READ_ONCE(*x);35}36 37exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)38