
diff -r 41da10da16a5 -r c62db88ab197 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Feb 14 03:26:18 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 14 04:13:15 2012 +0000
@@ -597,26 +597,29 @@
 begin
 (*>*)
 text {* 
-  Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
-  for PIP in terms of the number of critical resources: if there are
+  Sha et al.~state their first correctness criterion for PIP in terms
+  of the number of low-priority threads \cite[Theorem 3]{Sha90}: if
+  there are @{text n} low-priority threads, then a blocked job with
+  high priority can only be blocked @{text n} times.
+  Their second correctness criterion is stated
+  in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are
   @{text m} critical resources, then a blocked job with high priority
-  can only be blocked @{text m} times---that is a \emph{bounded}
-  number of times. This result on its own, strictly speaking, does
+  can only be blocked @{text m} times. Both results on their own, strictly speaking, do
   \emph{not} prevent indefinite, or unbounded, Priority Inversion,
-  because if one low-priority thread does not give up its critical
+  because if a low-priority thread does not give up its critical
   resource (the one the high-priority thread is waiting for), then the
   high-priority thread can never run.  The argument of Sha et al.~is
   that \emph{if} threads release locked resources in a finite amount
   of time, then indefinite Priority Inversion cannot occur---the high-priority
   thread is guaranteed to run eventually. The assumption is that
   programmers always ensure that this is the case.  However, even
-  taking this assumption into account, ther correctness property is
+  taking this assumption into account, their correctness properties are
   \emph{not} true for their version of PIP. As Yodaiken
   \cite{Yodaiken02} pointed out: If a low-priority thread possesses
   locks to two resources for which two high-priority threads are
   waiting for, then lowering the priority prematurely after giving up
   only one lock, can cause indefinite Priority Inversion for one of the
-  high-priority threads, invalidating their bound.
+  high-priority threads, invalidating their two bounds.
 
   Even when fixed, their proof idea does not seem to go through for
   us, because of the way we have set up our formal model of PIP.  The
@@ -628,9 +631,10 @@
   precedence; we show that in every future state (denoted by @{text
   "s' @ s"}) in which @{text th} is still alive, either @{text th} is
   running or it is blocked by a thread that was alive in the state
-  @{text s}. Since in @{text s}, as in every state, the set of alive
+  @{text s} and was in the possession of a lock in @{text s}. Since in @{text s}, as in every state, the set of alive
   threads is finite, @{text th} can only be blocked a finite number of
-  times. We will actually prove a stricter bound below. However, this
+  times. We will actually prove astronger statement where we also provide
+  the current precedence of the blocking thread. However, this
   correctness criterion hinges upon a number of assumptions about the
   states @{text s} and @{text "s' @ s"}, the thread @{text th} and the
   events happening in @{text s'}. We list them next:
@@ -684,15 +688,21 @@
   Given the assumptions about states @{text "s"} and @{text "s' @ s"},
   the thread @{text th} and the events in @{text "s'"},
   if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
-  @{text "th' \<in> threads s"}.
+  @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 
+  @{term "cp (s' @ s) th' = prec th s"}.
   \end{theorem}
 
   \noindent
   This theorem ensures that the thread @{text th}, which has the
   highest precedence in the state @{text s}, can only be blocked in
   the state @{text "s' @ s"} by a thread @{text th'} that already
-  existed in @{text s}. As we shall see shortly, that means by only
-  finitely many threads. Like in the argument by Sha et al.~this
+  existed in @{text s} and requested or had a lock on at least 
+  one resource---that means the thread was not \emph{detached} in @{text s}. 
+  As we shall see shortly, that means there are only finitely 
+  many threads that can block @{text th} and then need to run
+  with the same current precedence as @{text th}.
+
+  Like in the argument by Sha et al.~our
   finite bound does not guarantee absence of indefinite Priority
   Inversion. For this we further have to assume that every thread
   gives up its resources after a finite amount of time. We found that
@@ -701,6 +711,8 @@
   program threads in such a benign manner (in addition to causeing no 
   circularity in the @{text RAG}). In this detail, we do not
   make any progress in comparison with the work by Sha et al.
+  However, we are able to combine their two separate bounds into a
+  single theorem. 
 
   In what follows we will describe properties of PIP that allow us to prove 
   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
@@ -751,9 +763,7 @@
   The last two properties establish that every thread in a @{text "RAG"}
   (either holding or waiting for a resource) is a live thread.
 
-  To state the key lemma in our proof, it will be convenient to introduce the notion
-  of a \emph{detached} thread in a state, that is one which does not hold any
-  critical resource nor requests one. 
+  The key lemma in our proof of Theorem~\ref{mainthm} is as follows:
 
   \begin{lemma}\label{mainlem}
   Given the assumptions about states @{text "s"} and @{text "s' @ s"},
@@ -788,27 +798,19 @@
   one step further, @{text "th'"} still cannot hold any resource. The situation will 
   not change in further extensions as long as @{text "th"} holds the highest precedence.
 
-  From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that
+  From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be 
+  blocked by a thread @{text th'} that
   held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
   that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the 
   precedence of @{text th} in @{text "s"}.
-
-  \begin{theorem}
-  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
-  the thread @{text th} and the events in @{text "s'"}, if
-  @{term "th' \<in> running (s' @ s)"}, @{text "th' \<noteq> th"}, then
-  @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 
-  @{term "cp (s' @ s) th' = prec th s"}.
-  \end{theorem}
-
-  \noindent
   We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
   This theorem gives a stricter bound on the processes that can block @{text th}:
   only threads that were alive in state @{text s} and moreover held a resource.
-  Finally, the theorem establishes that the blocking threads have the
+  This means our bound is in terms of both---alive threads in state @{text s}
+  and number of critical resources. Finally, the theorem establishes that the blocking threads have the
   current precedence raised to the precedence of @{text th}.
 
-  We can furthermore prove that no deadlock exists in the state @{text "s' @ s"}
+  We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"}
   by showing that @{text "running (s' @ s)"} is not empty.
 
   \begin{lemma}
@@ -1243,8 +1245,9 @@
   code with a few apply-scripts interspersed. The formal model of PIP
   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
   definitions and proofs took 770 lines of code. The properties relevant
-  for an implementation took 2000 lines.  %%Our code can be downloaded from
-  %%...
+  for an implementation took 2000 lines. The code of our formalisation 
+  can be downloaded from\\
+  \url{http://www.dcs.kcl.ac.uk/staff/urbanc/pip.html}.
 
   \bibliographystyle{plain}
   \bibliography{root}




