1 C DCL-broken
2
3 (*
4 * Result: Sometimes
5 *
6 * This litmus test demonstrates more than just locking is required to
7 * correctly implement double-checked locking.
8 *)
9
10 {
11 int flag;
12 int data;
13 }
14
15 P0(int *flag, int *data, spinlock_t *lck)
16 {
17 int r0;
18 int r1;
19 int r2;
20
21 r0 = READ_ONCE(*flag);
22 if (r0 == 0) {
23 spin_lock(lck);
24 r1 = READ_ONCE(*flag);
25 if (r1 == 0) {
26 WRITE_ONCE(*data, 1);
27 WRITE_ONCE(*flag, 1);
28 }
29 spin_unlock(lck);
30 }
31 r2 = READ_ONCE(*data);
32 }
33
34 P1(int *flag, int *data, spinlock_t *lck)
35 {
36 int r0;
37 int r1;
38 int r2;
39
40 r0 = READ_ONCE(*flag);
41 if (r0 == 0) {
42 spin_lock(lck);
43 r1 = READ_ONCE(*flag);
44 if (r1 == 0) {
45 WRITE_ONCE(*data, 1);
46 WRITE_ONCE(*flag, 1);
47 }
48 spin_unlock(lck);
49 }
50 r2 = READ_ONCE(*data);
51 }
52
53 locations [flag;data;0:r0;0:r1;1:r0;1:r1]
54 exists (0:r2=0 \/ 1:r2=0)
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.