xref: /linux/tools/memory-model/litmus-tests/ISA2+pooncelock+pooncelock+pombonce.litmus (revision d0034a7a4ac7fae708146ac0059b9c47a1543f0d)
1acb6c96cSPaul E. McKenneyC ISA2+pooncelock+pooncelock+pombonce
2556bb7d2SAlan Stern
3556bb7d2SAlan Stern(*
46e89e831SAlan Stern * Result: Never
5556bb7d2SAlan Stern *
66e89e831SAlan Stern * This test shows that write-write ordering provided by locks
76e89e831SAlan Stern * (in P0() and P1()) is visible to external process P2().
8556bb7d2SAlan Stern *)
9556bb7d2SAlan Stern
10*5c587f9bSAkira Yokosawa{}
11556bb7d2SAlan Stern
12556bb7d2SAlan SternP0(int *x, int *y, spinlock_t *mylock)
13556bb7d2SAlan Stern{
14556bb7d2SAlan Stern	spin_lock(mylock);
15556bb7d2SAlan Stern	WRITE_ONCE(*x, 1);
16556bb7d2SAlan Stern	WRITE_ONCE(*y, 1);
17556bb7d2SAlan Stern	spin_unlock(mylock);
18556bb7d2SAlan Stern}
19556bb7d2SAlan Stern
20556bb7d2SAlan SternP1(int *y, int *z, spinlock_t *mylock)
21556bb7d2SAlan Stern{
22556bb7d2SAlan Stern	int r0;
23556bb7d2SAlan Stern
24556bb7d2SAlan Stern	spin_lock(mylock);
25556bb7d2SAlan Stern	r0 = READ_ONCE(*y);
26556bb7d2SAlan Stern	WRITE_ONCE(*z, 1);
27556bb7d2SAlan Stern	spin_unlock(mylock);
28556bb7d2SAlan Stern}
29556bb7d2SAlan Stern
30556bb7d2SAlan SternP2(int *x, int *z)
31556bb7d2SAlan Stern{
32556bb7d2SAlan Stern	int r1;
33556bb7d2SAlan Stern	int r2;
34556bb7d2SAlan Stern
35556bb7d2SAlan Stern	r2 = READ_ONCE(*z);
36556bb7d2SAlan Stern	smp_mb();
37556bb7d2SAlan Stern	r1 = READ_ONCE(*x);
38556bb7d2SAlan Stern}
39556bb7d2SAlan Stern
40556bb7d2SAlan Sternexists (1:r0=1 /\ 2:r2=1 /\ 2:r1=0)
41