--- a/Journal/Paper.thy	Mon Feb 06 12:27:20 2017 +0000
+++ b/Journal/Paper.thy	Mon Feb 20 13:07:26 2017 +0000
@@ -1520,29 +1520,36 @@
 end
 (*>*)
 
-section {* Avoiding Indefinite Priority Inversion *}
+section {* A Finite Bound on Priority Inversion *}
 
 text {*
-     Like in the argument by Sha et al.~our finite bound does not
-  guarantee absence of indefinite Priority Inversion. For this we
+
+  Like in the argument by Sha et al.~our result does not
+  yet guarantee absence of indefinite Priority Inversion. For this we
   further have to assume that every thread gives up its resources
-  after a finite amount of time. We found that this assumption is
-  awkward to formalise in our model. There are mainly two reasons for
-  this: First, we do not specify what ``running'' the code of a thread
-  means, for example by giving an operational semantics for machine
-  instructions. Therefore we cannot characterise what are ``good''
-  programs that contain for every looking request also a corresponding
-  unlocking request for a resource. Second, we would need to specify a
-  kind of global clock that tracks the time how long a thread locks a
-  resource. But this seems difficult, because how do we conveniently
-  distinguish between a thread that ``just'' locks a resource for a
-  very long time and one that locks it forever.  Therefore we decided
-  to leave out this property and let the programmer assume the
+  after a finite amount of time. We found that this assumption is not
+  so straightforward to formalise in our model. There are mainly two
+  reasons for this: First, we do not specify what ``running'' the code
+  of a thread means, for example by giving an operational semantics
+  for machine instructions. Therefore we cannot characterise what are
+  ``good'' programs that contain for every looking request also a
+  corresponding unlocking request for a resource. Second, we would
+  need to specify a kind of global clock that tracks the time how long
+  a thread locks a resource. But this seems difficult, because how do
+  we conveniently distinguish between a thread that ``just'' locks a
+  resource for a very long time and one that locks it forever.
+
+  Therefore we decided in our earlier paper \cite{ZhangUrbanWu12} to
+  leave out this property and let the programmer assume the
   responsibility to program threads in such a benign manner (in
-  addition to causing no circularity in the RAG). In this detail, we
+  addition to causing no circularity in the RAG). However, in this
+  paper we can make an improvement: 
+
+In this detail, we
   do not make any progress in comparison with the work by Sha et al.
   However, we are able to combine their two separate bounds into a
-  single theorem improving their bound.
+  single theorem improving their bound. We can characterise a 
+  program
 
 *}