--- a/Implementation.thy	Wed Aug 02 13:18:14 2017 +0100
+++ b/Implementation.thy	Wed Aug 02 14:56:47 2017 +0100
@@ -690,7 +690,7 @@
   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
 qed
 
-lemma cp_kept_tG:
+lemma cp_kept_tG: (* aaa *)
   assumes "th'' \<notin> ancestors (tG (e#s)) th"
   shows "cp (e#s) th'' = cp s th''"
   using cp_kept tG_ancestors_tRAG_refute assms
@@ -859,7 +859,7 @@
   show ?thesis by metis
 qed
 
-lemma cp_up_tG:
+lemma cp_up_tG: (* aaa *)
   assumes "th' \<in> ancestors (tG (e#s)) th"
   and "cp (e#s) th' = cp s th'"
   and "th'' \<in> ancestors (tG (e#s)) th'"

--- 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
 *}
 
 

--- a/Journal/document/root.tex	Wed Aug 02 13:18:14 2017 +0100
+++ b/Journal/document/root.tex	Wed Aug 02 14:56:47 2017 +0100
@@ -54,12 +54,14 @@
 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
 Compared with that paper we give an actual implementation of our formalised scheduling 
 algorithm in C and the operating system PINTOS. Our implementation follows closely all results
-we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper
-more details about the proof and also surveying 
+we proved about optimisations of the Priority Inheritance Protocol.
+In Section 4 we improve our previous result by proving a finite bound for Priority Inversion.
+Moreover, we are giving in this paper
+more details about our proof and also surveying 
 the existing literature in more depth.}
 \renewcommand{\thefootnote}{\arabic{footnote}}
 
-\title{Priority Inheritance Protocol Proved Correct}
+\title{Priority Inheritance Protocol Proved Correct$^\star$}
 \author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$}
 \institute{PLA University of Science and Technology, China \and 
            King's College London, United Kingdom}

Binary file journal.pdf has changed