1C S+fencewmbonceonce+poacquireonce
 2
 3(*
 4 * Result: Never
 5 *
 6 * Can a smp_wmb(), instead of a release, and an acquire order a prior
 7 * store against a subsequent store?
 8 *)
 9
10{}
11
12P0(int *x, int *y)
13{
14	WRITE_ONCE(*x, 2);
15	smp_wmb();
16	WRITE_ONCE(*y, 1);
17}
18
19P1(int *x, int *y)
20{
21	int r0;
22
23	r0 = smp_load_acquire(y);
24	WRITE_ONCE(*x, 1);
25}
26
27exists (x=2 /\ 1:r0=1)