1 C DCL-fixed
2
3 (*
4 * Result: Never
5 *
6 * This litmus test demonstrates that double-c
7 * reliable given proper use of smp_load_acqui
8 * in addition to the locking.
9 *)
10
11 {
12 int flag;
13 int data;
14 }
15
16 P0(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
29 }
30 spin_unlock(lck);
31 }
32 r2 = READ_ONCE(*data);
33 }
34
35 P1(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
48 }
49 spin_unlock(lck);
50 }
51 r2 = READ_ONCE(*data);
52 }
53
54 locations [flag;data;0:r0;0:r1;1:r0;1:r1]
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.