memory-model/litmus-tests/CoRR%2Bpoonceonce%2BOnce.litmus

0001 C CoRR+poonceonce+Once
0002
0003 (*
0004  * Result: Never
0005  *
0006  * Test of read-read coherence, that is, whether or not two successive
0007  * reads from the same variable are ordered.
0008  *)
0009
0010 {}
0011
0012 P0(int *x)
0013 {
0014         WRITE_ONCE(*x, 1);
0015 }
0016
0017 P1(int *x)
0018 {
0019         int r0;
0020         int r1;
0021
0022         r0 = READ_ONCE(*x);
0023         r1 = READ_ONCE(*x);
0024 }
0025
0026 exists (1:r0=1 /\ 1:r1=0)