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