0001 C SB+poonceonces
0002
0003 (*
0004 * Result: Sometimes
0005 *
0006 * This litmus test demonstrates that at least some ordering is required
0007 * to order the store-buffering pattern, where each process writes to the
0008 * variable that the preceding process reads.
0009 *)
0010
0011 {}
0012
0013 P0(int *x, int *y)
0014 {
0015 int r0;
0016
0017 WRITE_ONCE(*x, 1);
0018 r0 = READ_ONCE(*y);
0019 }
0020
0021 P1(int *x, int *y)
0022 {
0023 int r0;
0024
0025 WRITE_ONCE(*y, 1);
0026 r0 = READ_ONCE(*x);
0027 }
0028
0029 exists (0:r0=0 /\ 1:r0=0)
