44 lines · plain
1C IRIW+poonceonces+OnceOnce2 3(*4 * Result: Sometimes5 *6 * Test of independent reads from independent writes with nothing7 * between each pairs of reads. In other words, is anything at all8 * needed to cause two different reading processes to agree on the order9 * of a pair of writes, where each write is to a different variable by a10 * different process?11 *)12 13{}14 15P0(int *x)16{17 WRITE_ONCE(*x, 1);18}19 20P1(int *x, int *y)21{22 int r0;23 int r1;24 25 r0 = READ_ONCE(*x);26 r1 = READ_ONCE(*y);27}28 29P2(int *y)30{31 WRITE_ONCE(*y, 1);32}33 34P3(int *x, int *y)35{36 int r0;37 int r1;38 39 r0 = READ_ONCE(*y);40 r1 = READ_ONCE(*x);41}42 43exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)44