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

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