262
|
1 |
(*<*)
|
|
2 |
theory Paper
|
301
|
3 |
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
|
262
|
4 |
begin
|
266
|
5 |
ML {*
|
273
|
6 |
open Printer;
|
272
|
7 |
show_question_marks_default := false;
|
266
|
8 |
*}
|
284
|
9 |
|
|
10 |
notation (latex output)
|
|
11 |
Cons ("_::_" [78,77] 73) and
|
|
12 |
vt ("valid'_state") and
|
|
13 |
runing ("running") and
|
286
|
14 |
birthtime ("last'_set") and
|
284
|
15 |
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
|
286
|
16 |
Prc ("'(_, _')") and
|
287
|
17 |
holding ("holds") and
|
|
18 |
waiting ("waits") and
|
290
|
19 |
Th ("T") and
|
|
20 |
Cs ("C") and
|
287
|
21 |
readys ("ready") and
|
290
|
22 |
depend ("RAG") and
|
|
23 |
preced ("prec") and
|
|
24 |
cpreced ("cprec") and
|
291
|
25 |
dependents ("dependants") and
|
298
|
26 |
cp ("cprec") and
|
|
27 |
holdents ("resources") and
|
299
|
28 |
original_priority ("priority") and
|
284
|
29 |
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
|
325
|
30 |
|
|
31 |
abbreviation
|
|
32 |
"detached s th \<equiv> cntP s th = cntV s th"
|
262
|
33 |
(*>*)
|
|
34 |
|
|
35 |
section {* Introduction *}
|
|
36 |
|
|
37 |
text {*
|
284
|
38 |
Many real-time systems need to support threads involving priorities and
|
267
|
39 |
locking of resources. Locking of resources ensures mutual exclusion
|
275
|
40 |
when accessing shared data or devices that cannot be
|
284
|
41 |
preempted. Priorities allow scheduling of threads that need to
|
275
|
42 |
finish their work within deadlines. Unfortunately, both features
|
|
43 |
can interact in subtle ways leading to a problem, called
|
284
|
44 |
\emph{Priority Inversion}. Suppose three threads having priorities
|
|
45 |
$H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
|
|
46 |
$H$ blocks any other thread with lower priority and itself cannot
|
|
47 |
be blocked by any thread with lower priority. Alas, in a naive
|
275
|
48 |
implementation of resource looking and priorities this property can
|
|
49 |
be violated. Even worse, $H$ can be delayed indefinitely by
|
284
|
50 |
threads with lower priorities. For this let $L$ be in the
|
275
|
51 |
possession of a lock for a resource that also $H$ needs. $H$ must
|
|
52 |
therefore wait for $L$ to exit the critical section and release this
|
|
53 |
lock. The problem is that $L$ might in turn be blocked by any
|
284
|
54 |
thread with priority $M$, and so $H$ sits there potentially waiting
|
|
55 |
indefinitely. Since $H$ is blocked by threads with lower
|
275
|
56 |
priorities, the problem is called Priority Inversion. It was first
|
277
|
57 |
described in \cite{Lampson80} in the context of the
|
275
|
58 |
Mesa programming language designed for concurrent programming.
|
265
|
59 |
|
273
|
60 |
If the problem of Priority Inversion is ignored, real-time systems
|
267
|
61 |
can become unpredictable and resulting bugs can be hard to diagnose.
|
|
62 |
The classic example where this happened is the software that
|
284
|
63 |
controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
|
|
64 |
Once the spacecraft landed, the software shut down at irregular
|
|
65 |
intervals leading to loss of project time as normal operation of the
|
|
66 |
craft could only resume the next day (the mission and data already
|
|
67 |
collected were fortunately not lost, because of a clever system
|
|
68 |
design). The reason for the shutdowns was that the scheduling
|
|
69 |
software fell victim of Priority Inversion: a low priority thread
|
|
70 |
locking a resource prevented a high priority thread from running in
|
|
71 |
time leading to a system reset. Once the problem was found, it was
|
|
72 |
rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
|
|
73 |
\cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
|
286
|
74 |
Inheritance Protocol} \cite{Sha90} and others sometimes also call it
|
|
75 |
\emph{Priority Boosting}.} in the scheduling software.
|
262
|
76 |
|
284
|
77 |
The idea behind PIP is to let the thread $L$ temporarily inherit
|
286
|
78 |
the high priority from $H$ until $L$ leaves the critical section
|
284
|
79 |
unlocking the resource. This solves the problem of $H$ having to
|
|
80 |
wait indefinitely, because $L$ cannot be blocked by threads having
|
|
81 |
priority $M$. While a few other solutions exist for the Priority
|
|
82 |
Inversion problem, PIP is one that is widely deployed and
|
|
83 |
implemented. This includes VxWorks (a proprietary real-time OS used
|
|
84 |
in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
|
|
85 |
ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
|
|
86 |
example in libraries for FreeBSD, Solaris and Linux.
|
274
|
87 |
|
284
|
88 |
One advantage of PIP is that increasing the priority of a thread
|
275
|
89 |
can be dynamically calculated by the scheduler. This is in contrast
|
277
|
90 |
to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
|
|
91 |
solution to the Priority Inversion problem, which requires static
|
284
|
92 |
analysis of the program in order to prevent Priority
|
|
93 |
Inversion. However, there has also been strong criticism against
|
|
94 |
PIP. For instance, PIP cannot prevent deadlocks when lock
|
|
95 |
dependencies are circular, and also blocking times can be
|
|
96 |
substantial (more than just the duration of a critical section).
|
|
97 |
Though, most criticism against PIP centres around unreliable
|
|
98 |
implementations and PIP being too complicated and too inefficient.
|
|
99 |
For example, Yodaiken writes in \cite{Yodaiken02}:
|
274
|
100 |
|
|
101 |
\begin{quote}
|
|
102 |
\it{}``Priority inheritance is neither efficient nor reliable. Implementations
|
|
103 |
are either incomplete (and unreliable) or surprisingly complex and intrusive.''
|
|
104 |
\end{quote}
|
273
|
105 |
|
274
|
106 |
\noindent
|
275
|
107 |
He suggests to avoid PIP altogether by not allowing critical
|
286
|
108 |
sections to be preempted. Unfortunately, this solution does not
|
304
|
109 |
help in real-time systems with hard deadlines for high-priority
|
|
110 |
threads.
|
278
|
111 |
|
286
|
112 |
In our opinion, there is clearly a need for investigating correct
|
278
|
113 |
algorithms for PIP. A few specifications for PIP exist (in English)
|
|
114 |
and also a few high-level descriptions of implementations (e.g.~in
|
|
115 |
the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
|
|
116 |
with actual implementations. That this is a problem in practise is
|
283
|
117 |
proved by an email from Baker, who wrote on 13 July 2009 on the Linux
|
278
|
118 |
Kernel mailing list:
|
274
|
119 |
|
|
120 |
\begin{quote}
|
275
|
121 |
\it{}``I observed in the kernel code (to my disgust), the Linux PIP
|
|
122 |
implementation is a nightmare: extremely heavy weight, involving
|
|
123 |
maintenance of a full wait-for graph, and requiring updates for a
|
|
124 |
range of events, including priority changes and interruptions of
|
|
125 |
wait operations.''
|
274
|
126 |
\end{quote}
|
|
127 |
|
|
128 |
\noindent
|
277
|
129 |
The criticism by Yodaiken, Baker and others suggests to us to look
|
|
130 |
again at PIP from a more abstract level (but still concrete enough
|
286
|
131 |
to inform an implementation), and makes PIP an ideal candidate for a
|
277
|
132 |
formal verification. One reason, of course, is that the original
|
284
|
133 |
presentation of PIP~\cite{Sha90}, despite being informally
|
283
|
134 |
``proved'' correct, is actually \emph{flawed}.
|
|
135 |
|
|
136 |
Yodaiken \cite{Yodaiken02} points to a subtlety that had been
|
|
137 |
overlooked in the informal proof by Sha et al. They specify in
|
284
|
138 |
\cite{Sha90} that after the thread (whose priority has been raised)
|
283
|
139 |
completes its critical section and releases the lock, it ``returns
|
|
140 |
to its original priority level.'' This leads them to believe that an
|
284
|
141 |
implementation of PIP is ``rather straightforward''~\cite{Sha90}.
|
|
142 |
Unfortunately, as Yodaiken points out, this behaviour is too
|
|
143 |
simplistic. Consider the case where the low priority thread $L$
|
|
144 |
locks \emph{two} resources, and two high-priority threads $H$ and
|
300
|
145 |
$H'$ each wait for one of them. If $L$ releases one resource
|
283
|
146 |
so that $H$, say, can proceed, then we still have Priority Inversion
|
|
147 |
with $H'$ (which waits for the other resource). The correct
|
|
148 |
behaviour for $L$ is to revert to the highest remaining priority of
|
284
|
149 |
the threads that it blocks. The advantage of formalising the
|
|
150 |
correctness of a high-level specification of PIP in a theorem prover
|
|
151 |
is that such issues clearly show up and cannot be overlooked as in
|
|
152 |
informal reasoning (since we have to analyse all possible behaviours
|
300
|
153 |
of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
|
274
|
154 |
|
300
|
155 |
\noindent
|
301
|
156 |
{\bf Contributions:} There have been earlier formal investigations
|
304
|
157 |
into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
|
|
158 |
checking techniques. This paper presents a formalised and
|
|
159 |
mechanically checked proof for the correctness of PIP (to our
|
305
|
160 |
knowledge the first one; the earlier informal proof by Sha et
|
304
|
161 |
al.~\cite{Sha90} is flawed). In contrast to model checking, our
|
|
162 |
formalisation provides insight into why PIP is correct and allows us
|
310
|
163 |
to prove stronger properties that, as we will show, can inform an
|
314
|
164 |
efficient implementation. For example, we found by ``playing'' with the formalisation
|
304
|
165 |
that the choice of the next thread to take over a lock when a
|
305
|
166 |
resource is released is irrelevant for PIP being correct. Something
|
|
167 |
which has not been mentioned in the relevant literature.
|
280
|
168 |
*}
|
278
|
169 |
|
283
|
170 |
section {* Formal Model of the Priority Inheritance Protocol *}
|
267
|
171 |
|
280
|
172 |
text {*
|
286
|
173 |
The Priority Inheritance Protocol, short PIP, is a scheduling
|
|
174 |
algorithm for a single-processor system.\footnote{We shall come back
|
|
175 |
later to the case of PIP on multi-processor systems.} Our model of
|
|
176 |
PIP is based on Paulson's inductive approach to protocol
|
|
177 |
verification \cite{Paulson98}, where the \emph{state} of a system is
|
298
|
178 |
given by a list of events that happened so far. \emph{Events} of PIP fall
|
290
|
179 |
into five categories defined as the datatype:
|
283
|
180 |
|
|
181 |
\begin{isabelle}\ \ \ \ \ %%%
|
284
|
182 |
\mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
|
|
183 |
\isacommand{datatype} event
|
|
184 |
& @{text "="} & @{term "Create thread priority"}\\
|
|
185 |
& @{text "|"} & @{term "Exit thread"} \\
|
286
|
186 |
& @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\
|
284
|
187 |
& @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
|
|
188 |
& @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
|
|
189 |
\end{tabular}}
|
|
190 |
\end{isabelle}
|
|
191 |
|
|
192 |
\noindent
|
286
|
193 |
whereby threads, priorities and (critical) resources are represented
|
|
194 |
as natural numbers. The event @{term Set} models the situation that
|
|
195 |
a thread obtains a new priority given by the programmer or
|
|
196 |
user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we
|
298
|
197 |
need to define functions that allow us to make some observations
|
297
|
198 |
about states. One, called @{term threads}, calculates the set of
|
293
|
199 |
``live'' threads that we have seen so far:
|
284
|
200 |
|
|
201 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
202 |
\mbox{\begin{tabular}{lcl}
|
|
203 |
@{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
|
|
204 |
@{thm (rhs) threads.simps(1)}\\
|
|
205 |
@{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} &
|
|
206 |
@{thm (rhs) threads.simps(2)[where thread="th"]}\\
|
|
207 |
@{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
|
|
208 |
@{thm (rhs) threads.simps(3)[where thread="th"]}\\
|
|
209 |
@{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
|
|
210 |
\end{tabular}}
|
283
|
211 |
\end{isabelle}
|
|
212 |
|
|
213 |
\noindent
|
299
|
214 |
In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
|
290
|
215 |
Another function calculates the priority for a thread @{text "th"}, which is
|
|
216 |
defined as
|
284
|
217 |
|
|
218 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
219 |
\mbox{\begin{tabular}{lcl}
|
|
220 |
@{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
|
|
221 |
@{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
|
|
222 |
@{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
|
|
223 |
@{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
|
|
224 |
@{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
|
|
225 |
@{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
|
|
226 |
@{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
|
|
227 |
\end{tabular}}
|
|
228 |
\end{isabelle}
|
|
229 |
|
|
230 |
\noindent
|
|
231 |
In this definition we set @{text 0} as the default priority for
|
|
232 |
threads that have not (yet) been created. The last function we need
|
285
|
233 |
calculates the ``time'', or index, at which time a process had its
|
290
|
234 |
priority last set.
|
284
|
235 |
|
|
236 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
237 |
\mbox{\begin{tabular}{lcl}
|
|
238 |
@{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
|
|
239 |
@{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
|
|
240 |
@{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
|
|
241 |
@{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
|
|
242 |
@{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
|
|
243 |
@{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
|
|
244 |
@{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
|
|
245 |
\end{tabular}}
|
|
246 |
\end{isabelle}
|
286
|
247 |
|
|
248 |
\noindent
|
287
|
249 |
In this definition @{term "length s"} stands for the length of the list
|
|
250 |
of events @{text s}. Again the default value in this function is @{text 0}
|
|
251 |
for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a
|
290
|
252 |
state @{text s} is the pair of natural numbers defined as
|
284
|
253 |
|
286
|
254 |
\begin{isabelle}\ \ \ \ \ %%%
|
290
|
255 |
@{thm preced_def[where thread="th"]}
|
286
|
256 |
\end{isabelle}
|
|
257 |
|
|
258 |
\noindent
|
287
|
259 |
The point of precedences is to schedule threads not according to priorities (because what should
|
286
|
260 |
we do in case two threads have the same priority), but according to precedences.
|
290
|
261 |
Precedences allow us to always discriminate between two threads with equal priority by
|
296
|
262 |
taking into account the time when the priority was last set. We order precedences so
|
286
|
263 |
that threads with the same priority get a higher precedence if their priority has been
|
293
|
264 |
set earlier, since for such threads it is more urgent to finish their work. In an implementation
|
|
265 |
this choice would translate to a quite natural FIFO-scheduling of processes with
|
286
|
266 |
the same priority.
|
|
267 |
|
|
268 |
Next, we introduce the concept of \emph{waiting queues}. They are
|
|
269 |
lists of threads associated with every resource. The first thread in
|
298
|
270 |
this list (i.e.~the head, or short @{term hd}) is chosen to be the one
|
290
|
271 |
that is in possession of the
|
286
|
272 |
``lock'' of the corresponding resource. We model waiting queues as
|
293
|
273 |
functions, below abbreviated as @{text wq}. They take a resource as
|
|
274 |
argument and return a list of threads. This allows us to define
|
290
|
275 |
when a thread \emph{holds}, respectively \emph{waits} for, a
|
293
|
276 |
resource @{text cs} given a waiting queue function @{text wq}.
|
287
|
277 |
|
|
278 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
279 |
\begin{tabular}{@ {}l}
|
290
|
280 |
@{thm cs_holding_def[where thread="th"]}\\
|
|
281 |
@{thm cs_waiting_def[where thread="th"]}
|
287
|
282 |
\end{tabular}
|
|
283 |
\end{isabelle}
|
|
284 |
|
|
285 |
\noindent
|
|
286 |
In this definition we assume @{text "set"} converts a list into a set.
|
298
|
287 |
At the beginning, that is in the state where no thread is created yet,
|
|
288 |
the waiting queue function will be the function that returns the
|
293
|
289 |
empty list for every resource.
|
291
|
290 |
|
|
291 |
\begin{isabelle}\ \ \ \ \ %%%
|
301
|
292 |
@{abbrev all_unlocked}\hfill\numbered{allunlocked}
|
291
|
293 |
\end{isabelle}
|
|
294 |
|
|
295 |
\noindent
|
290
|
296 |
Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs}
|
|
297 |
(RAG), which represent the dependencies between threads and resources.
|
|
298 |
We represent RAGs as relations using pairs of the form
|
|
299 |
|
|
300 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
301 |
@{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
|
|
302 |
@{term "(Cs cs, Th th)"}
|
|
303 |
\end{isabelle}
|
|
304 |
|
|
305 |
\noindent
|
|
306 |
where the first stands for a \emph{waiting edge} and the second for a
|
|
307 |
\emph{holding edge} (@{term Cs} and @{term Th} are constructors of a
|
|
308 |
datatype for vertices). Given a waiting queue function, a RAG is defined
|
306
|
309 |
as the union of the sets of waiting and holding edges, namely
|
290
|
310 |
|
|
311 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
312 |
@{thm cs_depend_def}
|
|
313 |
\end{isabelle}
|
|
314 |
|
|
315 |
\noindent
|
306
|
316 |
Given three threads and three resources, an instance of a RAG can be pictured
|
|
317 |
as follows:
|
290
|
318 |
|
|
319 |
\begin{center}
|
297
|
320 |
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
|
291
|
321 |
\begin{tikzpicture}[scale=1]
|
297
|
322 |
%%\draw[step=2mm] (-3,2) grid (1,-1);
|
291
|
323 |
|
297
|
324 |
\node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
|
|
325 |
\node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
|
|
326 |
\node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
|
|
327 |
\node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
|
|
328 |
\node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
|
298
|
329 |
\node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
|
297
|
330 |
\node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
|
291
|
331 |
|
300
|
332 |
\draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);
|
297
|
333 |
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
|
298
|
334 |
\draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);
|
300
|
335 |
\draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E);
|
|
336 |
\draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1);
|
298
|
337 |
\draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);
|
291
|
338 |
\end{tikzpicture}
|
290
|
339 |
\end{center}
|
|
340 |
|
|
341 |
\noindent
|
296
|
342 |
The use of relations for representing RAGs allows us to conveniently define
|
306
|
343 |
the notion of the \emph{dependants} of a thread using the transitive closure
|
|
344 |
operation for relations. This gives
|
290
|
345 |
|
|
346 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
347 |
@{thm cs_dependents_def}
|
|
348 |
\end{isabelle}
|
|
349 |
|
|
350 |
\noindent
|
296
|
351 |
This definition needs to account for all threads that wait for a thread to
|
290
|
352 |
release a resource. This means we need to include threads that transitively
|
298
|
353 |
wait for a resource being released (in the picture above this means the dependants
|
306
|
354 |
of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"},
|
|
355 |
but also @{text "th\<^isub>3"},
|
298
|
356 |
which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
|
306
|
357 |
in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle in a RAG, then clearly
|
291
|
358 |
we have a deadlock. Therefore when a thread requests a resource,
|
298
|
359 |
we must ensure that the resulting RAG is not circular.
|
291
|
360 |
|
298
|
361 |
Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
|
|
362 |
state @{text s}. It is defined as
|
291
|
363 |
|
|
364 |
\begin{isabelle}\ \ \ \ \ %%%
|
299
|
365 |
@{thm cpreced_def2}\hfill\numbered{cpreced}
|
291
|
366 |
\end{isabelle}
|
|
367 |
|
|
368 |
\noindent
|
306
|
369 |
where the dependants of @{text th} are given by the waiting queue function.
|
293
|
370 |
While the precedence @{term prec} of a thread is determined by the programmer
|
|
371 |
(for example when the thread is
|
306
|
372 |
created), the point of the current precedence is to let the scheduler increase this
|
|
373 |
precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
|
291
|
374 |
given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all
|
306
|
375 |
threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
|
291
|
376 |
defined as the transitive closure of all dependent threads, we deal correctly with the
|
306
|
377 |
problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
|
291
|
378 |
lowered prematurely.
|
|
379 |
|
298
|
380 |
The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
|
306
|
381 |
by recursion on the state (a list of events); this function returns a \emph{schedule state}, which
|
298
|
382 |
we represent as a record consisting of two
|
296
|
383 |
functions:
|
293
|
384 |
|
|
385 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
386 |
@{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
|
|
387 |
\end{isabelle}
|
291
|
388 |
|
294
|
389 |
\noindent
|
314
|
390 |
The first function is a waiting queue function (that is, it takes a
|
|
391 |
resource @{text "cs"} and returns the corresponding list of threads
|
|
392 |
that lock, respectively wait for, it); the second is a function that
|
|
393 |
takes a thread and returns its current precedence (see
|
|
394 |
\eqref{cpreced}). We assume the usual getter and setter methods for
|
|
395 |
such records.
|
294
|
396 |
|
306
|
397 |
In the initial state, the scheduler starts with all resources unlocked (the corresponding
|
|
398 |
function is defined in \eqref{allunlocked}) and the
|
298
|
399 |
current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
|
299
|
400 |
\mbox{@{abbrev initial_cprec}}. Therefore
|
306
|
401 |
we have for the initial state
|
291
|
402 |
|
|
403 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
404 |
\begin{tabular}{@ {}l}
|
|
405 |
@{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\
|
294
|
406 |
\hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
|
291
|
407 |
\end{tabular}
|
|
408 |
\end{isabelle}
|
|
409 |
|
|
410 |
\noindent
|
296
|
411 |
The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
|
|
412 |
we calculate the waiting queue function of the (previous) state @{text s};
|
298
|
413 |
this waiting queue function @{text wq} is unchanged in the next schedule state---because
|
306
|
414 |
none of these events lock or release any resource;
|
|
415 |
for calculating the next @{term "cprec_fun"}, we use @{text wq} and
|
298
|
416 |
@{term cpreced}. This gives the following three clauses for @{term schs}:
|
290
|
417 |
|
|
418 |
\begin{isabelle}\ \ \ \ \ %%%
|
291
|
419 |
\begin{tabular}{@ {}l}
|
|
420 |
@{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\
|
294
|
421 |
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
|
298
|
422 |
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\
|
291
|
423 |
@{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
|
294
|
424 |
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
|
|
425 |
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
|
291
|
426 |
@{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\
|
294
|
427 |
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
|
|
428 |
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
|
291
|
429 |
\end{tabular}
|
|
430 |
\end{isabelle}
|
|
431 |
|
|
432 |
\noindent
|
306
|
433 |
More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
|
300
|
434 |
we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
|
306
|
435 |
the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th}
|
314
|
436 |
appended to the end of that list (remember the head of this list is assigned to be in the possession of this
|
306
|
437 |
resource). This gives the clause
|
291
|
438 |
|
|
439 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
440 |
\begin{tabular}{@ {}l}
|
|
441 |
@{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\
|
294
|
442 |
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
|
291
|
443 |
\hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
|
294
|
444 |
\hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
|
291
|
445 |
\end{tabular}
|
|
446 |
\end{isabelle}
|
|
447 |
|
|
448 |
\noindent
|
300
|
449 |
The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function
|
301
|
450 |
so that the thread that possessed the lock is deleted from the corresponding thread list. For this
|
|
451 |
list transformation, we use
|
296
|
452 |
the auxiliary function @{term release}. A simple version of @{term release} would
|
306
|
453 |
just delete this thread and return the remaining threads, namely
|
291
|
454 |
|
|
455 |
\begin{isabelle}\ \ \ \ \ %%%
|
296
|
456 |
\begin{tabular}{@ {}lcl}
|
|
457 |
@{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
|
|
458 |
@{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
|
|
459 |
\end{tabular}
|
291
|
460 |
\end{isabelle}
|
|
461 |
|
|
462 |
\noindent
|
300
|
463 |
In practice, however, often the thread with the highest precedence in the list will get the
|
296
|
464 |
lock next. We have implemented this choice, but later found out that the choice
|
300
|
465 |
of which thread is chosen next is actually irrelevant for the correctness of PIP.
|
296
|
466 |
Therefore we prove the stronger result where @{term release} is defined as
|
|
467 |
|
|
468 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
469 |
\begin{tabular}{@ {}lcl}
|
|
470 |
@{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
|
|
471 |
@{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\
|
|
472 |
\end{tabular}
|
|
473 |
\end{isabelle}
|
|
474 |
|
|
475 |
\noindent
|
306
|
476 |
where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
|
298
|
477 |
choice for the next waiting list. It just has to be a list of distinctive threads and
|
|
478 |
contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
|
291
|
479 |
|
|
480 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
481 |
\begin{tabular}{@ {}l}
|
|
482 |
@{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
|
294
|
483 |
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
|
291
|
484 |
\hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
|
294
|
485 |
\hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
|
291
|
486 |
\end{tabular}
|
290
|
487 |
\end{isabelle}
|
|
488 |
|
300
|
489 |
Having the scheduler function @{term schs} at our disposal, we can ``lift'', or
|
|
490 |
overload, the notions
|
|
491 |
@{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.
|
286
|
492 |
|
|
493 |
\begin{isabelle}\ \ \ \ \ %%%
|
298
|
494 |
\begin{tabular}{@ {}rcl}
|
|
495 |
@{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
|
|
496 |
@{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
|
|
497 |
@{thm (lhs) s_depend_abv} & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\
|
|
498 |
@{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}
|
287
|
499 |
\end{tabular}
|
|
500 |
\end{isabelle}
|
|
501 |
|
298
|
502 |
\noindent
|
300
|
503 |
With these abbreviations we can introduce
|
|
504 |
the notion of threads being @{term readys} in a state (i.e.~threads
|
298
|
505 |
that do not wait for any resource) and the running thread.
|
|
506 |
|
287
|
507 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
508 |
\begin{tabular}{@ {}l}
|
|
509 |
@{thm readys_def}\\
|
|
510 |
@{thm runing_def}\\
|
286
|
511 |
\end{tabular}
|
|
512 |
\end{isabelle}
|
284
|
513 |
|
298
|
514 |
\noindent
|
306
|
515 |
In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
|
|
516 |
Note that in the initial state, that is where the list of events is empty, the set
|
309
|
517 |
@{term threads} is empty and therefore there is neither a thread ready nor running.
|
298
|
518 |
If there is one or more threads ready, then there can only be \emph{one} thread
|
|
519 |
running, namely the one whose current precedence is equal to the maximum of all ready
|
314
|
520 |
threads. We use sets to capture both possibilities.
|
306
|
521 |
We can now also conveniently define the set of resources that are locked by a thread in a
|
298
|
522 |
given state.
|
284
|
523 |
|
298
|
524 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
525 |
@{thm holdents_def}
|
|
526 |
\end{isabelle}
|
284
|
527 |
|
306
|
528 |
Finally we can define what a \emph{valid state} is in our model of PIP. For
|
304
|
529 |
example we cannot expect to be able to exit a thread, if it was not
|
306
|
530 |
created yet. These validity constraints on states are characterised by the
|
|
531 |
inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
|
|
532 |
for @{term step} relating a state and an event that can happen next.
|
284
|
533 |
|
|
534 |
\begin{center}
|
|
535 |
\begin{tabular}{c}
|
|
536 |
@{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
|
298
|
537 |
@{thm[mode=Rule] thread_exit[where thread=th]}
|
|
538 |
\end{tabular}
|
|
539 |
\end{center}
|
|
540 |
|
|
541 |
\noindent
|
|
542 |
The first rule states that a thread can only be created, if it does not yet exists.
|
|
543 |
Similarly, the second rule states that a thread can only be terminated if it was
|
306
|
544 |
running and does not lock any resources anymore (this simplifies slightly our model;
|
314
|
545 |
in practice we would expect the operating system releases all locks held by a
|
306
|
546 |
thread that is about to exit). The event @{text Set} can happen
|
298
|
547 |
if the corresponding thread is running.
|
284
|
548 |
|
298
|
549 |
\begin{center}
|
|
550 |
@{thm[mode=Rule] thread_set[where thread=th]}
|
|
551 |
\end{center}
|
|
552 |
|
|
553 |
\noindent
|
301
|
554 |
If a thread wants to lock a resource, then the thread needs to be
|
|
555 |
running and also we have to make sure that the resource lock does
|
|
556 |
not lead to a cycle in the RAG. In practice, ensuring the latter is
|
314
|
557 |
the responsibility of the programmer. In our formal
|
|
558 |
model we brush aside these problematic cases in order to be able to make
|
301
|
559 |
some meaningful statements about PIP.\footnote{This situation is
|
310
|
560 |
similar to the infamous occurs check in Prolog: In order to say
|
306
|
561 |
anything meaningful about unification, one needs to perform an occurs
|
310
|
562 |
check. But in practice the occurs check is ommited and the
|
306
|
563 |
responsibility for avoiding problems rests with the programmer.}
|
|
564 |
|
|
565 |
\begin{center}
|
|
566 |
@{thm[mode=Rule] thread_P[where thread=th]}
|
|
567 |
\end{center}
|
|
568 |
|
|
569 |
\noindent
|
301
|
570 |
Similarly, if a thread wants to release a lock on a resource, then
|
|
571 |
it must be running and in the possession of that lock. This is
|
306
|
572 |
formally given by the last inference rule of @{term step}.
|
|
573 |
|
298
|
574 |
\begin{center}
|
306
|
575 |
@{thm[mode=Rule] thread_V[where thread=th]}
|
284
|
576 |
\end{center}
|
306
|
577 |
|
298
|
578 |
\noindent
|
|
579 |
A valid state of PIP can then be conveniently be defined as follows:
|
284
|
580 |
|
|
581 |
\begin{center}
|
|
582 |
\begin{tabular}{c}
|
298
|
583 |
@{thm[mode=Axiom] vt_nil}\hspace{1cm}
|
|
584 |
@{thm[mode=Rule] vt_cons}
|
284
|
585 |
\end{tabular}
|
|
586 |
\end{center}
|
|
587 |
|
298
|
588 |
\noindent
|
|
589 |
This completes our formal model of PIP. In the next section we present
|
309
|
590 |
properties that show our model of PIP is correct.
|
298
|
591 |
*}
|
274
|
592 |
|
310
|
593 |
section {* The Correctness Proof *}
|
298
|
594 |
|
301
|
595 |
(*<*)
|
|
596 |
context extend_highest_gen
|
|
597 |
begin
|
307
|
598 |
(*>*)
|
301
|
599 |
text {*
|
322
|
600 |
Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
|
|
601 |
for PIP in terms of the number of critical resources: if there are
|
|
602 |
@{text m} critical resources, then a blocked job with high priority
|
324
|
603 |
can only be blocked @{text m} times---that is a \emph{bounded}
|
|
604 |
number of times. This result on its own, strictly speaking, does
|
|
605 |
\emph{not} prevent indefinite, or unbounded, Priority Inversion,
|
|
606 |
because if one low-priority thread does not give up its critical
|
|
607 |
resource (the one the high-priority thread is waiting for), then the
|
322
|
608 |
high-priority thread can never run. The argument of Sha et al.~is
|
|
609 |
that \emph{if} threads release locked resources in a finite amount
|
324
|
610 |
of time, then indefinite Priority Inversion cannot occur---the high-priority
|
322
|
611 |
thread is guaranteed to run eventually. The assumption is that
|
|
612 |
programmers always ensure that this is the case. However, even
|
324
|
613 |
taking this assumption into account, ther correctness property is
|
|
614 |
\emph{not} true for their version of PIP. As Yodaiken
|
|
615 |
\cite{Yodaiken02} pointed out: If a low-priority thread possesses
|
|
616 |
locks to two resources for which two high-priority threads are
|
|
617 |
waiting for, then lowering the priority prematurely after giving up
|
|
618 |
only one lock, can cause indefinite Priority Inversion for one of the
|
|
619 |
high-priority threads, invalidating their bound.
|
307
|
620 |
|
323
|
621 |
Even when fixed, their proof idea does not seem to go through for
|
|
622 |
us, because of the way we have set up our formal model of PIP. The
|
|
623 |
reason is that we allow that critical sections can intersect
|
|
624 |
(something Sha et al.~explicitly exclude). Therefore we have a
|
|
625 |
different correctness criterion for PIP. The idea behind our
|
|
626 |
criterion is as follows: for all states @{text
|
|
627 |
s}, we know the corresponding thread @{text th} with the highest
|
|
628 |
precedence; we show that in every future state (denoted by @{text
|
|
629 |
"s' @ s"}) in which @{text th} is still alive, either @{text th} is
|
|
630 |
running or it is blocked by a thread that was alive in the state
|
|
631 |
@{text s}. Since in @{text s}, as in every state, the set of alive
|
|
632 |
threads is finite, @{text th} can only be blocked a finite number of
|
|
633 |
times. We will actually prove a stricter bound below. However, this
|
|
634 |
correctness criterion hinges upon a number of assumptions about the
|
|
635 |
states @{text s} and @{text "s' @ s"}, the thread @{text th} and the
|
|
636 |
events happening in @{text s'}. We list them next:
|
307
|
637 |
|
|
638 |
\begin{quote}
|
|
639 |
{\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make
|
|
640 |
any meaningful statement, we need to require that @{text "s"} and
|
|
641 |
@{text "s' @ s"} are valid states, namely
|
|
642 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
643 |
\begin{tabular}{l}
|
|
644 |
@{term "vt s"}\\
|
|
645 |
@{term "vt (s' @ s)"}
|
|
646 |
\end{tabular}
|
|
647 |
\end{isabelle}
|
|
648 |
\end{quote}
|
301
|
649 |
|
307
|
650 |
\begin{quote}
|
310
|
651 |
{\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and
|
|
652 |
has the highest precedence of all alive threads in @{text s}. Furthermore the
|
|
653 |
priority of @{text th} is @{text prio} (we need this in the next assumptions).
|
307
|
654 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
655 |
\begin{tabular}{l}
|
|
656 |
@{term "th \<in> threads s"}\\
|
|
657 |
@{term "prec th s = Max (cprec s ` threads s)"}\\
|
|
658 |
@{term "prec th s = (prio, DUMMY)"}
|
|
659 |
\end{tabular}
|
|
660 |
\end{isabelle}
|
|
661 |
\end{quote}
|
|
662 |
|
|
663 |
\begin{quote}
|
|
664 |
{\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
|
309
|
665 |
be blocked indefinitely. Of course this can happen if threads with higher priority
|
|
666 |
than @{text th} are continously created in @{text s'}. Therefore we have to assume that
|
|
667 |
events in @{text s'} can only create (respectively set) threads with equal or lower
|
310
|
668 |
priority than @{text prio} of @{text th}. We also need to assume that the
|
|
669 |
priority of @{text "th"} does not get reset and also that @{text th} does
|
|
670 |
not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications.
|
307
|
671 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
672 |
\begin{tabular}{l}
|
310
|
673 |
{If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
|
307
|
674 |
{If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
|
|
675 |
{If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
|
|
676 |
\end{tabular}
|
|
677 |
\end{isabelle}
|
|
678 |
\end{quote}
|
301
|
679 |
|
307
|
680 |
\noindent
|
310
|
681 |
Under these assumptions we will prove the following correctness property:
|
307
|
682 |
|
308
|
683 |
\begin{theorem}\label{mainthm}
|
307
|
684 |
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
|
308
|
685 |
the thread @{text th} and the events in @{text "s'"},
|
|
686 |
if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
|
|
687 |
@{text "th' \<in> threads s"}.
|
307
|
688 |
\end{theorem}
|
301
|
689 |
|
308
|
690 |
\noindent
|
324
|
691 |
This theorem ensures that the thread @{text th}, which has the
|
|
692 |
highest precedence in the state @{text s}, can only be blocked in
|
|
693 |
the state @{text "s' @ s"} by a thread @{text th'} that already
|
|
694 |
existed in @{text s}. As we shall see shortly, that means by only
|
|
695 |
finitely many threads. Like in the argument by Sha et al.~this
|
|
696 |
finite bound does not guarantee absence of indefinite Priority
|
|
697 |
Inversion. For this we further have to assume that every thread
|
|
698 |
gives up its resources after a finite amount of time. We found that
|
|
699 |
this assumption is awkward to formalise in our model. Therefore we
|
|
700 |
leave it out and let the programmer assume the responsibility to
|
325
|
701 |
program threads in such a benign manner (in addition to causeing no
|
|
702 |
circularity in the @{text RAG}). In this detail, we do not
|
324
|
703 |
make any progress in comparison with the work by Sha et al.
|
309
|
704 |
|
|
705 |
In what follows we will describe properties of PIP that allow us to prove
|
325
|
706 |
Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
|
|
707 |
It is relatively easily to see that
|
309
|
708 |
|
|
709 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
710 |
\begin{tabular}{@ {}l}
|
|
711 |
@{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
|
|
712 |
@{thm[mode=IfThen] finite_threads}
|
|
713 |
\end{tabular}
|
|
714 |
\end{isabelle}
|
|
715 |
|
|
716 |
\noindent
|
325
|
717 |
whereby the second property is by induction of @{term vt}. The next three
|
309
|
718 |
properties are
|
308
|
719 |
|
309
|
720 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
721 |
\begin{tabular}{@ {}l}
|
|
722 |
@{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
|
|
723 |
@{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
|
|
724 |
@{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
|
|
725 |
\end{tabular}
|
|
726 |
\end{isabelle}
|
308
|
727 |
|
309
|
728 |
\noindent
|
325
|
729 |
The first property states that every waiting thread can only wait for a single
|
|
730 |
resource (because it gets suspended after requesting that resource); the second
|
|
731 |
that every resource can only be held by a single thread;
|
310
|
732 |
the third property establishes that in every given valid state, there is
|
|
733 |
at most one running thread. We can also show the following properties
|
325
|
734 |
about the @{term RAG} in @{text "s"}.
|
310
|
735 |
|
|
736 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
737 |
\begin{tabular}{@ {}l}
|
312
|
738 |
@{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\
|
|
739 |
\hspace{5mm}@{thm (concl) acyclic_depend},
|
|
740 |
@{thm (concl) finite_depend} and
|
|
741 |
@{thm (concl) wf_dep_converse},\\
|
325
|
742 |
\hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}
|
|
743 |
and\\
|
|
744 |
\hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
|
310
|
745 |
\end{tabular}
|
|
746 |
\end{isabelle}
|
309
|
747 |
|
325
|
748 |
\noindent
|
|
749 |
The acyclicity property follow from how we restricted the events in
|
|
750 |
@{text step}; similarly the finiteness and well-foundedness property.
|
|
751 |
The last two properties establish that every thread in a @{text "RAG"}
|
|
752 |
(either holding or waiting for a resource) is a live thread.
|
|
753 |
|
|
754 |
To state the key lemma in our proof, it will be convenient to introduce the notion
|
|
755 |
of a \emph{detached} thread in a state, that is one which does not hold any
|
|
756 |
critical resource nor requests one.
|
|
757 |
|
|
758 |
\begin{lemma}\label{mainlem}
|
|
759 |
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
|
|
760 |
the thread @{text th} and the events in @{text "s'"},
|
|
761 |
if @{term "th' \<in> treads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
|
|
762 |
then @{text "th' \<notin> running (s' @ s)"}.
|
|
763 |
\end{lemma}
|
309
|
764 |
|
|
765 |
\noindent
|
325
|
766 |
The point of this lemma is that a thread different from @{text th} (which has the highest
|
|
767 |
precedence in @{text s}) not holding any resource cannot be running
|
|
768 |
in the state @{text "s' @ s"}.
|
301
|
769 |
|
325
|
770 |
\begin{proof}
|
|
771 |
Since thread @{text "th'"} does not hold any resource, no thread can depend on it.
|
|
772 |
Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence
|
|
773 |
@{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the
|
|
774 |
state @{text "(s' @ s)"} and precedences are distinct among threads, we have
|
|
775 |
@{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this
|
|
776 |
we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
|
|
777 |
Since @{text "prec th (s' @ s)"} is already the highest
|
|
778 |
@{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by
|
|
779 |
definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
|
|
780 |
Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
|
|
781 |
By defintion of @{text "running"}, @{text "th'"} can not be running in state
|
|
782 |
@{text "s' @ s"}, as we had to show.\qed
|
|
783 |
\end{proof}
|
308
|
784 |
|
325
|
785 |
\noindent
|
|
786 |
Since @{text "th'"} is not able to run at state @{text "s' @ s"}, it is not able to
|
328
|
787 |
issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
|
325
|
788 |
one step further, @{text "th'"} still cannot hold any resource. The situation will
|
|
789 |
not change in further extensions as long as @{text "th"} holds the highest precedence.
|
|
790 |
|
326
|
791 |
From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that
|
|
792 |
held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
|
|
793 |
that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the
|
|
794 |
precedence of @{text th} in @{text "s"}.
|
325
|
795 |
|
326
|
796 |
\begin{theorem}
|
|
797 |
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
|
|
798 |
the thread @{text th} and the events in @{text "s'"}, if
|
|
799 |
@{term "th' \<in> running (s' @ s)"}, @{text "th' \<noteq> th"}, then
|
|
800 |
@{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and
|
|
801 |
@{term "cp (s' @ s) th' = prec th s"}.
|
|
802 |
\end{theorem}
|
301
|
803 |
|
328
|
804 |
\noindent
|
326
|
805 |
We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
|
|
806 |
This theorem gives a stricter bound on the processes that can block @{text th}:
|
|
807 |
only threads that were alive in state @{text s} and moreover held a resource.
|
|
808 |
Finally, the theorem establishes that the blocking threads have the
|
|
809 |
current precedence raised to the precedence of @{text th}.
|
|
810 |
|
328
|
811 |
We can furthermore prove that no deadlock exists in the state @{text "s' @ s"}
|
|
812 |
by showing that @{text "running (s' @ s)"} is not empty.
|
|
813 |
|
|
814 |
\begin{lemma}
|
|
815 |
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
|
|
816 |
the thread @{text th} and the events in @{text "s'"},
|
|
817 |
@{term "running (s' @ s) \<noteq> {}"}.
|
|
818 |
\end{lemma}
|
|
819 |
|
|
820 |
\begin{proof}
|
|
821 |
If @{text th} is blocked, then by following its dependants graph, we can always
|
|
822 |
reach a ready thread @{text th'}, and that thread must have inherited the
|
|
823 |
precedence of @{text th}.\qed
|
|
824 |
\end{proof}
|
|
825 |
|
|
826 |
|
326
|
827 |
%The following lemmas show how every node in RAG can be chased to ready threads:
|
|
828 |
%\begin{enumerate}
|
|
829 |
%\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
|
|
830 |
% @ {thm [display] chain_building[rule_format]}
|
|
831 |
%\item The ready thread chased to is unique (@{text "dchain_unique"}):
|
|
832 |
% @ {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
|
|
833 |
%\end{enumerate}
|
301
|
834 |
|
326
|
835 |
%Some deeper results about the system:
|
|
836 |
%\begin{enumerate}
|
|
837 |
%\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
|
|
838 |
%@ {thm [display] max_cp_eq}
|
|
839 |
%\item There must be one ready thread having the max @{term "cp"}-value
|
|
840 |
%(@{text "max_cp_readys_threads"}):
|
|
841 |
%@ {thm [display] max_cp_readys_threads}
|
|
842 |
%\end{enumerate}
|
325
|
843 |
|
326
|
844 |
%The relationship between the count of @{text "P"} and @{text "V"} and the number of
|
|
845 |
%critical resources held by a thread is given as follows:
|
|
846 |
%\begin{enumerate}
|
|
847 |
%\item The @{term "V"}-operation decreases the number of critical resources
|
|
848 |
% one thread holds (@{text "cntCS_v_dec"})
|
|
849 |
% @ {thm [display] cntCS_v_dec}
|
|
850 |
%\item The number of @{text "V"} never exceeds the number of @{text "P"}
|
|
851 |
% (@ {text "cnp_cnv_cncs"}):
|
|
852 |
% @ {thm [display] cnp_cnv_cncs}
|
|
853 |
%\item The number of @{text "V"} equals the number of @{text "P"} when
|
|
854 |
% the relevant thread is not living:
|
|
855 |
% (@{text "cnp_cnv_eq"}):
|
|
856 |
% @ {thm [display] cnp_cnv_eq}
|
|
857 |
%\item When a thread is not living, it does not hold any critical resource
|
|
858 |
% (@{text "not_thread_holdents"}):
|
|
859 |
% @ {thm [display] not_thread_holdents}
|
|
860 |
%\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant
|
|
861 |
% thread does not hold any critical resource, therefore no thread can depend on it
|
|
862 |
% (@{text "count_eq_dependents"}):
|
|
863 |
% @ {thm [display] count_eq_dependents}
|
|
864 |
%\end{enumerate}
|
313
|
865 |
|
326
|
866 |
%The reason that only threads which already held some resoures
|
|
867 |
%can be runing and block @{text "th"} is that if , otherwise, one thread
|
|
868 |
%does not hold any resource, it may never have its prioirty raised
|
|
869 |
%and will not get a chance to run. This fact is supported by
|
|
870 |
%lemma @{text "moment_blocked"}:
|
|
871 |
%@ {thm [display] moment_blocked}
|
|
872 |
%When instantiating @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
|
|
873 |
%resource in state @{text "s"} will not have a change to run latter. Rephrased, it means
|
|
874 |
%any thread which is running after @{text "th"} became the highest must have already held
|
|
875 |
%some resource at state @{text "s"}.
|
313
|
876 |
|
|
877 |
|
326
|
878 |
%When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means
|
|
879 |
%if a thread releases all its resources at some moment in @{text "t"}, after that,
|
|
880 |
%it may never get a change to run. If every thread releases its resource in finite duration,
|
|
881 |
%then after a while, only thread @{text "th"} is left running. This shows how indefinite
|
|
882 |
%priority inversion can be avoided.
|
313
|
883 |
|
326
|
884 |
%All these assumptions are put into a predicate @{term "extend_highest_gen"}.
|
|
885 |
%It can be proved that @{term "extend_highest_gen"} holds
|
|
886 |
%for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
|
|
887 |
%@ {thm [display] red_moment}
|
325
|
888 |
|
326
|
889 |
%From this, an induction principle can be derived for @{text "t"}, so that
|
|
890 |
%properties already derived for @{term "t"} can be applied to any prefix
|
|
891 |
%of @{text "t"} in the proof of new properties
|
|
892 |
%about @{term "t"} (@{text "ind"}):
|
|
893 |
%\begin{center}
|
|
894 |
%@ {thm[display] ind}
|
|
895 |
%\end{center}
|
325
|
896 |
|
326
|
897 |
%The following properties can be proved about @{term "th"} in @{term "t"}:
|
|
898 |
%\begin{enumerate}
|
|
899 |
%\item In @{term "t"}, thread @{term "th"} is kept live and its
|
|
900 |
% precedence is preserved as well
|
|
901 |
% (@{text "th_kept"}):
|
|
902 |
% @ {thm [display] th_kept}
|
|
903 |
%\item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among
|
|
904 |
% all living threads
|
|
905 |
% (@{text "max_preced"}):
|
|
906 |
% @ {thm [display] max_preced}
|
|
907 |
%\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
|
|
908 |
% among all living threads
|
|
909 |
% (@{text "th_cp_max_preced"}):
|
|
910 |
% @ {thm [display] th_cp_max_preced}
|
|
911 |
%\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current
|
|
912 |
% precedence among all living threads
|
|
913 |
% (@{text "th_cp_max"}):
|
|
914 |
% @ {thm [display] th_cp_max}
|
|
915 |
%\item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment
|
|
916 |
% @{term "s"}
|
|
917 |
% (@{text "th_cp_preced"}):
|
|
918 |
% @ {thm [display] th_cp_preced}
|
|
919 |
%\end{enumerate}
|
|
920 |
|
|
921 |
%The main theorem of this part is to characterizing the running thread during @{term "t"}
|
|
922 |
%(@{text "runing_inversion_2"}):
|
|
923 |
%@ {thm [display] runing_inversion_2}
|
|
924 |
%According to this, if a thread is running, it is either @{term "th"} or was
|
|
925 |
%already live and held some resource
|
|
926 |
%at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
|
|
927 |
|
|
928 |
%Since there are only finite many threads live and holding some resource at any moment,
|
|
929 |
%if every such thread can release all its resources in finite duration, then after finite
|
|
930 |
%duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
|
|
931 |
%then.
|
325
|
932 |
*}
|
313
|
933 |
(*<*)
|
|
934 |
end
|
|
935 |
(*>*)
|
|
936 |
|
314
|
937 |
section {* Properties for an Implementation\label{implement} *}
|
311
|
938 |
|
|
939 |
text {*
|
312
|
940 |
While a formal correctness proof for our model of PIP is certainly
|
|
941 |
attractive (especially in light of the flawed proof by Sha et
|
|
942 |
al.~\cite{Sha90}), we found that the formalisation can even help us
|
|
943 |
with efficiently implementing PIP.
|
311
|
944 |
|
312
|
945 |
For example Baker complained that calculating the current precedence
|
321
|
946 |
in PIP is quite ``heavy weight'' in Linux (see the Introduction).
|
312
|
947 |
In our model of PIP the current precedence of a thread in a state s
|
|
948 |
depends on all its dependants---a ``global'' transitive notion,
|
|
949 |
which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
|
321
|
950 |
We can however improve upon this. For this let us define the notion
|
|
951 |
of @{term children} of a thread @{text th} in a state @{text s} as
|
312
|
952 |
|
|
953 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
954 |
\begin{tabular}{@ {}l}
|
|
955 |
@{thm children_def2}
|
|
956 |
\end{tabular}
|
|
957 |
\end{isabelle}
|
|
958 |
|
|
959 |
\noindent
|
321
|
960 |
where a child is a thread that is one ``hop'' away from the tread
|
|
961 |
@{text th} in the @{term RAG} (and waiting for @{text th} to release
|
|
962 |
a resource). We can prove that
|
311
|
963 |
|
312
|
964 |
\begin{lemma}\label{childrenlem}
|
|
965 |
@{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
|
|
966 |
\begin{center}
|
|
967 |
@{thm (concl) cp_rec}.
|
|
968 |
\end{center}
|
|
969 |
\end{lemma}
|
311
|
970 |
|
312
|
971 |
\noindent
|
|
972 |
That means the current precedence of a thread @{text th} can be
|
|
973 |
computed locally by considering only the children of @{text th}. In
|
|
974 |
effect, it only needs to be recomputed for @{text th} when one of
|
321
|
975 |
its children changes its current precedence. Once the current
|
312
|
976 |
precedence is computed in this more efficient manner, the selection
|
|
977 |
of the thread with highest precedence from a set of ready threads is
|
|
978 |
a standard scheduling operation implemented in most operating
|
|
979 |
systems.
|
311
|
980 |
|
321
|
981 |
Of course the main implementation work for PIP involves the
|
|
982 |
scheduler and coding how it should react to events. Below we
|
|
983 |
outline how our formalisation guides this implementation for each
|
|
984 |
kind of event.\smallskip
|
312
|
985 |
*}
|
311
|
986 |
|
|
987 |
(*<*)
|
312
|
988 |
context step_create_cps
|
|
989 |
begin
|
|
990 |
(*>*)
|
|
991 |
text {*
|
|
992 |
\noindent
|
321
|
993 |
\colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and
|
312
|
994 |
the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
|
|
995 |
is allowed to occur). In this situation we can show that
|
|
996 |
|
|
997 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
998 |
\begin{tabular}{@ {}l}
|
321
|
999 |
@{thm eq_dep},\\
|
|
1000 |
@{thm eq_cp_th}, and\\
|
312
|
1001 |
@{thm[mode=IfThen] eq_cp}
|
|
1002 |
\end{tabular}
|
|
1003 |
\end{isabelle}
|
|
1004 |
|
|
1005 |
\noindent
|
|
1006 |
This means we do not have recalculate the @{text RAG} and also none of the
|
|
1007 |
current precedences of the other threads. The current precedence of the created
|
321
|
1008 |
thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
|
312
|
1009 |
\smallskip
|
|
1010 |
*}
|
|
1011 |
(*<*)
|
|
1012 |
end
|
|
1013 |
context step_exit_cps
|
|
1014 |
begin
|
|
1015 |
(*>*)
|
|
1016 |
text {*
|
|
1017 |
\noindent
|
321
|
1018 |
\colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and
|
312
|
1019 |
the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
|
|
1020 |
|
|
1021 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1022 |
\begin{tabular}{@ {}l}
|
321
|
1023 |
@{thm eq_dep}, and\\
|
312
|
1024 |
@{thm[mode=IfThen] eq_cp}
|
|
1025 |
\end{tabular}
|
|
1026 |
\end{isabelle}
|
|
1027 |
|
|
1028 |
\noindent
|
321
|
1029 |
This means again we do not have to recalculate the @{text RAG} and
|
|
1030 |
also not the current precedences for the other threads. Since @{term th} is not
|
312
|
1031 |
alive anymore in state @{term "s"}, there is no need to calculate its
|
|
1032 |
current precedence.
|
|
1033 |
\smallskip
|
|
1034 |
*}
|
|
1035 |
(*<*)
|
|
1036 |
end
|
311
|
1037 |
context step_set_cps
|
|
1038 |
begin
|
|
1039 |
(*>*)
|
312
|
1040 |
text {*
|
|
1041 |
\noindent
|
321
|
1042 |
\colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and
|
312
|
1043 |
@{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
|
311
|
1044 |
|
312
|
1045 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1046 |
\begin{tabular}{@ {}l}
|
321
|
1047 |
@{thm[mode=IfThen] eq_dep}, and\\
|
312
|
1048 |
@{thm[mode=IfThen] eq_cp}
|
|
1049 |
\end{tabular}
|
|
1050 |
\end{isabelle}
|
311
|
1051 |
|
312
|
1052 |
\noindent
|
321
|
1053 |
The first property is again telling us we do not need to change the @{text RAG}. The second
|
|
1054 |
however states that only threads that are \emph{not} dependants of @{text th} have their
|
312
|
1055 |
current precedence unchanged. For the others we have to recalculate the current
|
|
1056 |
precedence. To do this we can start from @{term "th"}
|
|
1057 |
and follow the @{term "depend"}-chains to recompute the @{term "cp"} of every
|
|
1058 |
thread encountered on the way using Lemma~\ref{childrenlem}. Since the @{term "depend"}
|
321
|
1059 |
is loop free, this procedure will always stop. The following two lemmas show, however,
|
|
1060 |
that this procedure can actually stop often earlier without having to consider all
|
|
1061 |
dependants.
|
312
|
1062 |
|
|
1063 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1064 |
\begin{tabular}{@ {}l}
|
|
1065 |
@{thm[mode=IfThen] eq_up_self}\\
|
|
1066 |
@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
|
|
1067 |
@{text "then"} @{thm (concl) eq_up}.
|
|
1068 |
\end{tabular}
|
|
1069 |
\end{isabelle}
|
|
1070 |
|
|
1071 |
\noindent
|
|
1072 |
The first states that if the current precedence of @{text th} is unchanged,
|
|
1073 |
then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
|
|
1074 |
The second states that if an intermediate @{term cp}-value does not change, then
|
|
1075 |
the procedure can also stop, because none of its dependent threads will
|
|
1076 |
have their current precedence changed.
|
|
1077 |
\smallskip
|
311
|
1078 |
*}
|
|
1079 |
(*<*)
|
|
1080 |
end
|
|
1081 |
context step_v_cps_nt
|
|
1082 |
begin
|
|
1083 |
(*>*)
|
|
1084 |
text {*
|
312
|
1085 |
\noindent
|
321
|
1086 |
\colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and
|
312
|
1087 |
@{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
|
|
1088 |
subcases: one where there is a thread to ``take over'' the released
|
321
|
1089 |
resource @{text cs}, and one where there is not. Let us consider them
|
312
|
1090 |
in turn. Suppose in state @{text s}, the thread @{text th'} takes over
|
|
1091 |
resource @{text cs} from thread @{text th}. We can show
|
311
|
1092 |
|
|
1093 |
|
312
|
1094 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1095 |
@{thm depend_s}
|
|
1096 |
\end{isabelle}
|
|
1097 |
|
|
1098 |
\noindent
|
|
1099 |
which shows how the @{text RAG} needs to be changed. This also suggests
|
|
1100 |
how the current precedences need to be recalculated. For threads that are
|
|
1101 |
not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
|
|
1102 |
can show
|
|
1103 |
|
|
1104 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1105 |
@{thm[mode=IfThen] cp_kept}
|
|
1106 |
\end{isabelle}
|
|
1107 |
|
|
1108 |
\noindent
|
|
1109 |
For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
|
|
1110 |
recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
|
|
1111 |
\noindent
|
|
1112 |
In the other case where there is no thread that takes over @{text cs}, we can show how
|
|
1113 |
to recalculate the @{text RAG} and also show that no current precedence needs
|
321
|
1114 |
to be recalculated.
|
312
|
1115 |
|
|
1116 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1117 |
\begin{tabular}{@ {}l}
|
|
1118 |
@{thm depend_s}\\
|
|
1119 |
@{thm eq_cp}
|
|
1120 |
\end{tabular}
|
|
1121 |
\end{isabelle}
|
311
|
1122 |
*}
|
|
1123 |
(*<*)
|
|
1124 |
end
|
|
1125 |
context step_P_cps_e
|
|
1126 |
begin
|
|
1127 |
(*>*)
|
|
1128 |
|
|
1129 |
text {*
|
312
|
1130 |
\noindent
|
321
|
1131 |
\colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and
|
312
|
1132 |
@{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
|
|
1133 |
the one where @{text cs} is locked, and where it is not. We treat the second case
|
|
1134 |
first by showing that
|
|
1135 |
|
|
1136 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1137 |
\begin{tabular}{@ {}l}
|
|
1138 |
@{thm depend_s}\\
|
|
1139 |
@{thm eq_cp}
|
|
1140 |
\end{tabular}
|
|
1141 |
\end{isabelle}
|
311
|
1142 |
|
312
|
1143 |
\noindent
|
|
1144 |
This means we do not need to add a holding edge to the @{text RAG} and no
|
321
|
1145 |
current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
|
312
|
1146 |
\noindent
|
|
1147 |
In the second case we know that resouce @{text cs} is locked. We can show that
|
|
1148 |
|
|
1149 |
\begin{isabelle}\ \ \ \ \ %%%
|
|
1150 |
\begin{tabular}{@ {}l}
|
|
1151 |
@{thm depend_s}\\
|
|
1152 |
@{thm[mode=IfThen] eq_cp}
|
|
1153 |
\end{tabular}
|
|
1154 |
\end{isabelle}
|
311
|
1155 |
|
312
|
1156 |
\noindent
|
|
1157 |
That means we have to add a waiting edge to the @{text RAG}. Furthermore
|
321
|
1158 |
the current precedence for all threads that are not dependants of @{text th}
|
|
1159 |
are unchanged. For the others we need to follow the edges
|
312
|
1160 |
in the @{text RAG} and recompute the @{term "cp"}. However, like in the
|
321
|
1161 |
@case of {text Set}, this operation can stop often earlier, namely when intermediate
|
312
|
1162 |
values do not change.
|
311
|
1163 |
*}
|
|
1164 |
(*<*)
|
|
1165 |
end
|
|
1166 |
(*>*)
|
|
1167 |
text {*
|
312
|
1168 |
\noindent
|
321
|
1169 |
A pleasing result of our formalisation is that the properties in
|
|
1170 |
this section closely inform an implementation of PIP: Whether the
|
|
1171 |
@{text RAG} needs to be reconfigured or current precedences need to
|
|
1172 |
recalculated for an event is given by a lemma we proved.
|
311
|
1173 |
*}
|
|
1174 |
|
298
|
1175 |
section {* Conclusion *}
|
|
1176 |
|
300
|
1177 |
text {*
|
314
|
1178 |
The Priority Inheritance Protocol (PIP) is a classic textbook
|
315
|
1179 |
algorithm used in real-time operating systems in order to avoid the problem of
|
|
1180 |
Priority Inversion. Although classic and widely used, PIP does have
|
317
|
1181 |
its faults: for example it does not prevent deadlocks in cases where threads
|
315
|
1182 |
have circular lock dependencies.
|
300
|
1183 |
|
317
|
1184 |
We had two goals in mind with our formalisation of PIP: One is to
|
315
|
1185 |
make the notions in the correctness proof by Sha et al.~\cite{Sha90}
|
317
|
1186 |
precise so that they can be processed by a theorem prover. The reason is
|
|
1187 |
that a mechanically checked proof avoids the flaws that crept into their
|
|
1188 |
informal reasoning. We achieved this goal: The correctness of PIP now
|
315
|
1189 |
only hinges on the assumptions behind our formal model. The reasoning, which is
|
314
|
1190 |
sometimes quite intricate and tedious, has been checked beyond any
|
315
|
1191 |
reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
|
321
|
1192 |
inductive method for protocol verification~\cite{Paulson98} is quite
|
315
|
1193 |
suitable for our formal model and proof. The traditional application
|
|
1194 |
area of this method is security protocols. The only other
|
|
1195 |
application of Paulson's method we know of outside this area is
|
|
1196 |
\cite{Wang09}.
|
301
|
1197 |
|
317
|
1198 |
The second goal of our formalisation is to provide a specification for actually
|
|
1199 |
implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
|
315
|
1200 |
explain how to use various implementations of PIP and abstractly
|
317
|
1201 |
discuss their properties, but surprisingly lack most details for a
|
|
1202 |
programmer who wants to implement PIP. That this is an issue in practice is illustrated by the
|
315
|
1203 |
email from Baker we cited in the Introduction. We achieved also this
|
317
|
1204 |
goal: The formalisation gives the first author enough data to enable
|
|
1205 |
his undergraduate students to implement PIP (as part of their OS course)
|
|
1206 |
on top of PINTOS, a small operating system for teaching
|
315
|
1207 |
purposes. A byproduct of our formalisation effort is that nearly all
|
314
|
1208 |
design choices for the PIP scheduler are backed up with a proved
|
317
|
1209 |
lemma. We were also able to establish the property that the choice of
|
|
1210 |
the next thread which takes over a lock is irrelevant for the correctness
|
|
1211 |
of PIP. Earlier model checking approaches which verified implementations
|
|
1212 |
of PIP \cite{Faria08,Jahier09,Wellings07} cannot
|
|
1213 |
provide this kind of ``deep understanding'' about the principles behind
|
|
1214 |
PIP and its correctness.
|
315
|
1215 |
|
|
1216 |
PIP is a scheduling algorithm for single-processor systems. We are
|
316
|
1217 |
now living in a multi-processor world. So the question naturally
|
318
|
1218 |
arises whether PIP has any relevance in such a world beyond
|
|
1219 |
teaching. Priority Inversion certainly occurs also in
|
321
|
1220 |
multi-processor systems. However, the surprising answer, according
|
|
1221 |
to \cite{Steinberg10}, is that except for one unsatisfactory
|
|
1222 |
proposal nobody has a good idea for how PIP should be modified to
|
|
1223 |
work correctly on multi-processor systems. The difficulties become
|
|
1224 |
clear when considering that locking and releasing a resource always
|
|
1225 |
requires a small amount of time. If processes work independently,
|
|
1226 |
then a low priority process can ``steal'' in such an unguarded
|
|
1227 |
moment a lock for a resource that was supposed allow a high-priority
|
|
1228 |
process to run next. Thus the problem of Priority Inversion is not
|
|
1229 |
really prevented. It seems difficult to design a PIP-algorithm with
|
|
1230 |
a meaningful correctness property on a multi-processor systems where
|
|
1231 |
processes work independently. We can imagine PIP to be of use in
|
|
1232 |
situations where processes are \emph{not} independent, but
|
|
1233 |
coordinated via a master process that distributes work over some
|
|
1234 |
slave processes. However, a formal investigation of this is beyond
|
|
1235 |
the scope of this paper. We are not aware of any proofs in this
|
|
1236 |
area, not even informal ones.
|
265
|
1237 |
|
321
|
1238 |
The most closely related work to ours is the formal verification in
|
|
1239 |
PVS for Priority Ceiling done by Dutertre \cite{dutertre99b}. His formalisation
|
|
1240 |
consists of 407 lemmas and 2500 lines of ``specification'' (we do not
|
|
1241 |
know whether this includes also code for proofs). Our formalisation
|
|
1242 |
consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
|
|
1243 |
code with a few apply-scripts interspersed. The formal model of PIP
|
|
1244 |
is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
|
|
1245 |
definitions and proofs took 770 lines of code. The properties relevant
|
327
|
1246 |
for an implementation took 2000 lines. %%Our code can be downloaded from
|
|
1247 |
%%...
|
321
|
1248 |
|
|
1249 |
\bibliographystyle{plain}
|
|
1250 |
\bibliography{root}
|
262
|
1251 |
*}
|
|
1252 |
|
264
|
1253 |
|
|
1254 |
(*<*)
|
|
1255 |
end
|
262
|
1256 |
(*>*) |