# HG changeset patch # User urbanc # Date 1329161583 0 # Node ID ccb6c06016144a67c5294a32409f4f00cf1a42f5 # Parent 3d154253d5fef00c0fa9b6a7dce3eecdeeb1268a some parts of the conclusion diff -r 3d154253d5fe -r ccb6c0601614 prio/Paper/Paper.thy --- 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. diff -r 3d154253d5fe -r ccb6c0601614 prio/paper.pdf Binary file prio/paper.pdf has changed