tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus

   1 C LB+fencembonceonce+ctrlonceonce
   2
   3 (*
   4  * Result: Never
   5  *
   6  * This litmus test demonstrates that lightweight ordering suffices for
   7  * the load-buffering pattern, in other words, preventing all processes
   8  * reading from the preceding process's write.  In this example, the
   9  * combination of a control dependency and a full memory barrier are enough
  10  * to do the trick.  (But the full memory barrier could be replaced with
  11  * another control dependency and order would still be maintained.)
  12  *)
  13
  14 {}
  15
  16 P0(int *x, int *y)
  17 {
  18         int r0;
  19
  20         r0 = READ_ONCE(*x);
  21         if (r0)
  22                 WRITE_ONCE(*y, 1);
  23 }
  24
  25 P1(int *x, int *y)
  26 {
  27         int r0;
  28
  29         r0 = READ_ONCE(*y);
  30         smp_mb();
  31         WRITE_ONCE(*x, 1);
  32 }
  33
  34 exists (0:r0=1 /\ 1:r0=1)