0001 C SB+rfionceonce-poonceonces
0002
0003 (*
0004 * Result: Sometimes
0005 *
0006 * This litmus test demonstrates that LKMM is not fully multicopy atomic.
0007 *)
0008
0009 {}
0010
0011 P0(int *x, int *y)
0012 {
0013 int r1;
0014 int r2;
0015
0016 WRITE_ONCE(*x, 1);
0017 r1 = READ_ONCE(*x);
0018 r2 = READ_ONCE(*y);
0019 }
0020
0021 P1(int *x, int *y)
0022 {
0023 int r3;
0024 int r4;
0025
0026 WRITE_ONCE(*y, 1);
0027 r3 = READ_ONCE(*y);
0028 r4 = READ_ONCE(*x);
0029 }
0030
0031 locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *)
0032 exists (0:r2=0 /\ 1:r4=0)
