1C CoRR+poonceonce+Once
2
3(*
4 * Result: Never
5 *
6 * Test of read-read coherence, that is, whether or not two successive
7 * reads from the same variable are ordered.
8 *)
9
10{}
11
12P0(int *x)
13{
14	WRITE_ONCE(*x, 1);
15}
16
17P1(int *x)
18{
19	int r0;
20	int r1;
21
22	r0 = READ_ONCE(*x);
23	r1 = READ_ONCE(*x);
24}
25
26exists (1:r0=1 /\ 1:r1=0)
27