--- a/prio/Paper/Paper.thy Mon Apr 16 12:54:08 2012 +0000
+++ b/prio/Paper/Paper.thy Mon Apr 16 15:08:24 2012 +0000
@@ -53,8 +53,8 @@
can interact in subtle ways leading to a problem, called
\emph{Priority Inversion}. Suppose three threads having priorities
$H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
- $H$ blocks any other thread with lower priority and itself cannot
- be blocked by any thread with lower priority. Alas, in a naive
+ $H$ blocks any other thread with lower priority and the thread itself cannot
+ be blocked indefinitely by any thread with lower priority. Alas, in a naive
implementation of resource locking and priorities this property can
be violated. Even worse, $H$ can be delayed indefinitely by
threads with lower priorities. For this let $L$ be in the
@@ -168,15 +168,15 @@
checking techniques. This paper presents a formalised and
mechanically checked proof for the correctness of PIP (to our
knowledge the first one).
- %; the earlier informal proof by Sha et
- %al.~\cite{Sha90} is flawed).
In contrast to model checking, our
formalisation provides insight into why PIP is correct and allows us
to prove stronger properties that, as we will show, can inform an
efficient implementation. For example, we found by ``playing'' with the formalisation
that the choice of the next thread to take over a lock when a
resource is released is irrelevant for PIP being correct---a fact
- that has not been mentioned in the literature.
+ that has not been mentioned in the literature. This is important
+ for an efficient implementation, because we can give the lock to the
+ thread with the highest priority so that it terminates more quickly.
*}
section {* Formal Model of the Priority Inheritance Protocol *}
@@ -184,10 +184,12 @@
text {*
The Priority Inheritance Protocol, short PIP, is a scheduling
algorithm for a single-processor system.\footnote{We shall come back
- later to the case of PIP on multi-processor systems.} Our model of
- PIP is based on Paulson's inductive approach to protocol
- verification \cite{Paulson98}, where the \emph{state} of a system is
- given by a list of events that happened so far. \emph{Events} of PIP fall
+ later to the case of PIP on multi-processor systems.}
+ Following good experience in earlier work \cite{Wang09},
+ our model of PIP is based on Paulson's inductive approach to protocol
+ verification \cite{Paulson98}. In this approach a \emph{state} of a system is
+ given by a list of events that happened so far (with new events prepended to the list).
+ \emph{Events} of PIP fall
into five categories defined as the datatype:
\begin{isabelle}\ \ \ \ \ %%%
@@ -369,7 +371,12 @@
in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies
in a RAG, then clearly
we have a deadlock. Therefore when a thread requests a resource,
- we must ensure that the resulting RAG is not circular.
+ we must ensure that the resulting RAG is not circular. In practice, the
+ programmer has to ensure this.
+
+
+ {\bf define detached}
+
Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
state @{text s}. It is defined as
@@ -380,7 +387,7 @@
\noindent
where the dependants of @{text th} are given by the waiting queue function.
- While the precedence @{term prec} of a thread is determined by the programmer
+ While the precedence @{term prec} of a thread is determined statically
(for example when the thread is
created), the point of the current precedence is to let the scheduler increase this
precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
@@ -567,14 +574,15 @@
\noindent
If a thread wants to lock a resource, then the thread needs to be
running and also we have to make sure that the resource lock does
- not lead to a cycle in the RAG. In practice, ensuring the latter is
- the responsibility of the programmer. In our formal
+ not lead to a cycle in the RAG. In practice, ensuring the latter
+ is the responsibility of the programmer. In our formal
model we brush aside these problematic cases in order to be able to make
some meaningful statements about PIP.\footnote{This situation is
similar to the infamous \emph{occurs check} in Prolog: In order to say
anything meaningful about unification, one needs to perform an occurs
check. But in practice the occurs check is omitted and the
responsibility for avoiding problems rests with the programmer.}
+
\begin{center}
@{thm[mode=Rule] thread_P[where thread=th]}
@@ -638,7 +646,8 @@
Even when fixed, their proof idea does not seem to go through for
us, because of the way we have set up our formal model of PIP. One
- reason is that we allow critical sections to intersect
+ reason is that we allow critical sections, which start with a @{text P}-event
+ and finish with a corresponding @{text V}-event, to arbitrarily overlap
(something Sha et al.~explicitly exclude). Therefore we have
designed a different correctness criterion for PIP. The idea behind
our criterion is as follows: for all states @{text s}, we know the
@@ -658,9 +667,8 @@
\begin{quote}
{\bf Assumptions on the states {\boldmath@{text s}} and
- {\boldmath@{text "s' @ s"}:}} In order to make
- any meaningful statement, we need to require that @{text "s"} and
- @{text "s' @ s"} are valid states, namely
+ {\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and
+ @{text "s' @ s"} are valid states:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{l}
@{term "vt s"}\\
@@ -960,10 +968,8 @@
section {* Properties for an Implementation\label{implement} *}
text {*
- While a formal correctness proof for our model of PIP is certainly
- attractive (especially in light of the flawed proof by Sha et
- al.~\cite{Sha90}), we found that the formalisation can even help us
- with efficiently implementing PIP.
+ While our formalised proof gives us confidence about the correctness of our model of PIP,
+ we found that the formalisation can even help us with efficiently implementing it.
For example Baker complained that calculating the current precedence
in PIP is quite ``heavy weight'' in Linux (see the Introduction).
@@ -1068,36 +1074,42 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm[mode=IfThen] eq_dep}, and\\
- @{thm[mode=IfThen] eq_cp}
+ @{thm[mode=IfThen] eq_cp_pre}
\end{tabular}
\end{isabelle}
\noindent
- The first property is again telling us we do not need to change the @{text RAG}. The second
- however states that only threads that are \emph{not} dependants of @{text th} have their
- current precedence unchanged. For the others we have to recalculate the current
- precedence. To do this we can start from @{term "th"}
- and follow the @{term "depend"}-edges to recompute using Lemma~\ref{childrenlem}
- the @{term "cp"} of every
- thread encountered on the way. Since the @{term "depend"}
- is assumed to be loop free, this procedure will always stop. The following two lemmas show, however,
- that this procedure can actually stop often earlier without having to consider all
- dependants.
+ The first property is again telling us we do not need to change the @{text RAG}.
+ The second shows that the @{term cp}-values of all threads other than @{text th}
+ are unchanged. The reason is that @{text th} is running; therefore it is not in
+ the @{term dependants} relation of any thread. This in turn means that the
+ change of its priority cannot affect the threads.
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{thm[mode=IfThen] eq_up_self}\\
- @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
- @{text "then"} @{thm (concl) eq_up}.
- \end{tabular}
- \end{isabelle}
-
- \noindent
- The first lemma states that if the current precedence of @{text th} is unchanged,
- then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
- The second states that if an intermediate @{term cp}-value does not change, then
- the procedure can also stop, because none of its dependent threads will
- have their current precedence changed.
+ %The second
+ %however states that only threads that are \emph{not} dependants of @{text th} have their
+ %current precedence unchanged. For the others we have to recalculate the current
+ %precedence. To do this we can start from @{term "th"}
+ %and follow the @{term "depend"}-edges to recompute using Lemma~\ref{childrenlem}
+ %the @{term "cp"} of every
+ %thread encountered on the way. Since the @{term "depend"}
+ %is assumed to be loop free, this procedure will always stop. The following two lemmas show, however,
+ %that this procedure can actually stop often earlier without having to consider all
+ %dependants.
+ %
+ %\begin{isabelle}\ \ \ \ \ %%%
+ %\begin{tabular}{@ {}l}
+ %@{thm[mode=IfThen] eq_up_self}\\
+ %@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+ %@{text "then"} @{thm (concl) eq_up}.
+ %\end{tabular}
+ %\end{isabelle}
+ %
+ %\noindent
+ %The first lemma states that if the current precedence of @{text th} is unchanged,
+ %then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
+ %The second states that if an intermediate @{term cp}-value does not change, then
+ %the procedure can also stop, because none of its dependent threads will
+ %have their current precedence changed.
\smallskip
*}
(*<*)
@@ -1153,7 +1165,7 @@
\noindent
\colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and
@{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
- the one where @{text cs} is locked, and where it is not. We treat the second case
+ the one where @{text cs} is not locked, and one where it is. We treat the former case
first by showing that
\begin{isabelle}\ \ \ \ \ %%%
@@ -1210,13 +1222,11 @@
that a mechanically checked proof avoids the flaws that crept into their
informal reasoning. We achieved this goal: The correctness of PIP now
only hinges on the assumptions behind our formal model. The reasoning, which is
- sometimes quite intricate and tedious, has been checked beyond any
- reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
+ sometimes quite intricate and tedious, has been checked by Isabelle/HOL.
+ We can also confirm that Paulson's
inductive method for protocol verification~\cite{Paulson98} is quite
suitable for our formal model and proof. The traditional application
- area of this method is security protocols. The only other
- application of Paulson's method we know of outside this area is
- \cite{Wang09}.
+ area of this method is security protocols.
The second goal of our formalisation is to provide a specification for actually
implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
@@ -1237,6 +1247,8 @@
provide this kind of ``deep understanding'' about the principles behind
PIP and its correctness.
+ {\bf rewrite the following slightly}
+
PIP is a scheduling algorithm for single-processor systems. We are
now living in a multi-processor world. So the question naturally
arises whether PIP has any relevance in such a world beyond
@@ -1260,11 +1272,12 @@
area, not even informal or flawed ones.
The most closely related work to ours is the formal verification in
- PVS of the Priority Ceiling Protocol done by Dutertre
- \cite{dutertre99b}---another solution to the Priority Inversion
- problem, which however needs
- static analysis of programs in order to avoid it.
- His formalisation consists of 407 lemmas and 2500 lines of (PVS) code. Our formalisation
+ PVS of the Priority Ceiling Protocol done by Dutertre
+ \cite{dutertre99b}---another solution to the Priority Inversion
+ problem, which however needs static analysis of programs in order to
+ avoid it. {\bf mention model-checking approaches}
+
+ Our formalisation
consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
code with a few apply-scripts interspersed. The formal model of PIP
is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
@@ -1273,6 +1286,13 @@
can be downloaded from
\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
+ {\bf say:
+ So this paper is a good witness for one
+of the major reasons to be interested in machine checked reasoning:
+gaining deeper understanding of the subject matter.
+ }
+
+
\bibliographystyle{plain}
\bibliography{root}
*}