--- a/prio/Paper/Paper.thy Sun Feb 12 15:12:50 2012 +0000
+++ b/prio/Paper/Paper.thy Sun Feb 12 23:20:06 2012 +0000
@@ -103,7 +103,8 @@
\noindent
He suggests to avoid PIP altogether by not allowing critical
sections to be preempted. Unfortunately, this solution does not
- help in real-time systems with low latency \emph{requirements}.
+ help in real-time systems with hard deadlines for high-priority
+ threads.
In our opinion, there is clearly a need for investigating correct
algorithms for PIP. A few specifications for PIP exist (in English)
@@ -150,38 +151,16 @@
\noindent
{\bf Contributions:} There have been earlier formal investigations
- into PIP \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08}, but they
- are using model checking technology. As far as we are aware, this is
- the first formalised proof for the correctness of PIP. In contrast
- to model checking, our formalisation provides insight into why PIP
- is correct and allows us to prove stronger properties. For this Isar
- and Isabelle/HOL is an attractive tool for exploring definitions and
- keeping proofs consistent.
-
- For example, we find through formalization that the choice of next
- thread to take a lock when a resource is released is irrelevant for
- the very basic property of PIP to hold.
-
- 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.
-
- vt (valid trace) was introduced earlier, cite
-
-
- Paulson's method has not been used outside security field, except
- work by Zhang et al.
-
- How did Sha et al prove it....they did not use Paulson's method.
+ 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; an 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, inform an
+ 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.
*}
section {* Formal Model of the Priority Inheritance Protocol *}
@@ -528,7 +507,7 @@
@{term threads} is empty and therefore there is no thread ready nor a 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 possibilites.
+ threads. We use the set-comprehension to capture both possibilities.
We can now also define the set of resources that are locked by a thread in any
given state.
@@ -539,10 +518,11 @@
\noindent
These resources are given by the holding edges in the RAG.
- Finally we can define what a \emph{valid state} is in our PIP. For example we cannot exptect to
- be able to exit a thread, if it was not created yet. These validity constraints
- are characterised by the inductive predicate @{term "step"}. We give five
- inference rules relating a state and an event that can happen next.
+ Finally we can define what a \emph{valid state} is in our PIP. For
+ example we cannot expect to be able to exit a thread, if it was not
+ created yet. These validity constraints are characterised by the
+ inductive predicate @{term "step"}. We give five inference rules
+ relating a state and an event that can happen next.
\begin{center}
\begin{tabular}{c}
@@ -622,9 +602,23 @@
@{thm highest}.
\item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
@{thm preced_th}.
+
+ \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
+ \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
+ its precedence can not be higher than @{term "th"}, therefore
+ @{term "th"} remain to be the one with the highest precedence
+ (@{text "create_low"}):
+ @{thm [display] create_low}
+ \item Any adjustment of priority in
+ @{term "t"} does not happen to @{term "th"} and
+ the priority set is no higher than @{term "prio"}, therefore
+ @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
+ @{thm [display] set_diff_low}
+ \item Since we are investigating what happens to @{term "th"}, it is assumed
+ @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
+ @{thm [display] exit_diff}
\end{enumerate}
-
\begin{lemma}
@{thm[mode=IfThen] moment_blocked}
\end{lemma}
@@ -633,6 +627,9 @@
@{thm[mode=IfThen] runing_inversion_2}
\end{theorem}
+ \begin{theorem}
+ @{thm[mode=IfThen] runing_inversion_3}
+ \end{theorem}
@@ -660,6 +657,10 @@
has finally be reduced to the very first principle to be checked
mechanically.
+ 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.
+
TO DO
no clue about multi-processor case according to \cite{Steinberg10}
@@ -679,7 +680,7 @@
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{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the
+ \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
@@ -1038,7 +1039,7 @@
Section 5.6.5 of \cite{Vahalia96}, the implementation of Priority Inheritance in Solaris
uses sophisticated linking data structure. Except discussing two scenarios to show how
the data structure should be manipulated, a lot of details of the implementation are missing.
- In \cite{Faria08,conf/fase/JahierHR09,WellingsBSB07} the protocol is described formally
+ In \cite{Faria08,Jahier09,Wellings07} the protocol is described formally
using different notations, but little information is given on how this protocol can be
implemented efficiently, especially there is no information on how these data structure
should be manipulated.
@@ -1307,7 +1308,7 @@
text {*
\begin{enumerate}
\item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}
- \cite{WellingsBSB07} models and verifies the combination of Priority Inheritance (PI) and
+ \cite{Wellings07} models and verifies the combination of Priority Inheritance (PI) and
Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine
using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed
formal model of combined PI and PCE is given, the number of properties is quite
@@ -1320,7 +1321,7 @@
\cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown
for PI using model checking. The limitation of model checking is intrinsic to the work.
\item {\em Synchronous modeling and validation of priority inheritance schedulers}
- \cite{conf/fase/JahierHR09}. Gives a formal model
+ \cite{Jahier09}. Gives a formal model
of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked
several properties using model checking. The number of properties shown there is
less than here and the scale is also limited by the model checking technique.
--- a/prio/Paper/document/root.bib Sun Feb 12 15:12:50 2012 +0000
+++ b/prio/Paper/document/root.bib Sun Feb 12 23:20:06 2012 +0000
@@ -1,10 +1,13 @@
-@MISC{Yodaiken02,
+
+
+@TechReport{Yodaiken02,
author = {V.~Yodaiken},
title = {{A}gainst {P}riority {I}nheritance},
- year = {2002},
- howpublished = {\url{http://www.linuxfordevices.com/files/misc/yodaiken-july02.pdf}},
+ institution = {Finite State Machine Labs (FSMLabs)},
+ year = {2004}
}
+
@Book{Vahalia96,
author = {U.~Vahalia},
title = {{UNIX} {I}nternals: {T}he {N}ew {F}rontiers},
@@ -43,12 +46,23 @@
year = "1980"
}
-@MISC{Faria08,
+@inproceedings{Wang09,
+ author = {J.~Wang and H.~Yang and X.~Zhang},
+ title = {{L}iveness {R}easoning with {I}sabelle/{HOL}},
+ booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in
+ Higher Order Logics (TPHOLs)},
+ year = {2009},
+ pages = {485--499},
+ volume = {5674},
+ series = {LNCS}
+}
+
+@PhdThesis{Faria08,
author = {J.~M.~S.~Faria},
title = {{F}ormal {D}evelopment of {S}olutions for {R}eal-{T}ime {O}perating {S}ystems
with {TLA+/TLC}},
- year = {2008},
- howpublished = {\url{http://repositorio-aberto.up.pt/bitstream/10216/11466/2/Texto%20integral.pdf}},
+ school = {University of Porto},
+ year = {2008}
}
@@ -92,38 +106,27 @@
\url{http://www.sdl.sri.com/dsa/publis/prio-ceiling.html}",
}
-@InProceedings{conf/fase/JahierHR09,
- title = "Synchronous Modeling and Validation of Priority
- Inheritance Schedulers",
- author = "E. Jahier and B. Halbwachs and P.
- Raymond",
- bibdate = "2009-04-01",
- bibsource = "DBLP,
- http://dblp.uni-trier.de/db/conf/fase/fase2009.html#JahierHR09",
- booktitle = "FASE",
- booktitle = "Fundamental Approaches to Software Engineering, 12th
- International Conference, {FASE} 2009, Held as Part of
- the Joint European Conferences on Theory and Practice
- of Software, {ETAPS} 2009, York, {UK}, March 22-29,
- 2009. Proceedings",
- publisher = "Springer",
+@InProceedings{Jahier09,
+ title = "{S}ynchronous {M}odeling and {V}alidation of {P}riority
+ {I}nheritance {S}chedulers",
+ author = "E.~Jahier and B.~Halbwachs and P.~Raymond",
+ booktitle = "Proc.~of the 12th International Conference on Fundamental
+ Approaches to Software Engineering (FASE)",
year = "2009",
volume = "5503",
- editor = "Marsha Chechik and Martin Wirsing",
- ISBN = "978-3-642-00592-3",
- pages = "140--154",
- series = "Lecture Notes in Computer Science",
- URL = "http://dx.doi.org/10.1007/978-3-642-00593-0",
+ series = "LNCS",
+ pages = "140--154"
}
-@InProceedings{WellingsBSB07,
- title = "Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java",
- author = "A. J. Wellings and A. Burns and O. M. Santos and B. M. Brosgol",
+@InProceedings{Wellings07,
+ title = "{I}ntegrating {P}riority {I}nheritance {A}lgorithms in the {R}eal-{T}ime
+ {S}pecification for {J}ava",
+ author = "A.~Wellings and A.~Burns and O.~M.~Santos and B.~M.~Brosgol",
publisher = "IEEE Computer Society",
year = "2007",
- booktitle = "Proceedings of the 10th IEEE International Symposium on Object
- and Component-Oriented Real-Time Distributed Computing",
- pages = "115--123",
+ booktitle = "Proc.~of the 10th IEEE International Symposium on Object
+ and Component-Oriented Real-Time Distributed Computing (ISORC)",
+ pages = "115--123"
}
@Article{Wang:2002:SGP,
Binary file prio/paper.pdf has changed