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