linux/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
<<
>>
Prefs
   1C WRC+pooncerelease+fencermbonceonce+Once
   2
   3(*
   4 * Result: Never
   5 *
   6 * This litmus test is an extension of the message-passing pattern, where
   7 * the first write is moved to a separate process.  Because it features
   8 * a release and a read memory barrier, it should be forbidden.  More
   9 * specifically, this litmus test is forbidden because smp_store_release()
  10 * is A-cumulative in LKMM.
  11 *)
  12
  13{}
  14
  15P0(int *x)
  16{
  17        WRITE_ONCE(*x, 1);
  18}
  19
  20P1(int *x, int *y)
  21{
  22        int r0;
  23
  24        r0 = READ_ONCE(*x);
  25        smp_store_release(y, 1);
  26}
  27
  28P2(int *x, int *y)
  29{
  30        int r0;
  31        int r1;
  32
  33        r0 = READ_ONCE(*y);
  34        smp_rmb();
  35        r1 = READ_ONCE(*x);
  36}
  37
  38exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
  39