1 C RM-fixed
2
3 (*
4 * Result: Never
5 *
6 * This litmus test demonstrates that the old "roach motel" approach
7 * to locking, where code can be freely moved into critical sections,
8 * cannot be used in the Linux kernel.
9 *)
10
11 {
12 int x;
13 atomic_t y;
14 }
15
16 P0(int *x, atomic_t *y, spinlock_t *lck)
17 {
18 int r2;
19
20 spin_lock(lck);
21 r2 = atomic_inc_return(y);
22 WRITE_ONCE(*x, 1);
23 spin_unlock(lck);
24 }
25
26 P1(int *x, atomic_t *y, spinlock_t *lck)
27 {
28 int r0;
29 int r1;
30 int r2;
31
32 r0 = READ_ONCE(*x);
33 r1 = READ_ONCE(*x);
34 spin_lock(lck);
35 r2 = atomic_inc_return(y);
36 spin_unlock(lck);
37 }
38
39 locations [x;0:r2;1:r0;1:r1;1:r2]
40 filter (1:r0=0 /\ 1:r1=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.