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 11P0(int *x, int *y) 12{ 13 int r1; 14 int r2; 15 16 WRITE_ONCE(*x, 1); 17 r1 = READ_ONCE(*x); 18 r2 = READ_ONCE(*y); 19} 20 21P1(int *x, int *y) 22{ 23 int r3; 24 int r4; 25 26 WRITE_ONCE(*y, 1); 27 r3 = READ_ONCE(*y); 28 r4 = READ_ONCE(*x); 29} 30 31locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *) 32exists (0:r2=0 /\ 1:r4=0) 33