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 int x; 15 int y; 16} 17 18P0(int *x) 19{ 20 WRITE_ONCE(*x, 1); 21} 22 23P1(int *x, int *y) 24{ 25 int r0; 26 int r1; 27 28 r0 = READ_ONCE(*x); 29 r1 = READ_ONCE(*y); 30} 31 32P2(int *y) 33{ 34 WRITE_ONCE(*y, 1); 35} 36 37P3(int *x, int *y) 38{ 39 int r0; 40 int r1; 41 42 r0 = READ_ONCE(*y); 43 r1 = READ_ONCE(*x); 44} 45 46exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0) 47