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