1C SB+rfionceonce-poonceonces
2
3(*
4 * Result: Sometimes
5 *
6 * This litmus test demonstrates that LKMM is not fully multicopy atomic.
7 *)
8
9{
10	int x;
11	int y;
12}
13
14P0(int *x, int *y)
15{
16	int r1;
17	int r2;
18
19	WRITE_ONCE(*x, 1);
20	r1 = READ_ONCE(*x);
21	r2 = READ_ONCE(*y);
22}
23
24P1(int *x, int *y)
25{
26	int r3;
27	int r4;
28
29	WRITE_ONCE(*y, 1);
30	r3 = READ_ONCE(*y);
31	r4 = READ_ONCE(*x);
32}
33
34locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *)
35exists (0:r2=0 /\ 1:r4=0)
36