tools/memory-model/litmus-tests/S+poonceonces.litmus

   1 C S+poonceonces
   2
   3 (*
   4  * Result: Sometimes
   5  *
   6  * Starting with a two-process release-acquire chain ordering P0()'s
   7  * first store against P1()'s final load, if the smp_store_release()
   8  * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
   9  * READ_ONCE(), is ordering preserved?
  10  *)
  11
  12 {}
  13
  14 P0(int *x, int *y)
  15 {
  16         WRITE_ONCE(*x, 2);
  17         WRITE_ONCE(*y, 1);
  18 }
  19
  20 P1(int *x, int *y)
  21 {
  22         int r0;
  23
  24         r0 = READ_ONCE(*y);
  25         WRITE_ONCE(*x, 1);
  26 }
  27
  28 exists (x=2 /\ 1:r0=1)