1C DCL-fixed
2
3(*
4 * Result: Never
5 *
6 * This litmus test demonstrates that double-checked locking can be
7 * reliable given proper use of smp_load_acquire() and smp_store_release()
8 * in addition to the locking.
9 *)
10
11{
12	int flag;
13	int data;
14}
15
16P0(int *flag, int *data, spinlock_t *lck)
17{
18	int r0;
19	int r1;
20	int r2;
21
22	r0 = smp_load_acquire(flag);
23	if (r0 == 0) {
24		spin_lock(lck);
25		r1 = READ_ONCE(*flag);
26		if (r1 == 0) {
27			WRITE_ONCE(*data, 1);
28			smp_store_release(flag, 1);
29		}
30		spin_unlock(lck);
31	}
32	r2 = READ_ONCE(*data);
33}
34
35P1(int *flag, int *data, spinlock_t *lck)
36{
37	int r0;
38	int r1;
39	int r2;
40
41	r0 = smp_load_acquire(flag);
42	if (r0 == 0) {
43		spin_lock(lck);
44		r1 = READ_ONCE(*flag);
45		if (r1 == 0) {
46			WRITE_ONCE(*data, 1);
47			smp_store_release(flag, 1);
48		}
49		spin_unlock(lck);
50	}
51	r2 = READ_ONCE(*data);
52}
53
54locations [flag;data;0:r0;0:r1;1:r0;1:r1]
55exists (0:r2=0 \/ 1:r2=0)
56