diff -r 5920649c5a22 -r 572f202659ff prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Feb 07 01:10:34 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed Feb 08 16:35:49 2012 +0000
@@ -11,8 +11,9 @@
   Cons ("_::_" [78,77] 73) and
   vt ("valid'_state") and
   runing ("running") and
-  birthtime ("inception") and
+  birthtime ("last'_set") and
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+  Prc ("'(_, _')") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -55,11 +56,11 @@
   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.
+  Inheritance Protocol} \cite{Sha90} and others sometimes also call it
+  \emph{Priority Boosting}.} in the scheduling software.
 
   The idea behind PIP is to let the thread $L$ temporarily inherit
-  the high priority from $H$ until $L$ leaves the critical section by
+  the high priority from $H$ until $L$ leaves the critical section
   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
@@ -89,13 +90,10 @@
 
   \noindent
   He suggests to avoid PIP altogether by not allowing critical
-  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 
-  threads from running even when they do not make any use of the locked
-  resource.
+  sections to be preempted. Unfortunately, this solution does not
+  help in real-time systems with low latency \emph{requirements}.
 
-  However, there is clearly a need for investigating correct
+  In our opinion, there is clearly a need for investigating correct
   algorithms for PIP. A few specifications for PIP exist (in English)
   and also a few high-level descriptions of implementations (e.g.~in
   the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
@@ -114,7 +112,7 @@
   \noindent
   The criticism by Yodaiken, Baker and others suggests to us to look
   again at PIP from a more abstract level (but still concrete enough
-  to inform an implementation) and makes PIP an ideal candidate for a
+  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
   ``proved'' correct, is actually \emph{flawed}. 
@@ -143,36 +141,43 @@
   vt (valid trace) was introduced earlier, cite
   
   distributed PIP
+
+  Paulson's method has not been used outside security field, except
+  work by Zhang et al.
+
+  no clue about multi-processor case according to \cite{Steinberg10} 
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}
 
 text {*
-  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
+  The Priority Inheritance Protocol, short PIP, is a scheduling
+  algorithm for a single-processor system.\footnote{We shall come back
+  later to the case of PIP on multi-processor systems.} 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 five categories defined as the datatype
 
   \begin{isabelle}\ \ \ \ \ %%%
   \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 "Set thread priority"} & {\rm reset of the priority 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:
+  whereby threads, priorities and (critical) resources are represented
+  as natural numbers. The event @{term Set} models the situation that
+  a thread obtains a new priority given by the programmer or
+  user (for example via the {\tt nice} utility under UNIX).  As in Paulson's work, we
+  need to define functions that allow one to make some observations
+  about states.  One, called @{term threads}, calculates the set of
+  ``live'' threads that we have seen so far in a state:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -187,8 +192,7 @@
   \end{isabelle}
 
   \noindent
-  Another is that given a thread @{text "th"}, what is the original priority was at 
-  its inception. 
+  Another calculates the priority for a thread @{text "th"}, defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -219,10 +223,42 @@
   @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
   \end{tabular}}
   \end{isabelle}
+
+  \footnote{Can Precedence be the real birth-time / or must be time precedence last set?}
+
+  \noindent
+  A \emph{precedence} of a thread @{text th} in a state @{text s} is a pair of
+  natural numbers defined as
   
-  \begin{center}
-  threads, original-priority, birth time, precedence.
-  \end{center}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (rhs) preced_def[where thread="th"]}
+  \end{isabelle}
+
+  \noindent
+  The point of precedences is to schedule threads not according to priorities (what should
+  we do in case two threads have the same priority), but according to precedences. 
+  Precedences allow us to always discriminate two threads with equal priority by 
+  tacking into account the time when the priority was last set. We order precedences so 
+  that threads with the same priority get a higher precedence if their priority has been 
+  set earlier, since for such threads it is more urgent to finish. In an impementation
+  this choice would translate to a quite natural a FIFO-scheduling of processes with 
+  the same priority.
+
+  Next, we introduce the concept of \emph{waiting queues}. They are
+  lists of threads associated with every resource. The first thread in
+  this list is chosen to be in the one that is in possession of the
+  ``lock'' of the corresponding resource. We model waiting queues as
+  functions, below abbreviated as @{text wq}, taking a resource as
+  argument and returning a list of threads.  This allows us to define
+  when a thread \emph{holds}, respectively \emph{waits}, for a
+  resource @{text cs}.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm cs_holding_def[where thread="th"]}\\
+  @{thm cs_waiting_def[where thread="th"]}
+  \end{tabular}
+  \end{isabelle}
 
 
 
@@ -937,6 +973,34 @@
 
 section {* Conclusions \label{conclusion} *}
 
+text {*
+  The work in this paper only deals with single CPU configurations. The
+  "one CPU" assumption is essential for our formalisation, because the
+  main lemma fails in multi-CPU configuration. The lemma says that any
+  runing thead must be the one with the highest prioirty or already held
+  some resource when the highest priority thread was initiated. When
+  there are multiple CPUs, it may well be the case that a threads did
+  not hold any resource when the highest priority thread was initiated,
+  but that thread still runs after that moment on a separate CPU. In
+  this way, the main lemma does not hold anymore.
+
+
+  There are some works deals with priority inversion in multi-CPU
+  configurations[???], but none of them have given a formal correctness
+  proof. The extension of our formal proof to deal with multi-CPU
+  configurations is not obvious. One possibility, as suggested in paper
+  [???], is change our formal model (the defiintion of "schs") to give
+  the released resource to the thread with the highest prioirty. In this
+  way, indefinite prioirty inversion can be avoided, but for a quite
+  different reason from the one formalized in this paper (because the
+  "mail lemma" will be different). This means a formal correctness proof
+  for milt-CPU configuration would be quite different from the one given
+  in this paper. The solution of prioirty inversion problem in mult-CPU
+  configurations is a different problem which needs different solutions
+  which is outside the scope of this paper.
+
+*}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file