1C LB+poonceonces
2
3(*
4 * Result: Sometimes
5 *
6 * Can the counter-intuitive outcome for the load-buffering pattern
7 * be prevented even with no explicit ordering?
8 *)
9
10{
11	int x;
12	int y;
13}
14
15P0(int *x, int *y)
16{
17	int r0;
18
19	r0 = READ_ONCE(*x);
20	WRITE_ONCE(*y, 1);
21}
22
23P1(int *x, int *y)
24{
25	int r0;
26
27	r0 = READ_ONCE(*y);
28	WRITE_ONCE(*x, 1);
29}
30
31exists (0:r0=1 /\ 1:r0=1)
32