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