1 | Kernel makes it possible for a thread to be preempted anytime when
|
---|
2 | IRQ's are enabled on local CPU. This arrangement triggers a discussion
|
---|
3 | about its correctness and efficiency.
|
---|
4 |
|
---|
5 | The correctness issue relates to the possibility of preempting a
|
---|
6 | thread holding a spinlock. It is natural to ask whether such a
|
---|
7 | preemption can lead to a deadlock. By proving the following lemma, we
|
---|
8 | will show that deadlock is actually not possible.
|
---|
9 |
|
---|
10 | Lemma:
|
---|
11 | On condition that each spinning lock is always locked on the same
|
---|
12 | CPU priority level (either always with IRQ's disabled or always
|
---|
13 | with IRQ's enabled), otherwise correct code never deadlocks.
|
---|
14 |
|
---|
15 | Proof:
|
---|
16 | Let all assumptions from the lemma hold.
|
---|
17 | Let us further assume that we have encountered a deadlock.
|
---|
18 | We will analyse all likely ways how that could have happened.
|
---|
19 |
|
---|
20 | a) Deadlock happened between two CPUs. This means that there must
|
---|
21 | have been wrong lock-ordering. Code with lock-ordering problems is
|
---|
22 | considered incorrect and contradicts our assumptions.
|
---|
23 |
|
---|
24 | b) Deadlock happened between two threads of execution executing on
|
---|
25 | the same CPU.
|
---|
26 |
|
---|
27 | b1) If one thread of execution was servicing an interrupt and the
|
---|
28 | other was executing in thread context, our assumption that each
|
---|
29 | spinning lock is acquired always on the same CPU priority level is
|
---|
30 | violated.
|
---|
31 |
|
---|
32 | b2) The last likely scenario is that the deadlock happened between
|
---|
33 | two threads executing on the same CPU with IRQ's enabled. Again,
|
---|
34 | this means that we were working with incorrect code because it
|
---|
35 | contained wrong ordering of lock operations.
|
---|
36 |
|
---|
37 | Since there is no possibility left, except for trivial errors, we
|
---|
38 | have shown that the deadlock contradicts with our assumptions and
|
---|
39 | therefore is not possible.
|
---|
40 |
|
---|
41 | Q.E.D.
|
---|
42 |
|
---|
43 | Notes on the proof:
|
---|
44 | ad a) Deadlock between two CPUs is independent on the preemption
|
---|
45 | model. If we have this kind of deadlock, we would have had
|
---|
46 | the same kind of deadlock on an ordinary SMP system with
|
---|
47 | kernel preemption disabled.
|
---|
48 |
|
---|
49 | This preemption model makes UP behave more like SMP because
|
---|
50 | it introduces some SMP specific specialities.
|
---|
51 |
|
---|
52 | ad b2) Notice that the scenario when thread A acquires lock X and
|
---|
53 | gets preempted in favor of thread B which is trying to
|
---|
54 | acquire lock X, doesn't deadlock the two threads. Of course,
|
---|
55 | B won't be allowed to get X until A releases it, but that
|
---|
56 | will certainly happen because B too will sooner or later be
|
---|
57 | preempted. This scenario emphasizes the efficiency issues,
|
---|
58 | though.
|
---|