4 begin |
4 begin |
5 ML {* |
5 ML {* |
6 open Printer; |
6 open Printer; |
7 show_question_marks_default := false; |
7 show_question_marks_default := false; |
8 *} |
8 *} |
|
9 |
|
10 notation (latex output) |
|
11 Cons ("_::_" [78,77] 73) and |
|
12 vt ("valid'_state") and |
|
13 runing ("running") and |
|
14 birthtime ("inception") and |
|
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
|
16 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") |
9 (*>*) |
17 (*>*) |
10 |
18 |
11 section {* Introduction *} |
19 section {* Introduction *} |
12 |
20 |
13 text {* |
21 text {* |
14 Many real-time systems need to support processes with priorities and |
22 Many real-time systems need to support threads involving priorities and |
15 locking of resources. Locking of resources ensures mutual exclusion |
23 locking of resources. Locking of resources ensures mutual exclusion |
16 when accessing shared data or devices that cannot be |
24 when accessing shared data or devices that cannot be |
17 preempted. Priorities allow scheduling of processes that need to |
25 preempted. Priorities allow scheduling of threads that need to |
18 finish their work within deadlines. Unfortunately, both features |
26 finish their work within deadlines. Unfortunately, both features |
19 can interact in subtle ways leading to a problem, called |
27 can interact in subtle ways leading to a problem, called |
20 \emph{Priority Inversion}. Suppose three processes having priorities |
28 \emph{Priority Inversion}. Suppose three threads having priorities |
21 $H$(igh), $M$(edium) and $L$(ow). We would expect that the process |
29 $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread |
22 $H$ blocks any other process with lower priority and itself cannot |
30 $H$ blocks any other thread with lower priority and itself cannot |
23 be blocked by any process with lower priority. Alas, in a naive |
31 be blocked by any thread with lower priority. Alas, in a naive |
24 implementation of resource looking and priorities this property can |
32 implementation of resource looking and priorities this property can |
25 be violated. Even worse, $H$ can be delayed indefinitely by |
33 be violated. Even worse, $H$ can be delayed indefinitely by |
26 processes with lower priorities. For this let $L$ be in the |
34 threads with lower priorities. For this let $L$ be in the |
27 possession of a lock for a resource that also $H$ needs. $H$ must |
35 possession of a lock for a resource that also $H$ needs. $H$ must |
28 therefore wait for $L$ to exit the critical section and release this |
36 therefore wait for $L$ to exit the critical section and release this |
29 lock. The problem is that $L$ might in turn be blocked by any |
37 lock. The problem is that $L$ might in turn be blocked by any |
30 process with priority $M$, and so $H$ sits there potentially waiting |
38 thread with priority $M$, and so $H$ sits there potentially waiting |
31 indefinitely. Since $H$ is blocked by processes with lower |
39 indefinitely. Since $H$ is blocked by threads with lower |
32 priorities, the problem is called Priority Inversion. It was first |
40 priorities, the problem is called Priority Inversion. It was first |
33 described in \cite{Lampson80} in the context of the |
41 described in \cite{Lampson80} in the context of the |
34 Mesa programming language designed for concurrent programming. |
42 Mesa programming language designed for concurrent programming. |
35 |
43 |
36 If the problem of Priority Inversion is ignored, real-time systems |
44 If the problem of Priority Inversion is ignored, real-time systems |
37 can become unpredictable and resulting bugs can be hard to diagnose. |
45 can become unpredictable and resulting bugs can be hard to diagnose. |
38 The classic example where this happened is the software that |
46 The classic example where this happened is the software that |
39 controlled the Mars Pathfinder mission in 1997 |
47 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. |
40 \cite{Reeves98}. Once the spacecraft landed, the software |
48 Once the spacecraft landed, the software shut down at irregular |
41 shut down at irregular intervals leading to loss of project time as |
49 intervals leading to loss of project time as normal operation of the |
42 normal operation of the craft could only resume the next day (the |
50 craft could only resume the next day (the mission and data already |
43 mission and data already collected were fortunately not lost, because |
51 collected were fortunately not lost, because of a clever system |
44 of a clever system design). The reason for the shutdowns was that |
52 design). The reason for the shutdowns was that the scheduling |
45 the scheduling software fell victim of Priority Inversion: a low |
53 software fell victim of Priority Inversion: a low priority thread |
46 priority task locking a resource prevented a high priority process |
54 locking a resource prevented a high priority thread from running in |
47 from running in time leading to a system reset. Once the problem was found, |
55 time leading to a system reset. Once the problem was found, it was |
48 it was rectified by enabling the \emph{Priority Inheritance Protocol} |
56 rectified by enabling the \emph{Priority Inheritance Protocol} (PIP) |
49 (PIP) \cite{Sha90}\footnote{Sha et al.~call it the |
57 \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority |
50 \emph{Basic Priority Inheritance Protocol} \cite{Sha90}.} in the scheduling software. |
58 Inheritance Protocol} \cite{Sha90} and others sometimes call it |
51 |
59 also \emph{Priority Boosting}.} in the scheduling software. |
52 The idea behind PIP is to let the process $L$ temporarily |
60 |
53 inherit the high priority from $H$ until $L$ leaves the critical |
61 The idea behind PIP is to let the thread $L$ temporarily inherit |
54 section by unlocking the resource. This solves the problem of $H$ |
62 the high priority from $H$ until $L$ leaves the critical section by |
55 having to wait indefinitely, because $L$ cannot be |
63 unlocking the resource. This solves the problem of $H$ having to |
56 blocked by processes having priority $M$. While a few other |
64 wait indefinitely, because $L$ cannot be blocked by threads having |
57 solutions exist for the Priority Inversion problem, PIP is one that is widely deployed |
65 priority $M$. While a few other solutions exist for the Priority |
58 and implemented. This includes VxWorks (a proprietary real-time OS |
66 Inversion problem, PIP is one that is widely deployed and |
59 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
67 implemented. This includes VxWorks (a proprietary real-time OS used |
60 Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard |
68 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's |
61 realised for example in libraries for FreeBSD, Solaris and Linux. |
69 ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for |
62 |
70 example in libraries for FreeBSD, Solaris and Linux. |
63 One advantage of PIP is that increasing the priority of a process |
71 |
|
72 One advantage of PIP is that increasing the priority of a thread |
64 can be dynamically calculated by the scheduler. This is in contrast |
73 can be dynamically calculated by the scheduler. This is in contrast |
65 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
74 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
66 solution to the Priority Inversion problem, which requires static |
75 solution to the Priority Inversion problem, which requires static |
67 analysis of the program in order to prevent Priority Inversion. However, there has |
76 analysis of the program in order to prevent Priority |
68 also been strong criticism against PIP. For instance, PIP cannot |
77 Inversion. However, there has also been strong criticism against |
69 prevent deadlocks when lock dependencies are circular, and also |
78 PIP. For instance, PIP cannot prevent deadlocks when lock |
70 blocking times can be substantial (more than just the duration of a |
79 dependencies are circular, and also blocking times can be |
71 critical section). Though, most criticism against PIP centres |
80 substantial (more than just the duration of a critical section). |
72 around unreliable implementations and PIP being too complicated and |
81 Though, most criticism against PIP centres around unreliable |
73 too inefficient. For example, Yodaiken writes in \cite{Yodaiken02}: |
82 implementations and PIP being too complicated and too inefficient. |
|
83 For example, Yodaiken writes in \cite{Yodaiken02}: |
74 |
84 |
75 \begin{quote} |
85 \begin{quote} |
76 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
86 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
77 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
87 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
78 \end{quote} |
88 \end{quote} |
104 \noindent |
114 \noindent |
105 The criticism by Yodaiken, Baker and others suggests to us to look |
115 The criticism by Yodaiken, Baker and others suggests to us to look |
106 again at PIP from a more abstract level (but still concrete enough |
116 again at PIP from a more abstract level (but still concrete enough |
107 to inform an implementation) and makes PIP an ideal candidate for a |
117 to inform an implementation) and makes PIP an ideal candidate for a |
108 formal verification. One reason, of course, is that the original |
118 formal verification. One reason, of course, is that the original |
109 presentation of PIP \cite{Sha90}, despite being informally |
119 presentation of PIP~\cite{Sha90}, despite being informally |
110 ``proved'' correct, is actually \emph{flawed}. |
120 ``proved'' correct, is actually \emph{flawed}. |
111 |
121 |
112 Yodaiken \cite{Yodaiken02} points to a subtlety that had been |
122 Yodaiken \cite{Yodaiken02} points to a subtlety that had been |
113 overlooked in the informal proof by Sha et al. They specify in |
123 overlooked in the informal proof by Sha et al. They specify in |
114 \cite{Sha90} that after the process (whose priority has been raised) |
124 \cite{Sha90} that after the thread (whose priority has been raised) |
115 completes its critical section and releases the lock, it ``returns |
125 completes its critical section and releases the lock, it ``returns |
116 to its original priority level.'' This leads them to believe that an |
126 to its original priority level.'' This leads them to believe that an |
117 implementation of PIP is ``rather straightforward'' \cite{Sha90}. |
127 implementation of PIP is ``rather straightforward''~\cite{Sha90}. |
118 Unfortunately, as Yodaiken pointed out, this behaviour is too |
128 Unfortunately, as Yodaiken points out, this behaviour is too |
119 simplistic. Consider the case where the low priority process $L$ |
129 simplistic. Consider the case where the low priority thread $L$ |
120 locks \emph{two} resources, and two high-priority processes $H$ and |
130 locks \emph{two} resources, and two high-priority threads $H$ and |
121 $H'$ each wait for one of them. If $L$ then releases one resource |
131 $H'$ each wait for one of them. If $L$ then releases one resource |
122 so that $H$, say, can proceed, then we still have Priority Inversion |
132 so that $H$, say, can proceed, then we still have Priority Inversion |
123 with $H'$ (which waits for the other resource). The correct |
133 with $H'$ (which waits for the other resource). The correct |
124 behaviour for $L$ is to revert to the highest remaining priority of |
134 behaviour for $L$ is to revert to the highest remaining priority of |
125 processes that it blocks. The advantage of a formalisation in a |
135 the threads that it blocks. The advantage of formalising the |
126 theorem prover for the correctness of a high-level specification of |
136 correctness of a high-level specification of PIP in a theorem prover |
127 PIP is that such issues clearly show up and cannot be overlooked as |
137 is that such issues clearly show up and cannot be overlooked as in |
128 in informal reasoning (since we have to analyse all possible program |
138 informal reasoning (since we have to analyse all possible behaviours |
129 behaviours, i.e.~\emph{traces}, that could possibly happen). |
139 of threads, i.e.~\emph{traces}, that could possibly happen). |
130 |
140 |
131 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
141 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
|
142 |
|
143 vt (valid trace) was introduced earlier, cite |
|
144 |
|
145 distributed PIP |
132 *} |
146 *} |
133 |
147 |
134 section {* Formal Model of the Priority Inheritance Protocol *} |
148 section {* Formal Model of the Priority Inheritance Protocol *} |
135 |
149 |
136 text {* |
150 text {* |
137 Our formal model of PIP is based on Paulson's inductive approach to protocol |
151 We follow the original work by Sha et al.~\cite{Sha90} by modelling |
138 verification \cite{Paulson98}, where the state of the system is modelled as a list of events |
152 first a classical single CPU system where only one \emph{thread} is |
139 that happened so far. \emph{Events} fall into four categories defined as the datatype |
153 active at any given moment. We shall discuss later how to lift this |
|
154 restriction. Our model of PIP is based on Paulson's inductive |
|
155 approach to protocol verification \cite{Paulson98}, where the |
|
156 \emph{state} of a system is given by a list of events that |
|
157 happened so far. \emph{Events} fall into four categories defined as |
|
158 the datatype |
140 |
159 |
141 \begin{isabelle}\ \ \ \ \ %%% |
160 \begin{isabelle}\ \ \ \ \ %%% |
142 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
161 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
143 \isacommand{datatype} event & @{text "="} & @{term "Create thread priority"}\\ |
162 \isacommand{datatype} event |
144 & @{text "|"} & @{term "Exit thread"}\\ |
163 & @{text "="} & @{term "Create thread priority"}\\ |
145 & @{text "|"} & @{term "P thread cs"} & {\rm Request of a resource} @{text "cs"} {\rm by} @{text "thread"}\\ |
164 & @{text "|"} & @{term "Exit thread"} \\ |
146 & @{text "|"} & @{term "V thread cs"} & {\rm Release of a resource} @{text "cs"} {\rm by} @{text "thread"} |
165 & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the proprity for} @{text thread}\\ |
|
166 & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\ |
|
167 & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"} |
|
168 \end{tabular}} |
|
169 \end{isabelle} |
|
170 |
|
171 \noindent |
|
172 whereby threads, priorities and (critical) resources are represented |
|
173 as natural numbers. As in Paulson's work, we need to define |
|
174 functions that allow one to make some observations about states. |
|
175 One is the ``live'' threads we have seen so far in a state: |
|
176 |
|
177 \begin{isabelle}\ \ \ \ \ %%% |
|
178 \mbox{\begin{tabular}{lcl} |
|
179 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & |
|
180 @{thm (rhs) threads.simps(1)}\\ |
|
181 @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} & |
|
182 @{thm (rhs) threads.simps(2)[where thread="th"]}\\ |
|
183 @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} & |
|
184 @{thm (rhs) threads.simps(3)[where thread="th"]}\\ |
|
185 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\ |
|
186 \end{tabular}} |
|
187 \end{isabelle} |
|
188 |
|
189 \noindent |
|
190 Another is that given a thread @{text "th"}, what is the original priority was at |
|
191 its inception. |
|
192 |
|
193 \begin{isabelle}\ \ \ \ \ %%% |
|
194 \mbox{\begin{tabular}{lcl} |
|
195 @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & |
|
196 @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\ |
|
197 @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & |
|
198 @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\ |
|
199 @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & |
|
200 @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\ |
|
201 @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\ |
|
202 \end{tabular}} |
|
203 \end{isabelle} |
|
204 |
|
205 \noindent |
|
206 In this definition we set @{text 0} as the default priority for |
|
207 threads that have not (yet) been created. The last function we need |
|
208 calculates the ``time'', or index, at which a process was created. |
|
209 |
|
210 \begin{isabelle}\ \ \ \ \ %%% |
|
211 \mbox{\begin{tabular}{lcl} |
|
212 @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & |
|
213 @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\ |
|
214 @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & |
|
215 @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\ |
|
216 @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & |
|
217 @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\ |
|
218 @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\ |
|
219 \end{tabular}} |
|
220 \end{isabelle} |
|
221 |
|
222 \begin{center} |
|
223 threads, original-priority, birth time, precedence. |
|
224 \end{center} |
|
225 |
|
226 |
|
227 |
|
228 resources |
|
229 |
|
230 step relation: |
|
231 |
|
232 \begin{center} |
|
233 \begin{tabular}{c} |
|
234 @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm} |
|
235 @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\ |
|
236 |
|
237 @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\ |
|
238 @{thm[mode=Rule] thread_V[where thread=th]}\\ |
147 \end{tabular} |
239 \end{tabular} |
148 \end{isabelle} |
240 \end{center} |
149 |
241 |
150 \noindent |
242 valid state: |
151 whereby threads, priorities and resources are represented as natural numbers. |
243 |
152 A \emph{state} is a list of events. |
244 \begin{center} |
|
245 \begin{tabular}{c} |
|
246 @{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm} |
|
247 @{thm[mode=Rule] vt_cons[where cs=step]} |
|
248 \end{tabular} |
|
249 \end{center} |
|
250 |
153 |
251 |
154 To define events, the identifiers of {\em threads}, |
252 To define events, the identifiers of {\em threads}, |
155 {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) |
253 {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) |
156 need to be represented. All three are represetned using standard |
254 need to be represented. All three are represetned using standard |
157 Isabelle/HOL type @{typ "nat"}: |
255 Isabelle/HOL type @{typ "nat"}: |
158 *} |
256 *} |
159 |
257 |
160 text {* |
258 text {* |
161 \bigskip |
259 \bigskip |
162 The priority inversion phenomenon was first published in \cite{Lampson80}. |
260 The priority inversion phenomenon was first published in |
163 The two protocols widely used to eliminate priority inversion, namely |
261 \cite{Lampson80}. The two protocols widely used to eliminate |
164 PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed |
262 priority inversion, namely PI (Priority Inheritance) and PCE |
165 in \cite{Sha90}. PCE is less convenient to use because it requires |
263 (Priority Ceiling Emulation), were proposed in \cite{Sha90}. PCE is |
166 static analysis of programs. Therefore, PI is more commonly used in |
264 less convenient to use because it requires static analysis of |
167 practice\cite{locke-july02}. However, as pointed out in the literature, |
265 programs. Therefore, PI is more commonly used in |
168 the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}. |
266 practice\cite{locke-july02}. However, as pointed out in the |
169 A formal analysis will certainly be helpful for us to understand and correctly |
267 literature, the analysis of priority inheritance protocol is quite |
170 implement PI. All existing formal analysis of PI |
268 subtle\cite{yodaiken-july02}. A formal analysis will certainly be |
171 \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the model checking |
269 helpful for us to understand and correctly implement PI. All |
172 technology. Because of the state explosion problem, model check |
270 existing formal analysis of PI |
173 is much like an exhaustive testing of finite models with limited size. |
271 \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the |
174 The results obtained can not be safely generalized to models with arbitrarily |
272 model checking technology. Because of the state explosion problem, |
175 large size. Worse still, since model checking is fully automatic, it give little |
273 model check is much like an exhaustive testing of finite models with |
176 insight on why the formal model is correct. It is therefore |
274 limited size. The results obtained can not be safely generalized to |
177 definitely desirable to analyze PI using theorem proving, which gives |
275 models with arbitrarily large size. Worse still, since model |
178 more general results as well as deeper insight. And this is the purpose |
276 checking is fully automatic, it give little insight on why the |
179 of this paper which gives a formal analysis of PI in the interactive |
277 formal model is correct. It is therefore definitely desirable to |
180 theorem prover Isabelle using Higher Order Logic (HOL). The formalization |
278 analyze PI using theorem proving, which gives more general results |
|
279 as well as deeper insight. And this is the purpose of this paper |
|
280 which gives a formal analysis of PI in the interactive theorem |
|
281 prover Isabelle using Higher Order Logic (HOL). The formalization |
181 focuses on on two issues: |
282 focuses on on two issues: |
182 |
283 |
183 \begin{enumerate} |
284 \begin{enumerate} |
184 \item The correctness of the protocol model itself. A series of desirable properties is |
285 \item The correctness of the protocol model itself. A series of desirable properties is |
185 derived until we are fully convinced that the formal model of PI does |
286 derived until we are fully convinced that the formal model of PI does |