LXR linux/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus

   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