Documentation/litmus-tests/locking/RM-fixed.litmus

   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)