1C ISA2+poonceonces
2
3(*
4 * Result: Sometimes
5 *
6 * Given a release-acquire chain ordering the first process's store
7 * against the last process's load, is ordering preserved if all of the
8 * smp_store_release() invocations are replaced by WRITE_ONCE() and all
9 * of the smp_load_acquire() invocations are replaced by READ_ONCE()?
10 *)
11
12{
13	int x;
14	int y;
15	int z;
16}
17
18P0(int *x, int *y)
19{
20	WRITE_ONCE(*x, 1);
21	WRITE_ONCE(*y, 1);
22}
23
24P1(int *y, int *z)
25{
26	int r0;
27
28	r0 = READ_ONCE(*y);
29	WRITE_ONCE(*z, 1);
30}
31
32P2(int *x, int *z)
33{
34	int r0;
35	int r1;
36
37	r0 = READ_ONCE(*z);
38	r1 = READ_ONCE(*x);
39}
40
41exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
42