1*4882a593SmuzhiyunC ISA2+pooncelock+pooncelock+pombonce
2*4882a593Smuzhiyun
3*4882a593Smuzhiyun(*
4*4882a593Smuzhiyun * Result: Never
5*4882a593Smuzhiyun *
6*4882a593Smuzhiyun * This test shows that write-write ordering provided by locks
7*4882a593Smuzhiyun * (in P0() and P1()) is visible to external process P2().
8*4882a593Smuzhiyun *)
9*4882a593Smuzhiyun
10*4882a593Smuzhiyun{}
11*4882a593Smuzhiyun
12*4882a593SmuzhiyunP0(int *x, int *y, spinlock_t *mylock)
13*4882a593Smuzhiyun{
14*4882a593Smuzhiyun	spin_lock(mylock);
15*4882a593Smuzhiyun	WRITE_ONCE(*x, 1);
16*4882a593Smuzhiyun	WRITE_ONCE(*y, 1);
17*4882a593Smuzhiyun	spin_unlock(mylock);
18*4882a593Smuzhiyun}
19*4882a593Smuzhiyun
20*4882a593SmuzhiyunP1(int *y, int *z, spinlock_t *mylock)
21*4882a593Smuzhiyun{
22*4882a593Smuzhiyun	int r0;
23*4882a593Smuzhiyun
24*4882a593Smuzhiyun	spin_lock(mylock);
25*4882a593Smuzhiyun	r0 = READ_ONCE(*y);
26*4882a593Smuzhiyun	WRITE_ONCE(*z, 1);
27*4882a593Smuzhiyun	spin_unlock(mylock);
28*4882a593Smuzhiyun}
29*4882a593Smuzhiyun
30*4882a593SmuzhiyunP2(int *x, int *z)
31*4882a593Smuzhiyun{
32*4882a593Smuzhiyun	int r1;
33*4882a593Smuzhiyun	int r2;
34*4882a593Smuzhiyun
35*4882a593Smuzhiyun	r2 = READ_ONCE(*z);
36*4882a593Smuzhiyun	smp_mb();
37*4882a593Smuzhiyun	r1 = READ_ONCE(*x);
38*4882a593Smuzhiyun}
39*4882a593Smuzhiyun
40*4882a593Smuzhiyunexists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
41