tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus

   1 C WRC+poonceonces+Once
   2
   3 (*
   4  * Result: Sometimes
   5  *
   6  * This litmus test is an extension of the message-passing pattern,
   7  * where the first write is moved to a separate process.  Note that this
   8  * test has no ordering at all.
   9  *)
  10
  11 {}
  12
  13 P0(int *x)
  14 {
  15         WRITE_ONCE(*x, 1);
  16 }
  17
  18 P1(int *x, int *y)
  19 {
  20         int r0;
  21
  22         r0 = READ_ONCE(*x);
  23         WRITE_ONCE(*y, 1);
  24 }
  25
  26 P2(int *x, int *y)
  27 {
  28         int r0;
  29         int r1;
  30
  31         r0 = READ_ONCE(*y);
  32         r1 = READ_ONCE(*x);
  33 }
  34
  35 exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)