9 |
9 |
10 notation (latex output) |
10 notation (latex output) |
11 Cons ("_::_" [78,77] 73) and |
11 Cons ("_::_" [78,77] 73) and |
12 vt ("valid'_state") and |
12 vt ("valid'_state") and |
13 runing ("running") and |
13 runing ("running") and |
14 birthtime ("inception") and |
14 birthtime ("last'_set") and |
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
|
16 Prc ("'(_, _')") and |
16 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") |
17 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") |
17 (*>*) |
18 (*>*) |
18 |
19 |
19 section {* Introduction *} |
20 section {* Introduction *} |
20 |
21 |
53 software fell victim of Priority Inversion: a low priority thread |
54 software fell victim of Priority Inversion: a low priority thread |
54 locking a resource prevented a high priority thread from running in |
55 locking a resource prevented a high priority thread from running in |
55 time leading to a system reset. Once the problem was found, it was |
56 time leading to a system reset. Once the problem was found, it was |
56 rectified by enabling the \emph{Priority Inheritance Protocol} (PIP) |
57 rectified by enabling the \emph{Priority Inheritance Protocol} (PIP) |
57 \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority |
58 \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority |
58 Inheritance Protocol} \cite{Sha90} and others sometimes call it |
59 Inheritance Protocol} \cite{Sha90} and others sometimes also call it |
59 also \emph{Priority Boosting}.} in the scheduling software. |
60 \emph{Priority Boosting}.} in the scheduling software. |
60 |
61 |
61 The idea behind PIP is to let the thread $L$ temporarily inherit |
62 The idea behind PIP is to let the thread $L$ temporarily inherit |
62 the high priority from $H$ until $L$ leaves the critical section by |
63 the high priority from $H$ until $L$ leaves the critical section |
63 unlocking the resource. This solves the problem of $H$ having to |
64 unlocking the resource. This solves the problem of $H$ having to |
64 wait indefinitely, because $L$ cannot be blocked by threads having |
65 wait indefinitely, because $L$ cannot be blocked by threads having |
65 priority $M$. While a few other solutions exist for the Priority |
66 priority $M$. While a few other solutions exist for the Priority |
66 Inversion problem, PIP is one that is widely deployed and |
67 Inversion problem, PIP is one that is widely deployed and |
67 implemented. This includes VxWorks (a proprietary real-time OS used |
68 implemented. This includes VxWorks (a proprietary real-time OS used |
87 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
88 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
88 \end{quote} |
89 \end{quote} |
89 |
90 |
90 \noindent |
91 \noindent |
91 He suggests to avoid PIP altogether by not allowing critical |
92 He suggests to avoid PIP altogether by not allowing critical |
92 sections to be preempted. While this might have been a reasonable |
93 sections to be preempted. Unfortunately, this solution does not |
93 solution in 2002, in our modern multiprocessor world, this seems out |
94 help in real-time systems with low latency \emph{requirements}. |
94 of date. The reason is that this precludes other high-priority |
95 |
95 threads from running even when they do not make any use of the locked |
96 In our opinion, there is clearly a need for investigating correct |
96 resource. |
|
97 |
|
98 However, there is clearly a need for investigating correct |
|
99 algorithms for PIP. A few specifications for PIP exist (in English) |
97 algorithms for PIP. A few specifications for PIP exist (in English) |
100 and also a few high-level descriptions of implementations (e.g.~in |
98 and also a few high-level descriptions of implementations (e.g.~in |
101 the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little |
99 the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little |
102 with actual implementations. That this is a problem in practise is |
100 with actual implementations. That this is a problem in practise is |
103 proved by an email from Baker, who wrote on 13 July 2009 on the Linux |
101 proved by an email from Baker, who wrote on 13 July 2009 on the Linux |
112 \end{quote} |
110 \end{quote} |
113 |
111 |
114 \noindent |
112 \noindent |
115 The criticism by Yodaiken, Baker and others suggests to us to look |
113 The criticism by Yodaiken, Baker and others suggests to us to look |
116 again at PIP from a more abstract level (but still concrete enough |
114 again at PIP from a more abstract level (but still concrete enough |
117 to inform an implementation) and makes PIP an ideal candidate for a |
115 to inform an implementation), and makes PIP an ideal candidate for a |
118 formal verification. One reason, of course, is that the original |
116 formal verification. One reason, of course, is that the original |
119 presentation of PIP~\cite{Sha90}, despite being informally |
117 presentation of PIP~\cite{Sha90}, despite being informally |
120 ``proved'' correct, is actually \emph{flawed}. |
118 ``proved'' correct, is actually \emph{flawed}. |
121 |
119 |
122 Yodaiken \cite{Yodaiken02} points to a subtlety that had been |
120 Yodaiken \cite{Yodaiken02} points to a subtlety that had been |
141 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
139 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
142 |
140 |
143 vt (valid trace) was introduced earlier, cite |
141 vt (valid trace) was introduced earlier, cite |
144 |
142 |
145 distributed PIP |
143 distributed PIP |
|
144 |
|
145 Paulson's method has not been used outside security field, except |
|
146 work by Zhang et al. |
|
147 |
|
148 no clue about multi-processor case according to \cite{Steinberg10} |
146 *} |
149 *} |
147 |
150 |
148 section {* Formal Model of the Priority Inheritance Protocol *} |
151 section {* Formal Model of the Priority Inheritance Protocol *} |
149 |
152 |
150 text {* |
153 text {* |
151 We follow the original work by Sha et al.~\cite{Sha90} by modelling |
154 The Priority Inheritance Protocol, short PIP, is a scheduling |
152 first a classical single CPU system where only one \emph{thread} is |
155 algorithm for a single-processor system.\footnote{We shall come back |
153 active at any given moment. We shall discuss later how to lift this |
156 later to the case of PIP on multi-processor systems.} Our model of |
154 restriction. Our model of PIP is based on Paulson's inductive |
157 PIP is based on Paulson's inductive approach to protocol |
155 approach to protocol verification \cite{Paulson98}, where the |
158 verification \cite{Paulson98}, where the \emph{state} of a system is |
156 \emph{state} of a system is given by a list of events that |
159 given by a list of events that happened so far. \emph{Events} fall |
157 happened so far. \emph{Events} fall into four categories defined as |
160 into five categories defined as the datatype |
158 the datatype |
|
159 |
161 |
160 \begin{isabelle}\ \ \ \ \ %%% |
162 \begin{isabelle}\ \ \ \ \ %%% |
161 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
163 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
162 \isacommand{datatype} event |
164 \isacommand{datatype} event |
163 & @{text "="} & @{term "Create thread priority"}\\ |
165 & @{text "="} & @{term "Create thread priority"}\\ |
164 & @{text "|"} & @{term "Exit thread"} \\ |
166 & @{text "|"} & @{term "Exit thread"} \\ |
165 & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the proprity for} @{text thread}\\ |
167 & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\ |
166 & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\ |
168 & @{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"} |
169 & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"} |
168 \end{tabular}} |
170 \end{tabular}} |
169 \end{isabelle} |
171 \end{isabelle} |
170 |
172 |
171 \noindent |
173 \noindent |
172 whereby threads, priorities and (critical) resources are represented |
174 whereby threads, priorities and (critical) resources are represented |
173 as natural numbers. As in Paulson's work, we need to define |
175 as natural numbers. The event @{term Set} models the situation that |
174 functions that allow one to make some observations about states. |
176 a thread obtains a new priority given by the programmer or |
175 One is the ``live'' threads we have seen so far in a state: |
177 user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we |
|
178 need to define functions that allow one to make some observations |
|
179 about states. One, called @{term threads}, calculates the set of |
|
180 ``live'' threads that we have seen so far in a state: |
176 |
181 |
177 \begin{isabelle}\ \ \ \ \ %%% |
182 \begin{isabelle}\ \ \ \ \ %%% |
178 \mbox{\begin{tabular}{lcl} |
183 \mbox{\begin{tabular}{lcl} |
179 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & |
184 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & |
180 @{thm (rhs) threads.simps(1)}\\ |
185 @{thm (rhs) threads.simps(1)}\\ |
217 @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & |
221 @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & |
218 @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\ |
222 @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\ |
219 @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\ |
223 @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\ |
220 \end{tabular}} |
224 \end{tabular}} |
221 \end{isabelle} |
225 \end{isabelle} |
|
226 |
|
227 \footnote{Can Precedence be the real birth-time / or must be time precedence last set?} |
|
228 |
|
229 \noindent |
|
230 A \emph{precedence} of a thread @{text th} in a state @{text s} is a pair of |
|
231 natural numbers defined as |
222 |
232 |
223 \begin{center} |
233 \begin{isabelle}\ \ \ \ \ %%% |
224 threads, original-priority, birth time, precedence. |
234 @{thm (rhs) preced_def[where thread="th"]} |
225 \end{center} |
235 \end{isabelle} |
|
236 |
|
237 \noindent |
|
238 The point of precedences is to schedule threads not according to priorities (what should |
|
239 we do in case two threads have the same priority), but according to precedences. |
|
240 Precedences allow us to always discriminate two threads with equal priority by |
|
241 tacking into account the time when the priority was last set. We order precedences so |
|
242 that threads with the same priority get a higher precedence if their priority has been |
|
243 set earlier, since for such threads it is more urgent to finish. In an impementation |
|
244 this choice would translate to a quite natural a FIFO-scheduling of processes with |
|
245 the same priority. |
|
246 |
|
247 Next, we introduce the concept of \emph{waiting queues}. They are |
|
248 lists of threads associated with every resource. The first thread in |
|
249 this list is chosen to be in the one that is in possession of the |
|
250 ``lock'' of the corresponding resource. We model waiting queues as |
|
251 functions, below abbreviated as @{text wq}, taking a resource as |
|
252 argument and returning a list of threads. This allows us to define |
|
253 when a thread \emph{holds}, respectively \emph{waits}, for a |
|
254 resource @{text cs}. |
|
255 |
|
256 \begin{isabelle}\ \ \ \ \ %%% |
|
257 \begin{tabular}{@ {}l} |
|
258 @{thm cs_holding_def[where thread="th"]}\\ |
|
259 @{thm cs_waiting_def[where thread="th"]} |
|
260 \end{tabular} |
|
261 \end{isabelle} |
226 |
262 |
227 |
263 |
228 |
264 |
229 resources |
265 resources |
230 |
266 |
935 |
971 |
936 *} |
972 *} |
937 |
973 |
938 section {* Conclusions \label{conclusion} *} |
974 section {* Conclusions \label{conclusion} *} |
939 |
975 |
|
976 text {* |
|
977 The work in this paper only deals with single CPU configurations. The |
|
978 "one CPU" assumption is essential for our formalisation, because the |
|
979 main lemma fails in multi-CPU configuration. The lemma says that any |
|
980 runing thead must be the one with the highest prioirty or already held |
|
981 some resource when the highest priority thread was initiated. When |
|
982 there are multiple CPUs, it may well be the case that a threads did |
|
983 not hold any resource when the highest priority thread was initiated, |
|
984 but that thread still runs after that moment on a separate CPU. In |
|
985 this way, the main lemma does not hold anymore. |
|
986 |
|
987 |
|
988 There are some works deals with priority inversion in multi-CPU |
|
989 configurations[???], but none of them have given a formal correctness |
|
990 proof. The extension of our formal proof to deal with multi-CPU |
|
991 configurations is not obvious. One possibility, as suggested in paper |
|
992 [???], is change our formal model (the defiintion of "schs") to give |
|
993 the released resource to the thread with the highest prioirty. In this |
|
994 way, indefinite prioirty inversion can be avoided, but for a quite |
|
995 different reason from the one formalized in this paper (because the |
|
996 "mail lemma" will be different). This means a formal correctness proof |
|
997 for milt-CPU configuration would be quite different from the one given |
|
998 in this paper. The solution of prioirty inversion problem in mult-CPU |
|
999 configurations is a different problem which needs different solutions |
|
1000 which is outside the scope of this paper. |
|
1001 |
|
1002 *} |
|
1003 |
940 (*<*) |
1004 (*<*) |
941 end |
1005 end |
942 (*>*) |
1006 (*>*) |