Commit | Line | Data |
---|---|---|
1c27b644 PM |
1 | C ISA2+poonceonces |
2 | ||
8f32543b PM |
3 | (* |
4 | * Result: Sometimes | |
5 | * | |
6 | * Given a release-acquire chain ordering the first process's store | |
7 | * against the last process's load, is ordering preserved if all of the | |
8 | * smp_store_release() invocations are replaced by WRITE_ONCE() and all | |
9 | * of the smp_load_acquire() invocations are replaced by READ_ONCE()? | |
10 | *) | |
11 | ||
5c587f9b | 12 | {} |
1c27b644 PM |
13 | |
14 | P0(int *x, int *y) | |
15 | { | |
16 | WRITE_ONCE(*x, 1); | |
17 | WRITE_ONCE(*y, 1); | |
18 | } | |
19 | ||
20 | P1(int *y, int *z) | |
21 | { | |
22 | int r0; | |
23 | ||
24 | r0 = READ_ONCE(*y); | |
25 | WRITE_ONCE(*z, 1); | |
26 | } | |
27 | ||
28 | P2(int *x, int *z) | |
29 | { | |
30 | int r0; | |
31 | int r1; | |
32 | ||
33 | r0 = READ_ONCE(*z); | |
34 | r1 = READ_ONCE(*x); | |
35 | } | |
36 | ||
37 | exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) |