linux/tools/memory-model/litmus-tests/S+poonceonces.litmus
<<
>>
Prefs
   1C 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
  14P0(int *x, int *y)
  15{
  16        WRITE_ONCE(*x, 2);
  17        WRITE_ONCE(*y, 1);
  18}
  19
  20P1(int *x, int *y)
  21{
  22        int r0;
  23
  24        r0 = READ_ONCE(*y);
  25        WRITE_ONCE(*x, 1);
  26}
  27
  28exists (x=2 /\ 1:r0=1)
  29