# HG changeset patch # User urbanc # Date 1329166622 0 # Node ID f05f6aeb32f4e59471c3c6a041d3355d50259e6f # Parent ccb6c06016144a67c5294a32409f4f00cf1a42f5 more conclusion diff -r ccb6c0601614 -r f05f6aeb32f4 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Mon Feb 13 19:33:03 2012 +0000 +++ b/prio/Paper/Paper.thy Mon Feb 13 20:57:02 2012 +0000 @@ -1128,74 +1128,74 @@ text {* 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. + algorithm used in real-time operating systems in order to avoid the problem of + Priority Inversion. Although classic and widely used, PIP does have + its faults: for example it does not prevent deadlocks where threads + have circular lock dependencies. - 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 + We had two aims in mind with our formalisation of PIP: One is to + make the notions in the correctness proof by Sha et al.~\cite{Sha90} + precise so that they can be processed by a theorem prover, because a + mechanically checked proof avoids the flaws that crept into their + informal reasoning. We achieved this aim: 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. 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}. + reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's + inductive method to 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}. - 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 + The second aim is to provide a specification for actually + implementing PIP. Textbooks, like \cite[Section 5.6.5]{Vahalia96}, + explain how to use various implementations of PIP and abstractly + discuss its properties, but surprisingly lack most details for a + programmer. That this is an issue in practice is illustrated by the + email from Baker we cited in the Introduction. We achieved also this + aim: The formalisation gives the first author enough data to enable + his undergraduate students to implement as part of their OS course + PIP on top of PINTOS, a small operating system for teaching + purposes. A byproduct of our formalisation effort is that nearly all design choices for the PIP scheduler are backed up with a proved - lemma. + lemma. We were also able to prove the property that the choice of + the next thread taking over a lock is irrelevant for the correctness + of PIP. Earlier model checking techniques + \cite{Faria08,Jahier09,Wellings07} were not able to provided this + kind of ``deep understanding'' into PIP. + + 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 nowadays any relevance beyond teaching. + + The work in this paper only deals with single CPU configurations. The + "one CPU" assumption is essential for our formalisation, because the + main lemma fails in multi-CPU configuration. The lemma says that any + runing thead must be the one with the highest prioirty or already held + some resource when the highest priority thread was initiated. When + there are multiple CPUs, it may well be the case that a threads did + not hold any resource when the highest priority thread was initiated, + but that thread still runs after that moment on a separate CPU. In + this way, the main lemma does not hold anymore. - - + There are some works deals with priority inversion in multi-CPU + configurations[???], but none of them have given a formal correctness + proof. The extension of our formal proof to deal with multi-CPU + configurations is not obvious. One possibility, as suggested in paper + [???], is change our formal model (the defiintion of "schs") to give + the released resource to the thread with the highest prioirty. In this + way, indefinite prioirty inversion can be avoided, but for a quite + different reason from the one formalized in this paper (because the + "mail lemma" will be different). This means a formal correctness proof + for milt-CPU configuration would be quite different from the one given + in this paper. The solution of prioirty inversion problem in mult-CPU + configurations is a different problem which needs different solutions + which is outside the scope of this paper. no clue about multi-processor case according to \cite{Steinberg10} - - \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 - in due course. For example, we find through formalization that the choice of - next thread to take hold when a - resource is released is irrelevant for the very basic property of PI to hold. - 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} - - 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. - And results such obtained only apply to models of limited size. - This paper presents a formal verification based on theorem proving. - Machine checked formal proof does help to get deeper understanding. We found - the fact which is not mentioned in the literature, that the choice of next - thread to take over when an critical resource is release does not affect the correctness - of the protocol. The paper also shows how formal proof can help to construct - correct and efficient implementation.\bigskip *} @@ -1248,13 +1248,6 @@ Priority Inheritance is just such a byproduct. *} -(* -section {* Formal model of Priority Inheritance \label{model} *} -text {* - \input{../../generated/PrioGDef} -*} -*) - section {* General properties of Priority Inheritance \label{general} *} text {* @@ -1426,30 +1419,7 @@ section {* Conclusions \label{conclusion} *} text {* - The work in this paper only deals with single CPU configurations. The - "one CPU" assumption is essential for our formalisation, because the - main lemma fails in multi-CPU configuration. The lemma says that any - runing thead must be the one with the highest prioirty or already held - some resource when the highest priority thread was initiated. When - there are multiple CPUs, it may well be the case that a threads did - not hold any resource when the highest priority thread was initiated, - but that thread still runs after that moment on a separate CPU. In - this way, the main lemma does not hold anymore. - - - There are some works deals with priority inversion in multi-CPU - configurations[???], but none of them have given a formal correctness - proof. The extension of our formal proof to deal with multi-CPU - configurations is not obvious. One possibility, as suggested in paper - [???], is change our formal model (the defiintion of "schs") to give - the released resource to the thread with the highest prioirty. In this - way, indefinite prioirty inversion can be avoided, but for a quite - different reason from the one formalized in this paper (because the - "mail lemma" will be different). This means a formal correctness proof - for milt-CPU configuration would be quite different from the one given - in this paper. The solution of prioirty inversion problem in mult-CPU - configurations is a different problem which needs different solutions - which is outside the scope of this paper. + *} diff -r ccb6c0601614 -r f05f6aeb32f4 prio/paper.pdf Binary file prio/paper.pdf has changed