
diff -r 8e4a5fff2eda -r 2c8dcf010567 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Sat Feb 11 10:09:39 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 11 12:29:52 2012 +0000
@@ -248,7 +248,7 @@
   The point of precedences is to schedule threads not according to priorities (because what should
   we do in case two threads have the same priority), but according to precedences. 
   Precedences allow us to always discriminate between two threads with equal priority by 
-  tacking into account the time when the priority was last set. We order precedences so 
+  taking 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 their work. In an implementation
   this choice would translate to a quite natural FIFO-scheduling of processes with 
@@ -274,7 +274,7 @@
   \noindent
   In this definition we assume @{text "set"} converts a list into a set.
   At the beginning, that is in the state where no process is created yet, 
-  the waiting queue function will be just the function that returns the
+  the waiting queue function will be the function that just returns the
   empty list for every resource.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -317,7 +317,7 @@
   \end{center}
 
   \noindent
-  The use or relations for representing RAGs allows us to conveninetly define
+  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
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -325,11 +325,11 @@
   \end{isabelle}
 
   \noindent
-  This definition needs to account for all threads that wait for a tread to
+  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 realeased (in the picture above this means also @{text "th\<^isub>3"}, 
+  wait for a resource being released (in the picture above this means 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"}). If there is a cirle in a RAG, then clearly
+  in turn needs to wait for @{text "th\<^isub>1"}). 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 not circular. 
 
@@ -346,7 +346,7 @@
   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
   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 "dependents"} is
+  processes 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
   lowered prematurely.
@@ -354,17 +354,21 @@
   The next function, called @{term schs}, defines the behaviour of the scheduler. It is defined
   by recursion on the state (a list of events); @{term "schs"} takes a state as argument
   and returns a \emph{schedule state}, which we define as a record consisting of two
-  functions
+  functions:
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
   \end{isabelle}
 
   \noindent
-  We have the usual getter and setter methods for such records.
+  The first is a waiting queue function (that is takes a @{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 ???). We have the usual getter and 
+  setter methods for such records.
 
   In the initial state, the scheduler starts with all resources unlocked and the
-  precedence of every thread is initialised with @{term "Prc 0 0"}. 
+  precedence of every thread is initialised with @{term "Prc 0 0"}. Therefore
+  we have
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -374,11 +378,11 @@
   \end{isabelle}
 
   \noindent
-  The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward:
-  we calculuate the waiting queue function of the (previous) state @{text s}; 
-  this waiting queue function @{text wq} is unchanged in the next schedule state; for calculuating 
-  the next @{term "cprec_fun"} we use @{text wq} and the function @{term cpreced}. 
-  This gives the following clauses:
+  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; 
+  for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function 
+  @{term cpreced}. This gives the following three clauses:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -395,10 +399,10 @@
   \end{isabelle}
 
   \noindent 
-  More interesting are the cases when a resource, say @{text cs}, is locked or relaesed. In this case
-  we need to calculate a new waiting queue function. In case of @{term P} we update
-  the function so that the new thread list for @{text cs} is old thread list with the waiting 
-  thread appended to the end (remember the head of this list is in the possession of the
+  More interesting are the cases when a resource, say @{text cs}, is locked or released. In this case
+  we need to calculate a new waiting queue function. In case of @{term P}, we update
+  the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th} 
+  appended to the end (remember the head of this list is in the possession of the
   resource).
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -411,15 +415,35 @@
   \end{isabelle}
 
   \noindent
-  The case for @{term V} is similarly, except that we update the waiting queue function
-  using the auxiliary definition
+  The case for @{term V} is similar, except that we need to update the waiting queue function
+  so that the thread that possessed the lock is eliminated. For this we use
+  the auxiliary function @{term release}. A simple version of @{term release} would
+  just delete this thread and return the rest like so
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{abbrev release}
+  \begin{tabular}{@ {}lcl}
+  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
+  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
+  \end{tabular}
   \end{isabelle}
 
   \noindent
-  This gives for @{term schs} the clause:
+  However in practice often the thread with the highest precedence will get the
+  lock next. We have implemented this choice, but later found out that the choice 
+  about which thread is chosen next is actually irrelevant for the correctness of PIP.
+  Therefore we prove the stronger result where @{term release} is defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}lcl}
+  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
+  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
+  choice for the next waiting list, it just has to be a distinct list and
+  contain the same elements as @{text "qs"}. This gives for @{term V} and @{term schs} the clause:
  
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}




