1C IRIW+poonceonces+OnceOnce 2 3(* 4 * Result: Sometimes 5 * 6 * Test of independent reads from independent writes with nothing 7 * between each pairs of reads. In other words, is anything at all 8 * needed to cause two different reading processes to agree on the order 9 * of a pair of writes, where each write is to a different variable by a 10 * 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