31 lines · plain
1C R+fencembonceonces2 3(*4 * Result: Never5 *6 * This is the fully ordered (via smp_mb()) version of one of the classic7 * counterintuitive litmus tests that illustrates the effects of store8 * propagation delays. Note that weakening either of the barriers would9 * cause the resulting test to be allowed.10 *)11 12{}13 14P0(int *x, int *y)15{16 WRITE_ONCE(*x, 1);17 smp_mb();18 WRITE_ONCE(*y, 1);19}20 21P1(int *x, int *y)22{23 int r0;24 25 WRITE_ONCE(*y, 2);26 smp_mb();27 r0 = READ_ONCE(*x);28}29 30exists (y=2 /\ 1:r0=0)31