1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar |
3 imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar |
4 begin |
4 begin |
5 ML {* |
5 ML {* |
|
6 open Printer; |
6 show_question_marks_default := false; |
7 show_question_marks_default := false; |
7 *} |
8 *} |
8 (*>*) |
9 (*>*) |
9 |
10 |
10 section {* Introduction *} |
11 section {* Introduction *} |
11 |
12 |
12 text {* |
13 text {* |
13 Many realtime systems need to support processes with priorities and |
14 Many real-time systems need to support processes with priorities and |
14 locking of resources. Locking of resources ensures mutual exclusion |
15 locking of resources. Locking of resources ensures mutual exclusion |
15 when accessing shared data or devices. Priorities allow scheduling |
16 when accessing shared data or devices. Priorities allow scheduling |
16 of processes that need to finish their work within hard deadlines. |
17 of processes that need to finish their work within deadlines. |
17 Unfortunately, both features can interact in subtle ways leading to |
18 Unfortunately, both features can interact in subtle ways leading to |
18 a problem, called \emph{Priority Inversion}. Suppose three processes |
19 a problem, called \emph{Priority Inversion}. Suppose three processes |
19 having priorities $H$(igh), $M$(edium) and $L$(ow). We would expect |
20 having priorities $H$(igh), $M$(edium) and $L$(ow). We would expect |
20 that the process $H$ blocks any other process with lower priority |
21 that the process $H$ blocks any other process with lower priority |
21 and itself cannot be blocked by a process with lower priority. Alas, |
22 and itself cannot be blocked by a process with lower priority. Alas, |
29 blocked by processes with lower priorities, the problem is called |
30 blocked by processes with lower priorities, the problem is called |
30 Priority Inversion. It was first described in |
31 Priority Inversion. It was first described in |
31 \cite{Lampson:Redell:cacm:1980} in the context of the Mesa |
32 \cite{Lampson:Redell:cacm:1980} in the context of the Mesa |
32 programming language designed for concurrent programming. |
33 programming language designed for concurrent programming. |
33 |
34 |
34 If the problem of Priority Inversion is ignored, realtime systems |
35 If the problem of Priority Inversion is ignored, real-time systems |
35 can become unpredictable and resulting bugs can be hard to diagnose. |
36 can become unpredictable and resulting bugs can be hard to diagnose. |
36 The classic example where this happened is the software that |
37 The classic example where this happened is the software that |
37 controlled the Mars Pathfinder mission in 1997 |
38 controlled the Mars Pathfinder mission in 1997 |
38 \cite{Reeves-Glenn-1998}. Once the spacecraft landed, the software |
39 \cite{Reeves-Glenn-1998}. Once the spacecraft landed, the software |
39 shut down at irregular intervals leading to loss of project time, as |
40 shut down at irregular intervals leading to loss of project time, as |
44 priority task locking a resource prevented a high priority process |
45 priority task locking a resource prevented a high priority process |
45 from running in time leading to a system reset. Once the problem was found, |
46 from running in time leading to a system reset. Once the problem was found, |
46 it was rectified by enabling the Priority Inheritance Protocol in |
47 it was rectified by enabling the Priority Inheritance Protocol in |
47 the scheduling software. |
48 the scheduling software. |
48 |
49 |
49 The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to |
50 The idea behind the \emph{Priority Inheritance Protocol} (PIP) |
50 let the process $L$ temporarily inherit the high priority from $H$ |
51 \cite{journals/tc/ShaRL90} is to let the process $L$ temporarily |
51 until $L$ releases the locked resource. This solves the problem of |
52 inherit the high priority from $H$ until $L$ releases the locked |
52 $H$ having to wait indefinitely, because $L$ cannot, for example, be blocked by |
53 resource. This solves the problem of $H$ having to wait |
53 processes having priority $M$. This solution to the Priority |
54 indefinitely, because $L$ cannot, for example, be blocked by |
54 Inversion problem has been known since \cite{Lampson:Redell:cacm:1980} |
55 processes having priority $M$. While a few other solutions to the Priority |
55 but Lui et al give the first thorough analysis and present a correctness |
56 Inversion problem exists \cite{Lampson:Redell:cacm:1980}, PIP is one |
56 proof for an algorithm \cite{journals/tc/ShaRL90}. |
57 that is widely adopted and implemented [???Book] (where implemented???). |
|
58 One advantage of PIP is that raising the priority of a process |
|
59 having a lock can be dynamically calculated. This is in contrast, |
|
60 for example, to Priority Ceiling which requires static analysis |
|
61 of the program in order to avoid Priority Inversion. |
|
62 |
|
63 However there has also been strong criticism against PIP |
|
64 |
|
65 Priority Inversion problem has been known since 1980 |
|
66 \cite{Lampson:Redell:cacm:1980}, but Sha et al.~give the first |
|
67 thorough analysis and present an informal correctness proof for PIP |
|
68 .\footnote{Sha et al.~call it the |
|
69 \emph{Basic Priority Inheritance Protocol}.} |
57 |
70 |
58 However, there are further subtleties: just lowering the priority |
71 However, there are further subtleties: just lowering the priority |
59 of the process $L$ to its low priority, as proposed in ???, is |
72 of the process $L$ to its low priority, as proposed in ???, is |
60 incorrect.\bigskip |
73 incorrect.\bigskip |
|
74 |
|
75 \begin{quote} |
|
76 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
|
77 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
|
78 \end{quote} |
|
79 |
|
80 book: page 135, sec 5.6.5 |
|
81 |
|
82 do you need axioms in the formalisation? |
61 |
83 |
62 \noindent |
84 \noindent |
63 Priority inversion referrers to the phenomena where tasks with higher |
85 Priority inversion referrers to the phenomena where tasks with higher |
64 priority are blocked by ones with lower priority. If priority inversion |
86 priority are blocked by ones with lower priority. If priority inversion |
65 is not controlled, there will be no guarantee the urgent tasks will be |
87 is not controlled, there will be no guarantee the urgent tasks will be |
106 of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} |
128 of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} |
107 discusses a series of basic properties of PI. Section \ref{extension} shows formally |
129 discusses a series of basic properties of PI. Section \ref{extension} shows formally |
108 how priority inversion is controlled by PI. Section \ref{implement} gives properties |
130 how priority inversion is controlled by PI. Section \ref{implement} gives properties |
109 which can be used for guidelines of implementation. Section \ref{related} discusses |
131 which can be used for guidelines of implementation. Section \ref{related} discusses |
110 related works. Section \ref{conclusion} concludes the whole paper. |
132 related works. Section \ref{conclusion} concludes the whole paper. |
|
133 |
|
134 The basic priority inheritance protocol has two problems: |
|
135 |
|
136 It does not prevent a deadlock from happening in a program with circular lock dependencies. |
|
137 |
|
138 A chain of blocking may be formed; blocking duration can be substantial, though bounded. |
111 |
139 |
112 |
140 |
113 Contributions |
141 Contributions |
114 |
142 |
115 Despite the wide use of Priority Inheritance Protocol in real time operating |
143 Despite the wide use of Priority Inheritance Protocol in real time operating |