--- a/prio/Paper/Paper.thy Mon Feb 06 12:08:35 2012 +0000
+++ b/prio/Paper/Paper.thy Tue Feb 07 00:50:23 2012 +0000
@@ -6,29 +6,37 @@
open Printer;
show_question_marks_default := false;
*}
+
+notation (latex output)
+ Cons ("_::_" [78,77] 73) and
+ vt ("valid'_state") and
+ runing ("running") and
+ birthtime ("inception") and
+ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+ DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
section {* Introduction *}
text {*
- Many real-time systems need to support processes with priorities and
+ Many real-time systems need to support threads involving priorities and
locking of resources. Locking of resources ensures mutual exclusion
when accessing shared data or devices that cannot be
- preempted. Priorities allow scheduling of processes that need to
+ preempted. Priorities allow scheduling of threads that need to
finish their work within deadlines. Unfortunately, both features
can interact in subtle ways leading to a problem, called
- \emph{Priority Inversion}. Suppose three processes having priorities
- $H$(igh), $M$(edium) and $L$(ow). We would expect that the process
- $H$ blocks any other process with lower priority and itself cannot
- be blocked by any process with lower priority. Alas, in a naive
+ \emph{Priority Inversion}. Suppose three threads having priorities
+ $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
+ $H$ blocks any other thread with lower priority and itself cannot
+ be blocked by any thread with lower priority. Alas, in a naive
implementation of resource looking and priorities this property can
be violated. Even worse, $H$ can be delayed indefinitely by
- processes with lower priorities. For this let $L$ be in the
+ threads with lower priorities. For this let $L$ be in the
possession of a lock for a resource that also $H$ needs. $H$ must
therefore wait for $L$ to exit the critical section and release this
lock. The problem is that $L$ might in turn be blocked by any
- process with priority $M$, and so $H$ sits there potentially waiting
- indefinitely. Since $H$ is blocked by processes with lower
+ thread with priority $M$, and so $H$ sits there potentially waiting
+ indefinitely. Since $H$ is blocked by threads with lower
priorities, the problem is called Priority Inversion. It was first
described in \cite{Lampson80} in the context of the
Mesa programming language designed for concurrent programming.
@@ -36,41 +44,43 @@
If the problem of Priority Inversion is ignored, real-time systems
can become unpredictable and resulting bugs can be hard to diagnose.
The classic example where this happened is the software that
- controlled the Mars Pathfinder mission in 1997
- \cite{Reeves98}. Once the spacecraft landed, the software
- shut down at irregular intervals leading to loss of project time as
- normal operation of the craft could only resume the next day (the
- mission and data already collected were fortunately not lost, because
- of a clever system design). The reason for the shutdowns was that
- the scheduling software fell victim of Priority Inversion: a low
- 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}\footnote{Sha et al.~call it the
- \emph{Basic Priority Inheritance Protocol} \cite{Sha90}.} in the scheduling software.
+ controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
+ Once the spacecraft landed, the software shut down at irregular
+ intervals leading to loss of project time as normal operation of the
+ craft could only resume the next day (the mission and data already
+ collected were fortunately not lost, because of a clever system
+ design). The reason for the shutdowns was that the scheduling
+ software fell victim of Priority Inversion: a low priority thread
+ locking a resource prevented a high priority thread 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}\footnote{Sha et al.~call it the \emph{Basic Priority
+ Inheritance Protocol} \cite{Sha90} and others sometimes call it
+ also \emph{Priority Boosting}.} 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 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
- used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner,
- Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard
- realised for example in libraries for FreeBSD, Solaris and Linux.
+ The idea behind PIP is to let the thread $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 be blocked by threads 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 used
+ in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
+ ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
+ example in libraries for FreeBSD, Solaris and Linux.
- One advantage of PIP is that increasing the priority of a process
+ One advantage of PIP is that increasing the priority of a thread
can be dynamically calculated by the scheduler. This is in contrast
to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
solution to the Priority Inversion problem, which requires static
- analysis of the program in order to prevent Priority Inversion. However, there has
- also been strong criticism against PIP. For instance, PIP cannot
- prevent deadlocks when lock dependencies are circular, and also
- blocking times can be substantial (more than just the duration of a
- critical section). Though, most criticism against PIP centres
- around unreliable implementations and PIP being too complicated and
- too inefficient. For example, Yodaiken writes in \cite{Yodaiken02}:
+ analysis of the program in order to prevent Priority
+ Inversion. However, there has also been strong criticism against
+ PIP. For instance, PIP cannot prevent deadlocks when lock
+ dependencies are circular, and also blocking times can be
+ substantial (more than just the duration of a critical section).
+ Though, most criticism against PIP centres around unreliable
+ implementations and PIP being too complicated and too inefficient.
+ For example, Yodaiken writes in \cite{Yodaiken02}:
\begin{quote}
\it{}``Priority inheritance is neither efficient nor reliable. Implementations
@@ -82,7 +92,7 @@
sections to be preempted. While this might have been a reasonable
solution in 2002, in our modern multiprocessor world, this seems out
of date. The reason is that this precludes other high-priority
- processes from running even when they do not make any use of the locked
+ threads from running even when they do not make any use of the locked
resource.
However, there is clearly a need for investigating correct
@@ -106,50 +116,138 @@
again at PIP from a more abstract level (but still concrete enough
to inform an implementation) and makes PIP an ideal candidate for a
formal verification. One reason, of course, is that the original
- presentation of PIP \cite{Sha90}, despite being informally
+ 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 in the informal proof by Sha et al. They specify in
- \cite{Sha90} that after the process (whose priority has been raised)
+ \cite{Sha90} that after the thread (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 out, this behaviour is too
- simplistic. Consider the case where the low priority process $L$
- locks \emph{two} resources, and two high-priority processes $H$ and
+ implementation of PIP is ``rather straightforward''~\cite{Sha90}.
+ Unfortunately, as Yodaiken points out, this behaviour is too
+ simplistic. Consider the case where the low priority thread $L$
+ locks \emph{two} resources, and two high-priority threads $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'$ (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 in a
- theorem prover for the correctness of a high-level specification of
- PIP is that such issues clearly show up and cannot be overlooked as
- in informal reasoning (since we have to analyse all possible program
- behaviours, i.e.~\emph{traces}, that could possibly happen).
+ the threads that it blocks. The advantage of formalising the
+ correctness of a high-level specification 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 possible behaviours
+ of threads, i.e.~\emph{traces}, that could possibly happen).
There have been earlier formal investigations into PIP, but ...\cite{Faria08}
+
+ vt (valid trace) was introduced earlier, cite
+
+ distributed PIP
*}
section {* Formal Model of the Priority Inheritance Protocol *}
text {*
- Our formal model of PIP is based on Paulson's inductive approach to protocol
- verification \cite{Paulson98}, where the state of the system is modelled as a list of events
- that happened so far. \emph{Events} fall into four categories defined as the datatype
+ We follow the original work by Sha et al.~\cite{Sha90} by modelling
+ first a classical single CPU system where only one \emph{thread} is
+ active at any given moment. We shall discuss later how to lift this
+ restriction. Our model of PIP is based on Paulson's inductive
+ approach to protocol verification \cite{Paulson98}, where the
+ \emph{state} of a system is given by a list of events that
+ happened so far. \emph{Events} fall into four categories defined as
+ the datatype
\begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
- \isacommand{datatype} event & @{text "="} & @{term "Create thread priority"}\\
- & @{text "|"} & @{term "Exit thread"}\\
- & @{text "|"} & @{term "P thread cs"} & {\rm Request of a resource} @{text "cs"} {\rm by} @{text "thread"}\\
- & @{text "|"} & @{term "V thread cs"} & {\rm Release of a resource} @{text "cs"} {\rm by} @{text "thread"}
- \end{tabular}
+ \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
+ \isacommand{datatype} event
+ & @{text "="} & @{term "Create thread priority"}\\
+ & @{text "|"} & @{term "Exit thread"} \\
+ & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the proprity for} @{text thread}\\
+ & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
+ & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ whereby threads, priorities and (critical) resources are represented
+ as natural numbers. As in Paulson's work, we need to define
+ functions that allow one to make some observations about states.
+ One is the ``live'' threads we have seen so far in a state:
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(1)}\\
+ @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(2)[where thread="th"]}\\
+ @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(3)[where thread="th"]}\\
+ @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
+ \end{tabular}}
\end{isabelle}
\noindent
- whereby threads, priorities and resources are represented as natural numbers.
- A \emph{state} is a list of events.
+ Another is that given a thread @{text "th"}, what is the original priority was at
+ its inception.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
+ @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent
+ In this definition we set @{text 0} as the default priority for
+ threads that have not (yet) been created. The last function we need
+ calculates the ``time'', or index, at which a process was created.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{lcl}
+ @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
+ @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
+ @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+ @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
+ \end{tabular}}
+ \end{isabelle}
+
+ \begin{center}
+ threads, original-priority, birth time, precedence.
+ \end{center}
+
+
+
+ resources
+
+ step relation:
+
+ \begin{center}
+ \begin{tabular}{c}
+ @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
+ @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\
+
+ @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
+ @{thm[mode=Rule] thread_V[where thread=th]}\\
+ \end{tabular}
+ \end{center}
+
+ valid state:
+
+ \begin{center}
+ \begin{tabular}{c}
+ @{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm}
+ @{thm[mode=Rule] vt_cons[where cs=step]}
+ \end{tabular}
+ \end{center}
+
To define events, the identifiers of {\em threads},
{\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
@@ -159,25 +257,28 @@
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{conf/fase/JahierHR09,WellingsBSB07,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
+ 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{conf/fase/JahierHR09,WellingsBSB07,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}