tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus

   1 C SB+rfionceonce-poonceonces
   2
   3 (*
   4  * Result: Sometimes
   5  *
   6  * This litmus test demonstrates that LKMM is not fully multicopy atomic.
   7  *)
   8
   9 {
  10         int x;
  11         int y;
  12 }
  13
  14 P0(int *x, int *y)
  15 {
  16         int r1;
  17         int r2;
  18
  19         WRITE_ONCE(*x, 1);
  20         r1 = READ_ONCE(*x);
  21         r2 = READ_ONCE(*y);
  22 }
  23
  24 P1(int *x, int *y)
  25 {
  26         int r3;
  27         int r4;
  28
  29         WRITE_ONCE(*y, 1);
  30         r3 = READ_ONCE(*y);
  31         r4 = READ_ONCE(*x);
  32 }
  33
  34 locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *)
  35 exists (0:r2=0 /\ 1:r4=0)