LB+fencembonceonce+ctrlonceonce.litmus (694B)
1C 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 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)