tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus

   1 C 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
  15 P0(int *x)
  16 {
  17         WRITE_ONCE(*x, 1);
  18 }
  19
  20 P1(int *x, int *y)
  21 {
  22         int r0;
  23         int r1;
  24
  25         r0 = READ_ONCE(*x);
  26         r1 = READ_ONCE(*y);
  27 }
  28
  29 P2(int *y)
  30 {
  31         WRITE_ONCE(*y, 1);
  32 }
  33
  34 P3(int *x, int *y)
  35 {
  36         int r0;
  37         int r1;
  38
  39         r0 = READ_ONCE(*y);
  40         r1 = READ_ONCE(*x);
  41 }
  42
  43 exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)