1C S+poonceonces
2
3(*
4 * Result: Sometimes
5 *
6 * Starting with a two-process release-acquire chain ordering P0()'s
7 * first store against P1()'s final load, if the smp_store_release()
8 * is replaced by WRITE_ONCE() and the smp_load_acquire() replaced by
9 * READ_ONCE(), is ordering preserved?
10 *)
11
12{
13	int x;
14	int y;
15}
16
17P0(int *x, int *y)
18{
19	WRITE_ONCE(*x, 2);
20	WRITE_ONCE(*y, 1);
21}
22
23P1(int *x, int *y)
24{
25	int r0;
26
27	r0 = READ_ONCE(*y);
28	WRITE_ONCE(*x, 1);
29}
30
31exists (x=2 /\ 1:r0=1)
32