# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1481296699 0
# Node ID c5a65d98191ad3349fd530a319c2a308713cbc4c
# Parent  10c16b85a839a26ea2c2b1cc93b898a82552dc83
updated

diff -r 10c16b85a839 -r c5a65d98191a Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Dec 09 12:51:29 2016 +0000
+++ b/Journal/Paper.thy	Fri Dec 09 15:18:19 2016 +0000
@@ -309,7 +309,7 @@
   algorithm for a single-processor system.\footnote{We shall come back
   later to the case of PIP on multi-processor systems.} 
   Following good experience in earlier work \cite{Wang09},  
-  our model of PIP is based on Paulson's inductive approach to protocol
+  our model of PIP is based on Paulson's inductive approach for protocol
   verification \cite{Paulson98}. In this approach a \emph{state} of a system is
   given by a list of events that happened so far (with new events prepended to the list). 
   \emph{Events} of PIP fall
@@ -528,12 +528,13 @@
   If there is no cycle, then every RAG can be pictured as a forrest of trees, as
   for example in Figure~\ref{RAGgraph}.
 
+  Because of the RAGs, we will need to formalise some results about graphs.
   While there are few formalisations for graphs already implemented in
   Isabelle, we choose to introduce our own library of graphs for
   PIP. The reason for this is that we wanted to be able to reason with
   potentially infinite graphs (in the sense of infinitely branching
   and infinite size): the property that our RAGs are actually forrests
-  of finitely branching trees having only an finite depth should be a
+  of finitely branching trees having only an finite depth should be 
   something we can \emph{prove} for our model of PIP---it should not
   be an assumption we build already into our model. It seemed for our
   purposes the most convenient represeantation of graphs are binary
@@ -564,9 +565,9 @@
   \end{tabular}
   \end{isabelle}
   
-  \noindent Note that forests can have trees with infinte depth and
+  \noindent Note that forrests can have trees with infinte depth and
   containing nodes with infinitely many children.  A \emph{finite
-  forrest} is a forest which is well-founded and every node has 
+  forrest} is a forrest which is well-founded and every node has 
   finitely many children (is only finitely branching).
 
   \endnote{
@@ -581,15 +582,15 @@
 
   \endnote{{\bf Lemma about overlapping paths}}
   
-
-  We will design our PIP-scheduler  
-  so that every thread can be in the possession of several resources, that is 
-  it has potentially several incoming holding edges in the RAG, but has at most one outgoing  
-  waiting edge. The reason is that when a thread asks for resource that is locked
-  already, then the thread is blocked and cannot ask for another resource.
-  Clearly, also every resource can only have at most one outgoing holding edge---indicating
-  that the resource is locked. In this way we can always start at a thread waiting for a 
-  resource and ``chase'' outgoing arrows leading to a single root of a tree. 
+  The locking mechanism of PIP ensures that for each thread node,
+  there can be many incoming holding edges in the RAG, but at most one
+  out going waiting edge.  The reason is that when a thread asks for
+  resource that is locked already, then the thread is blocked and
+  cannot ask for another resource.  Clearly, also every resource can
+  only have at most one outgoing holding edge---indicating that the
+  resource is locked. So if the @{text "RAG"} is well-founded and
+  finite, we can always start at a thread waiting for a resource and
+  ``chase'' outgoing arrows leading to a single root of a tree.
   
   The use of relations for representing RAGs allows us to conveniently define
   the notion of the \emph{dependants} of a thread using the transitive closure
@@ -611,7 +612,7 @@
   deadlock. Therefore when a thread requests a resource, we must
   ensure that the resulting RAG is not circular. In practice, the
   programmer has to ensure this. Our model will assume that critical 
-  reseources can only be requested provided no circularity can arise.
+  resources can only be requested provided no circularity can arise.
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
diff -r 10c16b85a839 -r c5a65d98191a journal.pdf
Binary file journal.pdf has changed