0001 C R+fencembonceonces
0002
0003 (*
0004 * Result: Never
0005 *
0006 * This is the fully ordered (via smp_mb()) version of one of the classic
0007 * counterintuitive litmus tests that illustrates the effects of store
0008 * propagation delays. Note that weakening either of the barriers would
0009 * cause the resulting test to be allowed.
0010 *)
0011
0012 {}
0013
0014 P0(int *x, int *y)
0015 {
0016 WRITE_ONCE(*x, 1);
0017 smp_mb();
0018 WRITE_ONCE(*y, 1);
0019 }
0020
0021 P1(int *x, int *y)
0022 {
0023 int r0;
0024
0025 WRITE_ONCE(*y, 2);
0026 smp_mb();
0027 r0 = READ_ONCE(*x);
0028 }
0029
0030 exists (y=2 /\ 1:r0=0)
