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         int x;
  14         int y;
  15 }
  16
  17 P0(int *x, int *y)
  18 {
  19         WRITE_ONCE(*x, 2);
  20         WRITE_ONCE(*y, 1);
  21 }
  22
  23 P1(int *x, int *y)
  24 {
  25         int r0;
  26
  27         r0 = READ_ONCE(*y);
  28         WRITE_ONCE(*x, 1);
  29 }
  30
  31 exists (x=2 /\ 1:r0=1)