| C LB+fencembonceonce+ctrlonceonce |
| |
| (* |
| * Result: Never |
| * |
| * This litmus test demonstrates that lightweight ordering suffices for |
| * the load-buffering pattern, in other words, preventing all processes |
| * reading from the preceding process's write. In this example, the |
| * combination of a control dependency and a full memory barrier are enough |
| * to do the trick. (But the full memory barrier could be replaced with |
| * another control dependency and order would still be maintained.) |
| *) |
| |
| {} |
| |
| P0(int *x, int *y) |
| { |
| int r0; |
| |
| r0 = READ_ONCE(*x); |
| if (r0) |
| WRITE_ONCE(*y, 1); |
| } |
| |
| P1(int *x, int *y) |
| { |
| int r0; |
| |
| r0 = READ_ONCE(*y); |
| smp_mb(); |
| WRITE_ONCE(*x, 1); |
| } |
| |
| exists (0:r0=1 /\ 1:r0=1) |
