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) 42