
diff -r 463bed130705 -r 5113aa1ae69a prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Sun Feb 12 23:25:49 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 00:06:59 2012 +0000
@@ -303,14 +303,15 @@
   where the first stands for a \emph{waiting edge} and the second for a 
   \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 
   datatype for vertices). Given a waiting queue function, a RAG is defined 
-  as
+  as the union of the sets of waiting and holding edges, namely
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cs_depend_def}
   \end{isabelle}
 
   \noindent
-  Given three threads and three resources, an instance of a RAG is as follows:
+  Given three threads and three resources, an instance of a RAG can be pictured 
+  as follows:
 
   \begin{center}
   \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
@@ -336,7 +337,8 @@
 
   \noindent
   The use of relations for representing RAGs allows us to conveniently define
-  the notion of the \emph{dependants} of a thread. This is defined as
+  the notion of the \emph{dependants} of a thread using the transitive closure
+  operation for relations. This gives
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cs_dependents_def}
@@ -346,9 +348,10 @@
   This definition needs to account for all threads that wait for a thread to
   release a resource. This means we need to include threads that transitively
   wait for a resource being released (in the picture above this means the dependants
-  of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, but also @{text "th\<^isub>3"}, 
+  of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"}, 
+  but also @{text "th\<^isub>3"}, 
   which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
-  in turn needs to wait for @{text "th\<^isub>1"} to finish). If there is a circle in a RAG, then clearly
+  in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle in a RAG, then clearly
   we have a deadlock. Therefore when a thread requests a resource,
   we must ensure that the resulting RAG is not circular. 
 
@@ -360,18 +363,19 @@
   \end{isabelle}
 
   \noindent
+  where the dependants of @{text th} are given by the waiting queue function.
   While the precedence @{term prec} of a thread is determined by the programmer 
   (for example when the thread is
-  created), the point of the current precedence is to let scheduler increase this
-  priority, if needed according to PIP. Therefore the current precedence of @{text th} is
+  created), the point of the current precedence is to let the scheduler increase this
+  precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
   given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 
-  processes that are dependants of @{text th}. Since the notion @{term "dependants"} is
+  threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
   defined as the transitive closure of all dependent threads, we deal correctly with the 
-  problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
+  problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
   lowered prematurely.
   
   The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
-  by recursion on the state (a list of events); @{term "schs"} returns a \emph{schedule state}, which 
+  by recursion on the state (a list of events); this function returns a \emph{schedule state}, which 
   we represent as a record consisting of two
   functions:
 
@@ -380,15 +384,16 @@
   \end{isabelle}
 
   \noindent
-  The first function is a waiting queue function (that is it takes a resource @{text "cs"} and returns the
+  The first function is a waiting queue function (that is, it takes a resource @{text "cs"} and returns the
   corresponding list of threads that wait for it), the second is a function that takes
   a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and 
   setter methods for such records.
 
-  In the initial state, the scheduler starts with all resources unlocked (see \eqref{allunlocked}) and the
+  In the initial state, the scheduler starts with all resources unlocked (the corresponding 
+  function is defined in \eqref{allunlocked}) and the
   current precedence of every thread is initialised with @{term "Prc 0 0"}; that means 
   \mbox{@{abbrev initial_cprec}}. Therefore
-  we have
+  we have for the initial state
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -401,8 +406,8 @@
   The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
   we calculate the waiting queue function of the (previous) state @{text s}; 
   this waiting queue function @{text wq} is unchanged in the next schedule state---because
-  none of these events lock or release any resources; 
-  for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function 
+  none of these events lock or release any resource; 
+  for calculating the next @{term "cprec_fun"}, we use @{text wq} and 
   @{term cpreced}. This gives the following three clauses for @{term schs}:
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -420,11 +425,11 @@
   \end{isabelle}
 
   \noindent 
-  More interesting are the cases when a resource, say @{text cs}, is locked or released. In these cases
+  More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
   we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
-  the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th} 
+  the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} 
   appended to the end of that list (remember the head of this list is seen to be in the possession of this
-  resource).
+  resource). This gives the clause
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -440,7 +445,7 @@
   so that the thread that possessed the lock is deleted from the corresponding thread list. For this 
   list transformation, we use
   the auxiliary function @{term release}. A simple version of @{term release} would
