Merge tag 'block-5.9-2020-08-14' of git://git.kernel.dk/linux-block
[linux/fpc-iii.git] / tools / memory-model / litmus-tests / CoRW+poonceonce+Once.litmus
blob4635739f3974dd76925b2a20f874f03a2e55ce5f
1 C CoRW+poonceonce+Once
3 (*
4  * Result: Never
5  *
6  * Test of read-write coherence, that is, whether or not a read from
7  * a given variable and a later write to that same variable are ordered.
8  *)
12 P0(int *x)
14         int r0;
16         r0 = READ_ONCE(*x);
17         WRITE_ONCE(*x, 1);
20 P1(int *x)
22         WRITE_ONCE(*x, 2);
25 exists (x=2 /\ 0:r0=2)