Rev 1962 | Details | Compare with Previous | Last modification | View Log | RSS feed
Rev | Author | Line No. | Line |
---|---|---|---|
1 | jermar | 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. |