RM-fixed.litmus

 1C 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
16P0(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
26P1(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
39locations [x;0:r2;1:r0;1:r1;1:r2]
40filter (1:r0=0 /\ 1:r1=1)
41exists (1:r2=1)