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         int x;
  16         int y;
  17 }
  18
  19 P0(int *x, int *y)
  20 {
  21         int r0;
  22
  23         r0 = READ_ONCE(*x);
  24         if (r0)
  25                 WRITE_ONCE(*y, 1);
  26 }
  27
  28 P1(int *x, int *y)
  29 {
  30         int r0;
  31
  32         r0 = READ_ONCE(*y);
  33         smp_mb();
  34         WRITE_ONCE(*x, 1);
  35 }
  36
  37 exists (0:r0=1 /\ 1:r0=1)