
diff -r e44c4055d430 -r 4d93486cb302 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 13 05:41:53 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 10:44:42 2012 +0000
@@ -157,7 +157,7 @@
   knowledge the first one; the earlier informal proof by Sha et
   al.~\cite{Sha90} is flawed).  In contrast to model checking, our
   formalisation provides insight into why PIP is correct and allows us
-  to prove stronger properties that, as we will show, inform an
+  to prove stronger properties that, as we will show, can inform an
   implementation.  For example, we found by ``playing'' with the formalisation
   that the choice of the next thread to take over a lock when a
   resource is released is irrelevant for PIP being correct. Something
@@ -550,11 +550,11 @@
   running and also we have to make sure that the resource lock does
   not lead to a cycle in the RAG. In practice, ensuring the latter is
   of course the responsibility of the programmer.  In our formal
-  model we just exclude such problematic cases in order to make
+  model we just exclude such problematic cases in order to be able to make
   some meaningful statements about PIP.\footnote{This situation is
-  similar to the infamous occurs check in Prolog: in order to say
+  similar to the infamous occurs check in Prolog: In order to say
   anything meaningful about unification, one needs to perform an occurs
-  check, but in practice the occurs check is ommited and the
+  check. But in practice the occurs check is ommited and the
   responsibility for avoiding problems rests with the programmer.}
  
   \begin{center}
@@ -585,7 +585,7 @@
   properties that show our model of PIP is correct.
 *}
 
-section {* Correctness Proof *}
+section {* The Correctness Proof *}
 
 (*<*)
 context extend_highest_gen
@@ -596,27 +596,27 @@
 thm highest_gen_def
 (*>*)
 text {* 
-  Sha et al.~\cite{Sha90} state their correctness criterion of PIP in terms
+  Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion for PIP in terms
   of the number of critical resources: if there are @{text m} critical
   resources, then a blocked job can only be blocked @{text m} times---that is
   a bounded number of times.
   For their version of PIP, this property is \emph{not} true (as pointed out by 
   Yodaiken \cite{Yodaiken02}) as a high-priority thread can be
   blocked an unbounded number of times by creating medium-priority
-  threads that block a thread locking a critical resource and having 
-  a too low priority. In the way we have set up our formal model of PIP, 
+  threads that block a thread, which in turn locks a critical resource and has
+  too low priority to make progress. In the way we have set up our formal model of PIP, 
   their proof idea, even when fixed, does not seem to go through.
 
   The idea behind our correctness criterion of PIP is as follows: for all states
   @{text s}, we know the corresponding thread @{text th} with the highest precedence;
   we show that in every future state (denoted by @{text "s' @ s"}) in which
-  @{text th} is still active, either @{text th} is running or it is blocked by a 
-  thread that was active in the state @{text s}. Since in @{text s}, as in every 
-  state, the set of active threads is finite, @{text th} can only be blocked a
-  finite number of times. We will actually prove a stricter bound. However,
-  this correctness criterion hinges on a number of assumptions about the states
+  @{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 threads is finite, @{text th} can only be blocked a
+  finite number of times. We will actually prove a stricter bound below. 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.
+  in @{text s'}. We list them next:
 
   \begin{quote}
   {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 
@@ -631,9 +631,9 @@
   \end{quote}
 
   \begin{quote}
-  {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be active in @{text s} and 
-  has the highest precedence of all active threads in @{text s}. Furthermore the
-  priority of @{text th} is @{text prio}.
+  {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and 
+  has the highest precedence of all alive threads in @{text s}. Furthermore the
+  priority of @{text th} is @{text prio} (we need this in the next assumptions).
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
   @{term "th \<in> threads s"}\\
@@ -648,11 +648,12 @@
   be blocked indefinitely. Of course this can happen if threads with higher priority
   than @{text th} are continously created in @{text s'}. Therefore we have to assume that  
   events in @{text s'} can only create (respectively set) threads with equal or lower 
-  priority than @{text prio} of the thread @{text th}. We also have to assume that @{text th} does
-  not get ``exited'' in @{text "s'"}.
+  priority than @{text prio} of @{text th}. We also need to assume that the
+  priority of @{text "th"} does not get reset and also that @{text th} does
+  not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
-  {If}~~@{text "Create _ prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
+  {If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
   {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
   {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
   \end{tabular}
@@ -660,7 +661,7 @@
   \end{quote}
 
   \noindent
-  Under these assumptions we will prove the following property:
+  Under these assumptions we will prove the following correctness property:
 
   \begin{theorem}\label{mainthm}
   Given the assumptions about states @{text "s"} and @{text "s' @ s"},
@@ -674,7 +675,7 @@
   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. Consequently, indefinite wait of
-  @{text th}---whcih is Priority Inversion---cannot occur.
+  @{text th}---which would be Priority Inversion---cannot occur.
 
   In what follows we will describe properties of PIP that allow us to prove 
   Theorem~\ref{mainthm}. It is relatively easily to see that
@@ -700,10 +701,19 @@
 
   \noindent
   The first one states that every waiting thread can only wait for a single
-  resource (because it gets suspended after requesting that resource), and
-  the second that every resource can only be held by a single thread. The
-  third property establishes that in every given valid state, there is
-  at most one running thread.
+  resource (because it gets suspended after requesting that resource and having
+  to wait for it); the second that every resource can only be held by a single thread; 
+  the third property establishes that in every given valid state, there is
+  at most one running thread. We can also show the following properties 
+  about the RAG in @{text "s"}.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  %@{thm[mode=IfThen] }\\
+  %@{thm[mode=IfThen] }\\
+  %@{thm[mode=IfThen] }
+  \end{tabular}
+  \end{isabelle}
 
   TODO
 




