--- a/prio/Paper/Paper.thy Sat Feb 04 00:14:41 2012 +0000
+++ b/prio/Paper/Paper.thy Sat Feb 04 22:56:14 2012 +0000
@@ -46,12 +46,13 @@
priority task locking a resource prevented a high priority process
from running in time leading to a system reset. Once the problem was found,
it was rectified by enabling the \emph{Priority Inheritance Protocol}
- (PIP) \cite{Sha90} in the scheduling software.
+ (PIP) \cite{Sha90}\footnote{Sha et al.~call it the
+ \emph{Basic Priority Inheritance Protocol}.} in the scheduling software.
The idea behind PIP is to let the process $L$ temporarily
inherit the high priority from $H$ until $L$ leaves the critical
section by unlocking the resource. This solves the problem of $H$
- having to wait indefinitely, because $L$ cannot, for example, be
+ having to wait indefinitely, because $L$ cannot be
blocked by processes having priority $M$. While a few other
solutions exist for the Priority Inversion problem, PIP is one that is widely deployed
and implemented. This includes VxWorks (a proprietary real-time OS
@@ -107,9 +108,9 @@
formal verification. One reason, of course, is that the original
presentation of PIP \cite{Sha90}, despite being informally
``proved'' correct, is actually \emph{flawed}. Yodaiken
- \cite{Yodaiken02} points to a subtlety that had been overlooked by
- Sha et al. They specify in \cite{Sha90} that after the process whose
- priority has been raised completes its critical section and releases
+ \cite{Yodaiken02} points to a subtlety that had been overlooked in
+ the informal proof by Sha et al. They specify in \cite{Sha90} that after the process (whose
+ priority has been raised) completes its critical section and releases
the lock, it ``returns to its original priority level.'' This leads
them to believe that an implementation of PIP is ``rather
straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed
@@ -117,35 +118,32 @@
low priority process $L$ locks \emph{two} resources, and two
high-priority processes $H$ and $H'$ each wait for one of
them. If $L$ then releases one resource so that $H$, say, can
- proceed, then we still have Priority Inversion with $H'$. The correct
- behaviour for $L$
- is to revert to the highest remaining priority of processes which it
- blocks. The advantage of a formalisation of PIP in a theorem prover
- is that such issues clearly show up and cannot be overlooked as in
- informal reasoning.
+ proceed, then we still have Priority Inversion with $H'$ (which waits for
+ the other resource). The correct behaviour for $L$
+ is to revert to the highest remaining priority of processes that it
+ blocks. The advantage of a formalisation of the correctness of PIP
+ in a theorem prover is that such issues clearly show up and cannot
+ be overlooked as in informal reasoning (since we have to analyse all
+ \emph{traces} that could possibly happen).
There have been earlier formal investigations into PIP, but ...\cite{Faria08}
+*}
- \bigskip
- Priority Inversion problem has been known since 1980
- \cite{Lampson80}, but Sha et al.~give the first
- thorough analysis and present an informal correctness proof for PIP
- .\footnote{Sha et al.~call it the
- \emph{Basic Priority Inheritance Protocol}.}
+section {* Preliminaries *}
- POSIX.4: programming for the real world (Google eBook)
+text {*
+ Our formal model of PIP is based on Paulson's inductive approach to protocol
+ verification, where the state of the system is modelled as a list of events
+ that happened so far. \emph{Events} will use
- However, there are further subtleties: just lowering the priority
- of the process $L$ to its low priority, as proposed in ???, is
- incorrect.\bigskip
-
-
+ To define events, the identifiers of {\em threads},
+ {\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
+ need to be represented. All three are represetned using standard
+ Isabelle/HOL type @{typ "nat"}:
+*}
- very little on implementations, not to mention implementations informed by
- formal correctness proofs.
-
-
-
+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
--- a/prio/Paper/document/root.bib Sat Feb 04 00:14:41 2012 +0000
+++ b/prio/Paper/document/root.bib Sat Feb 04 22:56:14 2012 +0000
@@ -1,12 +1,12 @@
@MISC{Yodaiken02,
- author = {V.~Yodaiken},
- title = {{A}gainst {P}riority {I}nheritance},
- year = {2002},
- howpublished={\url{http://www.linuxfordevices.com/files/misc/yodaiken-july02.pdf}},
+ author = {V.~Yodaiken},
+ title = {{A}gainst {P}riority {I}nheritance},
+ year = {2002},
+ howpublished = {\url{http://www.linuxfordevices.com/files/misc/yodaiken-july02.pdf}},
}
@Book{Vahalia96,
- author = {U.~Vahalia},
+ author = {U.~Vahalia},
title = {{UNIX} {I}nternals: {T}he {N}ew {F}rontiers},
publisher = {Prentice-Hall},
year = {1996}
@@ -44,10 +44,11 @@
}
@MISC{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}},
+ 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}},
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/README.txt Sat Feb 04 22:56:14 2012 +0000
@@ -0,0 +1,2 @@
+Overview of files:
+
Binary file prio/paper.pdf has changed