0001 C IRIW+poonceonces+OnceOnce
0002
0003 (*
0004 * Result: Sometimes
0005 *
0006 * Test of independent reads from independent writes with nothing
0007 * between each pairs of reads. In other words, is anything at all
0008 * needed to cause two different reading processes to agree on the order
0009 * of a pair of writes, where each write is to a different variable by a
0010 * different process?
0011 *)
0012
0013 {}
0014
0015 P0(int *x)
0016 {
0017 WRITE_ONCE(*x, 1);
0018 }
0019
0020 P1(int *x, int *y)
0021 {
0022 int r0;
0023 int r1;
0024
0025 r0 = READ_ONCE(*x);
0026 r1 = READ_ONCE(*y);
0027 }
0028
0029 P2(int *y)
0030 {
0031 WRITE_ONCE(*y, 1);
0032 }
0033
0034 P3(int *x, int *y)
0035 {
0036 int r0;
0037 int r1;
0038
0039 r0 = READ_ONCE(*y);
0040 r1 = READ_ONCE(*x);
0041 }
0042
0043 exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)
