diff -r 7d2bab099b89 -r d296cb127fcb prio/Paper/Paper.thy
--- 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}