Commit | Line | Data |
---|---|---|
1c27b644 PM |
1 | C WRC+poonceonces+Once |
2 | ||
8f32543b PM |
3 | (* |
4 | * Result: Sometimes | |
5 | * | |
6 | * This litmus test is an extension of the message-passing pattern, | |
7 | * where the first write is moved to a separate process. Note that this | |
8 | * test has no ordering at all. | |
9 | *) | |
10 | ||
5c587f9b | 11 | {} |
1c27b644 PM |
12 | |
13 | P0(int *x) | |
14 | { | |
15 | WRITE_ONCE(*x, 1); | |
16 | } | |
17 | ||
18 | P1(int *x, int *y) | |
19 | { | |
20 | int r0; | |
21 | ||
22 | r0 = READ_ONCE(*x); | |
23 | WRITE_ONCE(*y, 1); | |
24 | } | |
25 | ||
26 | P2(int *x, int *y) | |
27 | { | |
28 | int r0; | |
29 | int r1; | |
30 | ||
31 | r0 = READ_ONCE(*y); | |
32 | r1 = READ_ONCE(*x); | |
33 | } | |
34 | ||
35 | exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) |