]>
Commit | Line | Data |
---|---|---|
71b7ff5e | 1 | C LB+fencembonceonce+ctrlonceonce |
1c27b644 | 2 | |
8f32543b PM |
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 | ||
1c27b644 PM |
14 | {} |
15 | ||
16 | P0(int *x, int *y) | |
17 | { | |
18 | int r0; | |
19 | ||
20 | r0 = READ_ONCE(*x); | |
21 | if (r0) | |
22 | WRITE_ONCE(*y, 1); | |
23 | } | |
24 | ||
25 | P1(int *x, int *y) | |
26 | { | |
27 | int r0; | |
28 | ||
29 | r0 = READ_ONCE(*y); | |
30 | smp_mb(); | |
31 | WRITE_ONCE(*x, 1); | |
32 | } | |
33 | ||
34 | exists (0:r0=1 /\ 1:r0=1) |