| 0,0 → 1,58 |
|---|
| 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. |