linux/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus
<<
>>
Prefs
   1C IRIW+poonceonces+OnceOnce
   2
   3(*
   4 * Result: Sometimes
   5 *
   6 * Test of independent reads from independent writes with nothing
   7 * between each pairs of reads.  In other words, is anything at all
   8 * needed to cause two different reading processes to agree on the order
   9 * of a pair of writes, where each write is to a different variable by a
  10 * different process?
  11 *)
  12
  13{}
  14
  15P0(int *x)
  16{
  17        WRITE_ONCE(*x, 1);
  18}
  19
  20P1(int *x, int *y)
  21{
  22        int r0;
  23        int r1;
  24
  25        r0 = READ_ONCE(*x);
  26        r1 = READ_ONCE(*y);
  27}
  28
  29P2(int *y)
  30{
  31        WRITE_ONCE(*y, 1);
  32}
  33
  34P3(int *x, int *y)
  35{
  36        int r0;
  37        int r1;
  38
  39        r0 = READ_ONCE(*y);
  40        r1 = READ_ONCE(*x);
  41}
  42
  43exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)
  44