# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1487596084 0
# Node ID 8a9767ab64155fb0dff8c097a3f2b9493e37add0
# Parent  15f4481bc0c9c168c38ffb54fd570f8f1837709e# Parent  a79a6a286108faed97b05743fdfe84e4a8467f10
merged

diff -r a79a6a286108 -r 8a9767ab6415 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Feb 07 02:10:22 2017 +0000
+++ b/Journal/Paper.thy	Mon Feb 20 13:08:04 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
 
 *}
 
diff -r a79a6a286108 -r 8a9767ab6415 journal.pdf
Binary file journal.pdf has changed