source: mainline/doc/preemption@ 24bd23a

lfn serial ticket/834-toolchain-update topic/msim-upgrade topic/simplify-dev-export
Last change on this file since 24bd23a was f761f1eb, checked in by Jakub Jermar <jakub@…>, 20 years ago

Initial import

  • Property mode set to 100644
File size: 2.4 KB
Line 
1Kernel makes it possible for a thread to be preempted anytime when
2IRQ's are enabled on local CPU. This arrangement triggers a discussion
3about its correctness and efficiency.
4
5The correctness issue relates to the possibility of preempting a
6thread holding a spinlock. It is natural to ask whether such a
7preemption can lead to a deadlock. By proving the following lemma, we
8will show that deadlock is actually not possible.
9
10Lemma:
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
15Proof:
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
43Notes 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.
Note: See TracBrowser for help on using the repository browser.