1 C RM-broken 1 C RM-broken
2 2
3 (* 3 (*
4 * Result: DEADLOCK 4 * Result: DEADLOCK
5 * 5 *
6 * This litmus test demonstrates that the old 6 * This litmus test demonstrates that the old "roach motel" approach
7 * to locking, where code can be freely moved 7 * to locking, where code can be freely moved into critical sections,
8 * cannot be used in the Linux kernel. 8 * cannot be used in the Linux kernel.
9 *) 9 *)
10 10
11 { 11 {
12 int x; 12 int x;
13 atomic_t y; 13 atomic_t y;
14 } 14 }
15 15
16 P0(int *x, atomic_t *y, spinlock_t *lck) 16 P0(int *x, atomic_t *y, spinlock_t *lck)
17 { 17 {
18 int r2; 18 int r2;
19 19
20 spin_lock(lck); 20 spin_lock(lck);
21 r2 = atomic_inc_return(y); 21 r2 = atomic_inc_return(y);
22 WRITE_ONCE(*x, 1); 22 WRITE_ONCE(*x, 1);
23 spin_unlock(lck); 23 spin_unlock(lck);
24 } 24 }
25 25
26 P1(int *x, atomic_t *y, spinlock_t *lck) 26 P1(int *x, atomic_t *y, spinlock_t *lck)
27 { 27 {
28 int r0; 28 int r0;
29 int r1; 29 int r1;
30 int r2; 30 int r2;
31 31
32 spin_lock(lck); 32 spin_lock(lck);
33 r0 = READ_ONCE(*x); 33 r0 = READ_ONCE(*x);
34 r1 = READ_ONCE(*x); 34 r1 = READ_ONCE(*x);
35 r2 = atomic_inc_return(y); 35 r2 = atomic_inc_return(y);
36 spin_unlock(lck); 36 spin_unlock(lck);
37 } 37 }
38 38
39 locations [x;0:r2;1:r0;1:r1;1:r2] 39 locations [x;0:r2;1:r0;1:r1;1:r2]
40 filter (1:r0=0 /\ 1:r1=1) 40 filter (1:r0=0 /\ 1:r1=1)
41 exists (1:r2=1) 41 exists (1:r2=1)
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.