tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus

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