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