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