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 12P0(int *x, int *y) 13{ 14 int r0; 15 16 r0 = READ_ONCE(*x); 17 WRITE_ONCE(*y, 1); 18} 19 20P1(int *x, int *y) 21{ 22 int r0; 23 24 r0 = READ_ONCE(*y); 25 WRITE_ONCE(*x, 1); 26} 27 28exists (0:r0=1 /\ 1:r0=1) 29