xref: /OK3568_Linux_fs/kernel/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus (revision 4882a59341e53eb6f0b4789bf948001014eff981)
1*4882a593SmuzhiyunC IRIW+fencembonceonces+OnceOnce
2*4882a593Smuzhiyun
3*4882a593Smuzhiyun(*
4*4882a593Smuzhiyun * Result: Never
5*4882a593Smuzhiyun *
6*4882a593Smuzhiyun * Test of independent reads from independent writes with smp_mb()
7*4882a593Smuzhiyun * between each pairs of reads.  In other words, is smp_mb() sufficient to
8*4882a593Smuzhiyun * cause two different reading processes to agree on the order of a pair
9*4882a593Smuzhiyun * of writes, where each write is to a different variable by a different
10*4882a593Smuzhiyun * process?  This litmus test exercises LKMM's "propagation" rule.
11*4882a593Smuzhiyun *)
12*4882a593Smuzhiyun
13*4882a593Smuzhiyun{}
14*4882a593Smuzhiyun
15*4882a593SmuzhiyunP0(int *x)
16*4882a593Smuzhiyun{
17*4882a593Smuzhiyun	WRITE_ONCE(*x, 1);
18*4882a593Smuzhiyun}
19*4882a593Smuzhiyun
20*4882a593SmuzhiyunP1(int *x, int *y)
21*4882a593Smuzhiyun{
22*4882a593Smuzhiyun	int r0;
23*4882a593Smuzhiyun	int r1;
24*4882a593Smuzhiyun
25*4882a593Smuzhiyun	r0 = READ_ONCE(*x);
26*4882a593Smuzhiyun	smp_mb();
27*4882a593Smuzhiyun	r1 = READ_ONCE(*y);
28*4882a593Smuzhiyun}
29*4882a593Smuzhiyun
30*4882a593SmuzhiyunP2(int *y)
31*4882a593Smuzhiyun{
32*4882a593Smuzhiyun	WRITE_ONCE(*y, 1);
33*4882a593Smuzhiyun}
34*4882a593Smuzhiyun
35*4882a593SmuzhiyunP3(int *x, int *y)
36*4882a593Smuzhiyun{
37*4882a593Smuzhiyun	int r0;
38*4882a593Smuzhiyun	int r1;
39*4882a593Smuzhiyun
40*4882a593Smuzhiyun	r0 = READ_ONCE(*y);
41*4882a593Smuzhiyun	smp_mb();
42*4882a593Smuzhiyun	r1 = READ_ONCE(*x);
43*4882a593Smuzhiyun}
44*4882a593Smuzhiyun
45*4882a593Smuzhiyunexists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0)
46