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