# HG changeset patch # User urbanc # Date 1328396174 0 # Node ID c91c2dd0859991546e16b52f33e748868d32d7d4 # Parent 7911439863b00babe9c7ab8d8e028d87382ec837 updated diff -r 7911439863b0 -r c91c2dd08599 prio/Paper/Paper.thy --- 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 diff -r 7911439863b0 -r c91c2dd08599 prio/Paper/document/root.bib --- 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}}, } diff -r 7911439863b0 -r c91c2dd08599 prio/README.txt --- /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: + diff -r 7911439863b0 -r c91c2dd08599 prio/paper.pdf Binary file prio/paper.pdf has changed