summaryrefslogtreecommitdiff
path: root/Documentation/litmus-tests/locking/DCL-broken.litmus
blob: bfb7ba4316d6901a52cadb5e83cfbc44ba4974aa (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
C DCL-broken

(*
 * Result: Sometimes
 *
 * This litmus test demonstrates more than just locking is required to
 * correctly implement double-checked locking.
 *)

{
	int flag;
	int data;
}

P0(int *flag, int *data, spinlock_t *lck)
{
	int r0;
	int r1;
	int r2;

	r0 = READ_ONCE(*flag);
	if (r0 == 0) {
		spin_lock(lck);
		r1 = READ_ONCE(*flag);
		if (r1 == 0) {
			WRITE_ONCE(*data, 1);
			WRITE_ONCE(*flag, 1);
		}
		spin_unlock(lck);
	}
	r2 = READ_ONCE(*data);
}

P1(int *flag, int *data, spinlock_t *lck)
{
	int r0;
	int r1;
	int r2;

	r0 = READ_ONCE(*flag);
	if (r0 == 0) {
		spin_lock(lck);
		r1 = READ_ONCE(*flag);
		if (r1 == 0) {
			WRITE_ONCE(*data, 1);
			WRITE_ONCE(*flag, 1);
		}
		spin_unlock(lck);
	}
	r2 = READ_ONCE(*data);
}

locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)