-  just delete this thread and return the rest, namely
+  just delete this thread and return the remaining threads, namely
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}lcl}
@@ -463,7 +468,7 @@
   \end{isabelle}
 
   \noindent
-  @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
+  where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
   choice for the next waiting list. It just has to be a list of distinctive threads and
   contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
  
@@ -502,28 +507,24 @@
   \end{isabelle}
 
   \noindent
-  In this definition @{term "f ` S"} stands for the set @{text S} under the image of the 
-  function @{text f}. 
-  Note that in the initial case, that is where the list of events is empty, the set 
+  In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
+  Note that in the initial state, that is where the list of events is empty, the set 
   @{term threads} is empty and therefore there is no thread ready nor a running.
   If there is one or more threads ready, then there can only be \emph{one} thread
   running, namely the one whose current precedence is equal to the maximum of all ready 
   threads. We use the set-comprehension to capture both possibilities.
-  We can now also define the set of resources that are locked by a thread in any
+  We can now also conveniently define the set of resources that are locked by a thread in a
   given state.
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm holdents_def}
   \end{isabelle}
 
-  \noindent
-  These resources are given by the holding edges in the RAG.
-
-  Finally we can define what a \emph{valid state} is in our PIP. For
+  Finally we can define what a \emph{valid state} is in our model of PIP. For
   example we cannot expect to be able to exit a thread, if it was not
-  created yet. These validity constraints are characterised by the
-  inductive predicate @{term "step"}. We give five inference rules
-  relating a state and an event that can happen next.
+  created yet. These validity constraints on states are characterised by the
+  inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
+  for @{term step} relating a state and an event that can happen next.
 
   \begin{center}
   \begin{tabular}{c}
@@ -535,7 +536,9 @@
   \noindent
   The first rule states that a thread can only be created, if it does not yet exists.
   Similarly, the second rule states that a thread can only be terminated if it was
-  running and does not lock any resources anymore (to simplify ). The event @{text Set} can happen
+  running and does not lock any resources anymore (this simplifies slightly our model;
+  in practice we would expect the operating system releases all held lock of a
+  thread that is about to exit). The event @{text Set} can happen
   if the corresponding thread is running. 
 
   \begin{center}
@@ -546,24 +549,27 @@
   If a thread wants to lock a resource, then the thread needs to be
   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.  Here in our formal
+  of course the responsibility of the programmer.  In our formal
   model we just exclude such problematic cases in order to make
   some meaningful statements about PIP.\footnote{This situation is
   similar to the infamous occurs check in Prolog: in order to say
-  anything meaningful about unification, we need to perform an occurs
-  check; but in practice the occurs check is ommited and the
-  responsibility to avoid problems rests with the programmer.}
+  anything meaningful about unification, one needs to perform an occurs
+  check, but in practice the occurs check is ommited and the
+  responsibility for avoiding problems rests with the programmer.}
+ 
+  \begin{center}
+  @{thm[mode=Rule] thread_P[where thread=th]}
+  \end{center}
+ 
+  \noindent
   Similarly, if a thread wants to release a lock on a resource, then
   it must be running and in the possession of that lock. This is
-  formally given by the last two inference rules of @{term step}.
-
+  formally given by the last inference rule of @{term step}.
+ 
   \begin{center}
-  \begin{tabular}{c}
-  @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
-  @{thm[mode=Rule] thread_V[where thread=th]}\\
-  \end{tabular}
+  @{thm[mode=Rule] thread_V[where thread=th]}
   \end{center}
-  
+
   \noindent
   A valid state of PIP can then be conveniently be defined as follows:
 




