
diff -r 914288aec495 -r 312497c6d6b9 Journal/Paper.thy
--- a/Journal/Paper.thy	Wed Aug 02 13:18:14 2017 +0100
+++ b/Journal/Paper.thy	Wed Aug 02 14:56:47 2017 +0100
@@ -2064,42 +2064,43 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (concl) valid_trace_p_w.RAG_es}\\
-  @{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept} @{text "then"}
+  @{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept_tG} @{text "then"}
   @{thm (concl) valid_trace_p_w.cp_kept_tG}
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  That means we have to add a waiting edge to the @{text RAG}. Furthermore
-  the current precedence for all threads that are not dependants of @{text "th'"}
-  are unchanged. For the others we need to follow the edges 
-  in the @{text RAG} and recompute the @{term "cp"}. 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 
-  thread encountered on the way. Since the @{term "depend"}
-  is loop free, this procedure will always stop. The following lemma shows, however, 
-  that this procedure can actually stop often earlier without having to consider all
-  dependants.
+  \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
+  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
+  @{term "children"}-edges to recompute the @{term "cp"} of every
+  thread encountered on the way using Lemma~\ref{childrenlem}. 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
+  consider all ancestors.
 
   \begin{isabelle}\ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  %%@ {t hm[mode=IfThen] eq_up_self}\\
-  HERE
-  %@{text "If"} @ {thm (prem 1) eq_up}, @ {thm (prem 2) eq_up} and @ {thm (prem 3) eq_up}\\
-  %@{text "then"} @ {thm (concl) eq_up}.
+  \begin{tabular}{@ {}ll}
+  @{text If} & @{thm (prem 2) valid_trace_p_w.cp_up_tG}\\
+             & @{thm (prem 4) valid_trace_p_w.cp_up_tG} and \\
+             & @{thm (prem 3) valid_trace_p_w.cp_up_tG}\\
+  & @{text then} @{thm (concl) valid_trace_p_w.cp_up_tG}\\
   \end{tabular}
   \end{isabelle}
  
-  \noindent
-  This lemma states that if an intermediate @{term cp}-value does not change, then
-  the procedure can also stop, because none of its dependent threads will
-  have their current precedence changed.
-  *}
+  \noindent This lemma 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.  
+
+*}
 
 text {*
   As can be seen, a pleasing byproduct of our formalisation is that the properties in
   this section closely inform an implementation of PIP, namely whether the
-  RAG needs to be reconfigured or current precedences need to
+  @{text RAG} needs to be reconfigured or current precedences need to
   be recalculated for an event. This information is provided by the lemmas we proved.
   We confirmed that our observations translate into practice by implementing
   our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 
@@ -2212,8 +2213,8 @@
   Thus we established two pointers: one in the waiting queue of the lock pointing to the 
   current thread, and the other from the currend thread pointing to the lock.
   According to our specification in Section~\ref{model} and the properties we were able 
-  to prove for @{text P}, we need to ``chase'' all the dependants 
-  in the RAG (Resource Allocation Graph) and update their
+  to prove for @{text P}, we need to ``chase'' all the ancestor threads
+  in the @{text RAG} and update their
   current precedence; however we only have to do this as long as there is change in the 
   current precedence.
 
@@ -2226,7 +2227,8 @@
   then we leave the loop, since nothing else needs to be updated (Lines 15 and 16).
   If there is a change, then we have to continue our ``chase''. We check what lock the 
   thread @{ML_text pt} is waiting for (Lines 17 and 18). If there is none, then 
-  the thread @{ML_text pt} is ready (the ``chase'' is finished with finding a root in the RAG). In this 
+  the thread @{ML_text pt} is ready (the ``chase'' is finished with finding a root in the @{text RAG}). 
+  In this 
   case we update the ready-queue accordingly (Lines 19 and 20). If there is a lock  @{ML_text pt} is 
   waiting for, we update the waiting queue for this lock and we continue the loop with 
   the holder of that lock 
@@ -2354,7 +2356,7 @@
   \bibliographystyle{plain}
   \bibliography{root}
 
-  \theendnotes
+  %%\theendnotes
 *}
 
 




