tools/memory-model: Add types to litmus tests
[linux-2.6-microblaze.git] / tools / memory-model / litmus-tests / SB+poonceonces.litmus
1 C SB+poonceonces
2
3 (*
4  * Result: Sometimes
5  *
6  * This litmus test demonstrates that at least some ordering is required
7  * to order the store-buffering pattern, where each process writes to the
8  * variable that the preceding process reads.
9  *)
10
11 {
12         int x;
13         int y;
14 }
15
16 P0(int *x, int *y)
17 {
18         int r0;
19
20         WRITE_ONCE(*x, 1);
21         r0 = READ_ONCE(*y);
22 }
23
24 P1(int *x, int *y)
25 {
26         int r0;
27
28         WRITE_ONCE(*y, 1);
29         r0 = READ_ONCE(*x);
30 }
31
32 exists (0:r0=0 /\ 1:r0=0)