29 lines · plain
1C LB+poonceonces2 3(*4 * Result: Sometimes5 *6 * Can the counter-intuitive outcome for the load-buffering pattern7 * 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