30 lines · plain
1C SB+poonceonces2 3(*4 * Result: Sometimes5 *6 * This litmus test demonstrates that at least some ordering is required7 * to order the store-buffering pattern, where each process writes to the8 * variable that the preceding process reads.9 *)10 11{}12 13P0(int *x, int *y)14{15 int r0;16 17 WRITE_ONCE(*x, 1);18 r0 = READ_ONCE(*y);19}20 21P1(int *x, int *y)22{23 int r0;24 25 WRITE_ONCE(*y, 1);26 r0 = READ_ONCE(*x);27}28 29exists (0:r0=0 /\ 1:r0=0)30