--- a/prio/Paper/Paper.thy Mon Feb 13 15:42:45 2012 +0000
+++ b/prio/Paper/Paper.thy Mon Feb 13 19:33:03 2012 +0000
@@ -158,7 +158,7 @@
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.
@@ -384,10 +384,12 @@
\end{isabelle}
\noindent
- The first function is a waiting queue function (that is, it takes a resource @{text "cs"} and returns the
- corresponding list of threads that wait for it), the second is a function that takes
- a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and
- setter methods for such records.
+ The first function is a waiting queue function (that is, it takes a
+ resource @{text "cs"} and returns the corresponding list of threads
+ that lock, respectively wait for, it); the second is a function that
+ 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
@@ -428,7 +430,7 @@
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}\ \ \ \ \ %%%
@@ -512,7 +514,7 @@
@{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.
@@ -537,7 +539,7 @@
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.
@@ -549,8 +551,8 @@
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
- model we just exclude such problematic cases in order to be able to make
+ 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 occurs check in Prolog: In order to say
anything meaningful about unification, one needs to perform an occurs
@@ -886,7 +888,7 @@
(*>*)
-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
@@ -1125,50 +1127,48 @@
section {* Conclusion *}
text {*
- The Priority Inheritance Protocol is a classic textbook algorithm
- used in real-time systems in order to avoid the problem of Priority
- Inversion.
+ The Priority Inheritance Protocol (PIP) is a classic textbook
+ algorithm used in real-time systems in order to avoid the problem of
+ Priority Inversion. While classic and widely used, PIP does have its faults: for
+ example it does not prevent deadlocks where threads have circular
+ lock dependencies.
- A clear and simple understanding of the problem at hand is both a
- prerequisite and a byproduct of such an effort, because everything
- has finally be reduced to the very first principle to be checked
- mechanically.
+ We had two aims in mind with our formalisation
+ of PIP: One is to understand the relevant literature and to make the
+ notions in its correctness proof precise so that they can be
+ processed by a theorem prover, because a mechanically checked proof
+ avoids the flaws that crept into the informal reasoning by Sha et
+ al.~\cite{Sha90}. We achieved this aim: The correctness of PIP now
+ hinges only on the assumptions behind our formal model, which can
+ 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}.
- Our formalisation and the one presented
- in \cite{Wang09} are the only ones that employ Paulson's method for
- verifying protocols which are \emph{not} security related.
+ 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.
- TO DO
+
+
+
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
@@ -1182,21 +1182,8 @@
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}
- 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
+
+ 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.