42 lines · plain
1C RM-fixed2 3(*4 * Result: Never5 *6 * This litmus test demonstrates that the old "roach motel" approach7 * 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)42