--- a/prio/Paper/Paper.thy	Sat Feb 11 08:16:11 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 11 09:14:14 2012 +0000
@@ -187,8 +187,8 @@
   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:
+  about states.  One, called @{term threads}, calculates, given a state @{text s}, the set of
+  ``live'' threads that we have seen so far:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -252,8 +252,8 @@
   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 
   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 impementation
-  this choice would translate to a quite natural a FIFO-scheduling of processes with 
+  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 
   the same priority.
 
   Next, we introduce the concept of \emph{waiting queues}. They are
@@ -261,10 +261,10 @@
   this list (the head, or short @{term hd}) is chosen to be 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
+  functions, below abbreviated as @{text wq}. They take a resource as
+  argument and return a list of threads.  This allows us to define
   when a thread \emph{holds}, respectively \emph{waits} for, a
-  resource @{text cs} given a waiting queue function.
+  resource @{text cs} given a waiting queue function @{text wq}.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -277,7 +277,7 @@
   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
-  empty list.
+  empty list for every resource.
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{abbrev all_unlocked}
@@ -327,15 +327,15 @@
   \end{isabelle}
 
   \noindent
-  This definition needs to account for all threads that wait for tread to
+  This definition needs to account for all threads that wait for a tread to
   release a resource. This means we need to include threads that transitively
-  wait for a resource being realeased (in the picture this means also @{text "th\<^isub>3"}, 
+  wait for a resource being realeased (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 waits 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 cirle 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. 
 
-  Next we introduce the notion of \emph{current precedence} for a thread @{text th} in a 
+  Next we introduce the notion of the \emph{current precedence} for a thread @{text th} in a 
   state @{text s}, which is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -343,7 +343,8 @@
   \end{isabelle}
 
   \noindent
-  While the precedence of a thread is determined by the programmer (for example when the thread is
+  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
   given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 
@@ -354,7 +355,12 @@
   
   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 defined as a record consisting of ...
+  and returns a \emph{schedule state}, which we define as a record consisting of two
+  functions
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
+  \end{isabelle}
 
   In the initial state, the scheduler starts with all resources unlocked and the
   precedence of every thread is initialised with @{term "Prc 0 0"}. 

Binary file prio/paper.pdf has changed