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. |