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)

 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)