regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:eb2fc3ac934d
+:a40a35d1bc91
 preempted. Priorities allow scheduling of threads that need to
 finish their work within deadlines.  Unfortunately, both features
 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
+$H$ blocks any other thread with lower priority and the thread itself cannot
-be blocked by any thread with lower priority. Alas, in a naive
+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
 possession of a lock for a resource that $H$ also needs. $H$ must
 therefore wait for $L$ to exit the critical section and release this
 {\bf Contributions:} There have been earlier formal investigations
 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
 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 *}
 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
+later to the case of PIP on multi-processor systems.}
-PIP is based on Paulson's inductive approach to protocol
+Following good experience in earlier work \cite{Wang09},
-verification \cite{Paulson98}, where the \emph{state} of a system is
+our model of PIP is based on Paulson's inductive approach to protocol
-given by a list of events that happened so far.  \emph{Events} of PIP fall
+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}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
 \isacommand{datatype} event
 but also @{text "th\<^isub>3"},
 which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
 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
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cpreced_def2}\hfill\numbered{cpreced}
 \end{isabelle}
 \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
 given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all
 threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
 \end{center}
 \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
+not lead to a cycle in the RAG. In practice, ensuring the latter
-the responsibility of the programmer.  In our formal
+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]}
 \end{center}
 only one lock, can cause indefinite Priority Inversion for one of the
 high-priority threads, invalidating their two bounds.
 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
 corresponding thread @{text th} with the highest precedence; we show
 that in every future state (denoted by @{text "s' @ s"}) in which
 s"}, the thread @{text th} and the events happening in @{text
 s'}. We list them next:
 \begin{quote}
 {\bf Assumptions on the states {\boldmath@{text s}} and
-{\boldmath@{text "s' @ s"}:}} In order to make
+{\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and
-any meaningful statement, we need to require that @{text "s"} and
+@{text "s' @ s"} are valid states:
-@{text "s' @ s"} are valid states, namely
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{l}
 @{term "vt s"}\\
 @{term "vt (s' @ s)"}
 \end{tabular}
 (*>*)
 section {* Properties for an Implementation\label{implement} *}
 text {*
-While a formal correctness proof for our model of PIP is certainly
+While our formalised proof gives us confidence about the correctness of our model of PIP,
-attractive (especially in light of the flawed proof by Sha et
+we found that the formalisation can even help us with efficiently implementing it.
-al.~\cite{Sha90}), we found that the formalisation can even help us
-with efficiently implementing PIP.
 For example Baker complained that calculating the current precedence
 in PIP is quite ``heavy weight'' in Linux (see the Introduction).
 In our model of PIP the current precedence of a thread in a state @{text s}
 depends on all its dependants---a ``global'' transitive notion,
 @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
 \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
+The first property is again telling us we do not need to change the @{text RAG}.
-however states that only threads that are \emph{not} dependants of @{text th} have their
+The second shows that the @{term cp}-values of all threads other than @{text th}
-current precedence unchanged. For the others we have to recalculate the current
+are unchanged. The reason is that @{text th} is running; therefore it is not in
-precedence. To do this we can start from @{term "th"}
+the @{term dependants} relation of any thread. This in turn means that the
-and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
+change of its priority cannot affect the threads.
-the @{term "cp"} of every
-thread encountered on the way. Since the @{term "depend"}
+%The second
-is assumed to be loop free, this procedure will always stop. The following two lemmas show, however,
+%however states that only threads that are \emph{not} dependants of @{text th} have their
-that this procedure can actually stop often earlier without having to consider all
+%current precedence unchanged. For the others we have to recalculate the current
-dependants.
+%precedence. To do this we can start from @{term "th"}
+%and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
-\begin{isabelle}\ \ \ \ \ %%%
+%the @{term "cp"} of every
-\begin{tabular}{@ {}l}
+%thread encountered on the way. Since the @{term "depend"}
-@{thm[mode=IfThen] eq_up_self}\\
+%is assumed to be loop free, this procedure will always stop. The following two lemmas show, however,
-@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+%that this procedure can actually stop often earlier without having to consider all
-@{text "then"} @{thm (concl) eq_up}.
+%dependants.
-\end{tabular}
+%
-\end{isabelle}
+%\begin{isabelle}\ \ \ \ \ %%%
+%\begin{tabular}{@ {}l}
-\noindent
+%@{thm[mode=IfThen] eq_up_self}\\
-The first lemma states that if the current precedence of @{text th} is unchanged,
+%@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
-then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
+%@{text "then"} @{thm (concl) eq_up}.
-The second states that if an intermediate @{term cp}-value does not change, then
+%\end{tabular}
-the procedure can also stop, because none of its dependent threads will
+%\end{isabelle}
-have their current precedence changed.
+%
+%\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
 *}
 (*<*)
 end
 context step_v_cps_nt
 (*>*)
 text {*
 \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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm depend_s}\\
 make the notions in the correctness proof by Sha et al.~\cite{Sha90}
 precise so that they can be processed by a theorem prover. The reason is
 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
+sometimes quite intricate and tedious, has been checked by Isabelle/HOL.
-reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
+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
+area of this method is security protocols.
-application of Paulson's method we know of outside this area is
-\cite{Wang09}.
 The second goal of our formalisation is to provide a specification for actually
 implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
 explain how to use various implementations of PIP and abstractly
 discuss their properties, but surprisingly lack most details important for a
 the next thread which takes over a lock is irrelevant for the correctness
 of PIP. Earlier model checking approaches which verified particular implementations
 of PIP \cite{Faria08,Jahier09,Wellings07} cannot
 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
 teaching. Priority Inversion certainly occurs also in
 slave processes. However, a formal investigation of this idea is beyond
 the scope of this paper.  We are not aware of any proofs in this
 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
+problem, which however needs static analysis of programs in order to
-static analysis of programs in order to avoid it.
+avoid it. {\bf mention model-checking approaches}
-His formalisation consists of 407 lemmas and 2500 lines of (PVS) code.  Our formalisation
+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
 definitions and proofs span over 770 lines of code. The properties relevant
 for an implementation require 2000 lines. The code of our formalisation
 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}
 *}

changeset 342	a40a35d1bc91
parent 341	eb2fc3ac934d
child 343	1687f868dd5e