0001 C LB+fencembonceonce+ctrlonceonce
0002
0003 (*
0004 * Result: Never
0005 *
0006 * This litmus test demonstrates that lightweight ordering suffices for
0007 * the load-buffering pattern, in other words, preventing all processes
0008 * reading from the preceding process's write. In this example, the
0009 * combination of a control dependency and a full memory barrier are enough
0010 * to do the trick. (But the full memory barrier could be replaced with
0011 * another control dependency and order would still be maintained.)
0012 *)
0013
0014 {}
0015
0016 P0(int *x, int *y)
0017 {
0018 int r0;
0019
0020 r0 = READ_ONCE(*x);
0021 if (r0)
0022 WRITE_ONCE(*y, 1);
0023 }
0024
0025 P1(int *x, int *y)
0026 {
0027 int r0;
0028
0029 r0 = READ_ONCE(*y);
0030 smp_mb();
0031 WRITE_ONCE(*x, 1);
0032 }
0033
0034 exists (0:r0=1 /\ 1:r0=1)
