Subversion Repositories HelenOS

Kernel makes it possible for a thread to be preempted anytime when
IRQ's are enabled on local CPU. This arrangement triggers a discussion
about its correctness and efficiency.

The correctness issue relates to the possibility of preempting a
thread holding a spinlock. It is natural to ask whether such a
preemption can lead to a deadlock. By proving the following lemma, we
will show that deadlock is actually not possible.

Lemma:
  On condition that each spinning lock is always locked on the same
  CPU priority level (either always with IRQ's disabled or always
  with IRQ's enabled), otherwise correct code never deadlocks.

Proof:
  Let all assumptions from the lemma hold.
  Let us further assume that we have encountered a deadlock.
  We will analyse all likely ways how that could have happened.

  a)  Deadlock happened between two CPUs. This means that there must
  have been wrong lock-ordering. Code with lock-ordering problems is
  considered incorrect and contradicts our assumptions.
  
  b)  Deadlock happened between two threads of execution executing on
  the same CPU. 

  b1) If one thread of execution was servicing an interrupt and the
  other was executing in thread context, our assumption that each
  spinning lock is acquired always on the same CPU priority level is
  violated.
  
  b2) The last likely scenario is that the deadlock happened between
  two threads executing on the same CPU with IRQ's enabled.  Again,
  this means that we were working with incorrect code because it
  contained wrong ordering of lock operations.
  
  Since there is no possibility left, except for trivial errors, we
  have shown that the deadlock contradicts with our assumptions and
  therefore is not possible.

  Q.E.D.
  
Notes on the proof:
  ad a)  Deadlock between two CPUs is independent on the preemption
         model. If we have this kind of deadlock, we would have had
     the same kind of deadlock on an ordinary SMP system with
     kernel preemption disabled.
     
     This preemption model makes UP behave more like SMP because
     it introduces some SMP specific specialities.

  ad b2) Notice that the scenario when thread A acquires lock X and
     gets preempted in favor of thread B which is trying to
     acquire lock X, doesn't deadlock the two threads. Of course,
     B won't be allowed to get X until A releases it, but that
     will certainly happen because B too will sooner or later be
     preempted. This scenario emphasizes the efficiency issues,
     though.