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