regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:3d154253d5fe
+:ccb6c0601614
 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
-implementation.  For example, we found by ``playing'' with the formalisation
+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. Something
 which has not been mentioned in the relevant literature.
 *}
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
 \end{isabelle}
 \noindent
-The first function is a waiting queue function (that is, it takes a resource @{text "cs"} and returns the
+The first function is a waiting queue function (that is, it takes a
-corresponding list of threads that wait for it), the second is a function that takes
+resource @{text "cs"} and returns the corresponding list of threads
-a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and
+that lock, respectively wait for, it); the second is a function that
-setter methods for such records.
+takes a thread and returns its current precedence (see
+\eqref{cpreced}). We assume the usual getter and setter methods for
+such records.
 In the initial state, the scheduler starts with all resources unlocked (the corresponding
 function is defined in \eqref{allunlocked}) and the
 current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
 \mbox{@{abbrev initial_cprec}}. Therefore
 \noindent
 More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
 we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
 the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th}
-appended to the end of that list (remember the head of this list is seen to be in the possession of this
+appended to the end of that list (remember the head of this list is assigned to be in the possession of this
 resource). This gives the clause
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\
 In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
 Note that in the initial state, that is where the list of events is empty, the set
 @{term threads} is empty and therefore there is neither a thread ready nor running.
 If there is one or more threads ready, then there can only be \emph{one} thread
 running, namely the one whose current precedence is equal to the maximum of all ready
-threads. We use the set-comprehension to capture both possibilities.
+threads. We use sets to capture both possibilities.
 We can now also conveniently define the set of resources that are locked by a thread in a
 given state.
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm holdents_def}
 \noindent
 The first rule states that a thread can only be created, if it does not yet exists.
 Similarly, the second rule states that a thread can only be terminated if it was
 running and does not lock any resources anymore (this simplifies slightly our model;
-in practice we would expect the operating system releases all held lock of a
+in practice we would expect the operating system releases all locks held by a
 thread that is about to exit). The event @{text Set} can happen
 if the corresponding thread is running.
 \begin{center}
 @{thm[mode=Rule] thread_set[where thread=th]}
 \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
-of course the responsibility of the programmer.  In our formal
+the responsibility of the programmer.  In our formal
-model we just exclude such problematic cases in order to be able to make
+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 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 ommited and the
 responsibility for avoiding problems rests with the programmer.}
 (*<*)
 end
 (*>*)
-section {* Properties for an Implementation\label{implement}*}
+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
 *}
 section {* Conclusion *}
 text {*
-The Priority Inheritance Protocol is a classic textbook algorithm
+The Priority Inheritance Protocol (PIP) is a classic textbook
-used in real-time systems in order to avoid the problem of Priority
+algorithm used in real-time systems in order to avoid the problem of
-Inversion.
+Priority Inversion.  While classic and widely used, PIP does have its faults: for
+example it does not prevent deadlocks where threads have circular
-A clear and simple understanding of the problem at hand is both a
+lock dependencies.
-prerequisite and a byproduct of such an effort, because everything
-has finally be reduced to the very first principle to be checked
+We had two aims in mind with our formalisation
-mechanically.
+of PIP: One is to understand the relevant literature and to make the
+notions in its correctness proof precise so that they can be
-Our formalisation and the one presented
+processed by a theorem prover, because a mechanically checked proof
-in \cite{Wang09} are the only ones that employ Paulson's method for
+avoids the flaws that crept into the informal reasoning by Sha et
-verifying protocols which are \emph{not} security related.
+al.~\cite{Sha90}. We achieved this aim: The correctness of PIP now
+hinges only on the assumptions behind our formal model, which can
-TO DO
+now be debated and potentially be modified. The reasoning, which is
+sometimes quite intricate and tedious, has been checked beyond any
+reasonable doubt by Isabelle. We can confirm that Paulson's
+inductive approach to protocol verification \cite{Paulson98} is
+quite suitable for our formal model and proof. The traditianal
+application area of this approach are security protocols.
+The only other application of Paulson's approach outside this area we know of
+is \cite{Wang09}.
+The second aim is to provide a specification for PIP so that it can
+actually be implemented. Textbooks, like \cite[Section
+5.6.5]{Vahalia96}, explain how to use various implementations of PIP
+and abstractly discuss its properties, but surprisinly lack many
+details for an implementor.  That this is an issue in practice is
+illustrated by the email from Baker we cited in the
+Introduction. The formalisation gives the first author enough data
+to enable his undergraduate students to implement PIP on top of
+PINTOS, an small operating system for teaching purposes.  Given the
+results in Section~\ref{implement}, we also succeeded with this
+aim. A byproduct of our formalisation effort is that nearly all
+design choices for the PIP scheduler are backed up with a proved
+lemma.
 no clue about multi-processor case according to \cite{Steinberg10}
-*}
-text {*
-\bigskip
-The priority inversion phenomenon was first published in
-\cite{Lampson80}.  The two protocols widely used to eliminate
-priority inversion, namely PI (Priority Inheritance) and PCE
-(Priority Ceiling Emulation), were proposed in \cite{Sha90}. PCE is
-less convenient to use because it requires static analysis of
-programs. Therefore, PI is more commonly used in
-practice\cite{locke-july02}. However, as pointed out in the
-literature, the analysis of priority inheritance protocol is quite
-subtle\cite{yodaiken-july02}.  A formal analysis will certainly be
-helpful for us to understand and correctly implement PI. All
-existing formal analysis of PI
-\cite{Jahier09,Wellings07,Faria08} are based on the
-model checking technology. Because of the state explosion problem,
-model check is much like an exhaustive testing of finite models with
-limited size.  The results obtained can not be safely generalized to
-models with arbitrarily large size. Worse still, since model
-checking is fully automatic, it give little insight on why the
-formal model is correct. It is therefore definitely desirable to
-analyze PI using theorem proving, which gives more general results
-as well as deeper insight. And this is the purpose of this paper
-which gives a formal analysis of PI in the interactive theorem
-prover Isabelle using Higher Order Logic (HOL). The formalization
-focuses on on two issues:
 \begin{enumerate}
 \item The correctness of the protocol model itself. A series of desirable properties is
 derived until we are fully convinced that the formal model of PI does
 eliminate priority inversion. And a better understanding of PI is so obtained
 A point never mentioned in literature.
 \item The correctness of the implementation. A series of properties is derived the meaning
 of which can be used as guidelines on how PI can be implemented efficiently and correctly.
 \end{enumerate}
-The rest of the paper is organized as follows: Section \ref{overview} gives an overview
-of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general}
+Contributions
-discusses a series of basic properties of PI. Section \ref{extension} shows formally
-how priority inversion is controlled by PI. Section \ref{implement} gives properties
-which can be used for guidelines of implementation. Section \ref{related} discusses
-related works. Section \ref{conclusion} concludes the whole paper.
-The basic priority inheritance protocol has two problems:
-It does not prevent a deadlock from happening in a program with circular lock dependencies.
-A chain of blocking may be formed; blocking duration can be substantial, though bounded.
-Contributions
 Despite the wide use of Priority Inheritance Protocol in real time operating
 system, it's correctness has never been formally proved and mechanically checked.
 All existing verification are based on model checking technology. Full automatic
 verification gives little help to understand why the protocol is correct.

changeset 314	ccb6c0601614
parent 313	3d154253d5fe
child 315	f05f6aeb32f4