--- a/Journal/Paper.thy	Fri Aug 11 16:09:02 2017 +0100
+++ b/Journal/Paper.thy	Mon Aug 14 14:16:25 2017 +0100
@@ -1839,8 +1839,8 @@
   depends on the precedenes of all threads in its subtree---a ``global'' transitive notion,
   which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}).
   We can however improve upon this. For this recall the notion
-  of @{term children} of a thread @{text th} (defined in \eqref{children})
-  where a child is a thread that is only one ``hop'' away from the thread
+  of @{term children} of a thread @{text th} defined in \eqref{children}.
+  There a child is a thread that is only one ``hop'' away from the thread
   @{text th} in the @{term TDG} (and waiting for @{text th} to release
   a resource). Using children, we can prove the following lemma for more efficiently calculating
   @{text cprec} of a thread @{text th}.
@@ -1865,14 +1865,14 @@
   precedence is re-set or when @{text "(ii)"} one of
   its children changes its current precedence or when @{text "(iii)"} the children set changes
   (for example in an @{text "V"}-event).   
-  If only the static precedence or the children-set changes, the we can 
+  If only the static precedence or the children-set changes, then we can 
   avoid the recursion and compute the @{text cprec} of @{text th} locally.
-  In this cases
+  In such cases
   the recursion does not need to decend into the corresponding subtree.
   Once the current 
   precedence is computed in this more efficient manner, the selection
   of the thread with highest precedence from a set of ready threads is
-  a standard scheduling operation implemented in most operating
+  a standard scheduling operation and implemented in most operating
   systems.
 
   %\begin{proof}[of Lemma~\ref{childrenlem}]
@@ -1948,7 +1948,8 @@
 
   %The second
   %however states that only threads that are \emph{not} dependants of @{text th} have their
-  %current precedence unchanged. For the others we have to recalculate the current
+  %current precedence unchanged. For the ancestors of @{text th}, we 
+  %have to recalculate the current
   %precedence. To do this we can start from @{term "th"} 
   %and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
   %the @{term "cp"} of every 
@@ -2081,11 +2082,20 @@
 
   \noindent That means we have to add a waiting edge to the @{text
   RAG}. Furthermore the current precedence for all threads that are
-  not ancestors of @{text "th"} are unchanged. For the others we need
+  not ancestors of @{text "th"} are unchanged. For the ancestors of 
+  @{text th} we need
   to follow the edges in the @{text TDG} and recompute the @{term
-  "cp"}. To do this we can start from @{term "th"} and follow the
+  "cprecs"}. Whereas in all other event we might have to make
+  modifications to the @{text "RAG"}, no recalculation of @{text
+  cprec} depends on the @{text RAG}. This is the only case where
+  the recalulation needs to take the connections in the @{text RAG} into
+  account.
+  To do this we can start from @{term "th"} and follow the
   @{term "children"}-edges to recompute the @{term "cp"} of every
-  thread encountered on the way using Lemma~\ref{childrenlem}. Since
+  thread encountered on the way using Lemma~\ref{childrenlem}. 
+  This means the recomputation can be done locally (level-by-level)
+  in a bottom-up fashion.
+  Since
   the @{text RAG}, and thus @{text "TDG"}, are loop free, this
   procedure will always stop. The following lemma shows, however, that
   this procedure can actually stop often earlier without having to
@@ -2100,7 +2110,7 @@
   \end{tabular}
   \end{isabelle}
  
-  \noindent This lemma states that if an intermediate @{term cp}-value
+  \noindent This property states that if an intermediate @{term cp}-value
   does not change (in this case the @{text cprec}-value of @{text "th'"}), then the procedure can
   also stop, because none of @{text "th'"} ancestor-threads will have their
   current precedence changed.  
@@ -2347,11 +2357,16 @@
   reasoning: gaining deeper understanding of the subject matter.
 
   Our formalisation
-  consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
+  consists of around 600 lemmas and overall 10800 lines 
+  of readable and commented Isabelle/Isar
   code with a few apply-scripts interspersed. The formal model of PIP
-  is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
-  definitions and proofs span over 770 lines of code. The properties relevant
-  for an implementation require 2000 lines. 
+  is 620 lines long; our graph theory implementation using relations is 
+  1860 lines; the basic properties of PIP take around 5500 lines of code; 
+  and the formal correctness proof 1700 lines. 
+  %Some auxiliary
+  %definitions and proofs span over 770 lines of code. 
+  The properties relevant
+  for an implementation require 1000 lines. 
   The code of our formalisation 
   can be downloaded from the Mercurial repository at
   \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/pip}.

Binary file journal.pdf has changed