33 lines · plain
1C SB+rfionceonce-poonceonces2 3(*4 * Result: Sometimes5 *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