1*4882a593SmuzhiyunC ISA2+pooncerelease+poacquirerelease+poacquireonce
2*4882a593Smuzhiyun
3*4882a593Smuzhiyun(*
4*4882a593Smuzhiyun * Result: Never
5*4882a593Smuzhiyun *
6*4882a593Smuzhiyun * This litmus test demonstrates that a release-acquire chain suffices
7*4882a593Smuzhiyun * to order P0()'s initial write against P2()'s final read.  The reason
8*4882a593Smuzhiyun * that the release-acquire chain suffices is because in all but one
9*4882a593Smuzhiyun * case (P2() to P0()), each process reads from the preceding process's
10*4882a593Smuzhiyun * write.  In memory-model-speak, there is only one non-reads-from
11*4882a593Smuzhiyun * (AKA non-rf) link, so release-acquire is all that is needed.
12*4882a593Smuzhiyun *)
13*4882a593Smuzhiyun
14*4882a593Smuzhiyun{}
15*4882a593Smuzhiyun
16*4882a593SmuzhiyunP0(int *x, int *y)
17*4882a593Smuzhiyun{
18*4882a593Smuzhiyun	WRITE_ONCE(*x, 1);
19*4882a593Smuzhiyun	smp_store_release(y, 1);
20*4882a593Smuzhiyun}
21*4882a593Smuzhiyun
22*4882a593SmuzhiyunP1(int *y, int *z)
23*4882a593Smuzhiyun{
24*4882a593Smuzhiyun	int r0;
25*4882a593Smuzhiyun
26*4882a593Smuzhiyun	r0 = smp_load_acquire(y);
27*4882a593Smuzhiyun	smp_store_release(z, 1);
28*4882a593Smuzhiyun}
29*4882a593Smuzhiyun
30*4882a593SmuzhiyunP2(int *x, int *z)
31*4882a593Smuzhiyun{
32*4882a593Smuzhiyun	int r0;
33*4882a593Smuzhiyun	int r1;
34*4882a593Smuzhiyun
35*4882a593Smuzhiyun	r0 = smp_load_acquire(z);
36*4882a593Smuzhiyun	r1 = READ_ONCE(*x);
37*4882a593Smuzhiyun}
38*4882a593Smuzhiyun
39*4882a593Smuzhiyunexists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)
40