--- a/prio/Paper/Paper.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -16,9 +16,12 @@
   Prc ("'(_, _')") and
   holding ("holds") and
   waiting ("waits") and
-  Th ("_") and
-  Cs ("_") and
+  Th ("T") and
+  Cs ("C") and
   readys ("ready") and
+  depend ("RAG") and 
+  preced ("prec") and
+  cpreced ("cprec") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -162,7 +165,7 @@
   PIP is based on Paulson's inductive approach to protocol
   verification \cite{Paulson98}, where the \emph{state} of a system is
   given by a list of events that happened so far.  \emph{Events} in PIP fall
-  into five categories defined as the datatype
+  into five categories defined as the datatype:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
@@ -197,7 +200,8 @@
   \end{isabelle}
 
   \noindent
-  Another function calculates the priority for a thread @{text "th"}, defined as
+  Another function calculates the priority for a thread @{text "th"}, which is 
+  defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -215,7 +219,7 @@
   In this definition we set @{text 0} as the default priority for
   threads that have not (yet) been created. The last function we need 
   calculates the ``time'', or index, at which time a process had its 
-  priority set.
+  priority last set.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -233,40 +237,91 @@
   In this definition @{term "length s"} stands for the length of the list
   of events @{text s}. Again the default value in this function is @{text 0}
   for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 
-  state @{text s} is a pair of natural numbers defined as
+  state @{text s} is the pair of natural numbers defined as
   
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm (rhs) preced_def[where thread="th"]}
+  @{thm preced_def[where thread="th"]}
   \end{isabelle}
 
   \noindent
   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 two threads with equal priority by 
+  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. In an impementation
+  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 
   the same priority.
 
   Next, we introduce the concept of \emph{waiting queues}. They are
   lists of threads associated with every resource. The first thread in
-  this list is chosen to be in the one that is in possession of the
+  this list (the head, or short @{term hd}) is chosen to be in 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
-  when a thread \emph{holds}, respectively \emph{waits}, for a
+  when a thread \emph{holds}, respectively \emph{waits} for, a
   resource @{text cs} given a waiting queue function.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm s_holding_def[where thread="th"]}\\
-  @{thm s_waiting_def[where thread="th"]}
+  @{thm cs_holding_def[where thread="th"]}\\
+  @{thm cs_waiting_def[where thread="th"]}
   \end{tabular}
   \end{isabelle}
 
   \noindent
   In this definition we assume @{text "set"} converts a list into a set.
+  Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 
+  (RAG), which represent the dependencies between threads and resources.
+  We represent RAGs as relations using pairs of the form
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
+  @{term "(Cs cs, Th th)"}
+  \end{isabelle}
+
+  \noindent
+  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
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cs_depend_def}
+  \end{isabelle}
+
+  \noindent
+  An instance of a RAG is as follows:
+
+  \begin{center}
+  Picture
+  \end{center}
+
+  \noindent
+  The use or relations for representing RAGs allows us to conveninetly define
+  the notion of the \emph{dependants} of a thread. This is defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cs_dependents_def}
+  \end{isabelle}
+
+  \noindent
+  This definition needs to account for all threads that wait for 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"}, 
+  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
+  we have a deadlock. Therefore when we state our correctness property for PIP
+  we must ensure that RAGs are not circular. This allows us to define the notion
+  of the \emph{current precedence} of a thread @{text th} in a state @{text s}.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cpreced_def2}\\
+  \end{isabelle}
+
+
+
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}