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
14P0(int *x, int *y)
15{
16	WRITE_ONCE(*x, 1);
17	WRITE_ONCE(*y, 1);
18}
19
20P1(int *y, int *z)
21{
22	int r0;
23
24	r0 = READ_ONCE(*y);
25	WRITE_ONCE(*z, 1);
26}
27
28P2(int *x, int *z)
29{
30	int r0;
31	int r1;
32
33	r0 = READ_ONCE(*z);
34	r1 = READ_ONCE(*x);
35}
36
37exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)