--- a/Correctness.thy	Mon Feb 20 13:08:04 2017 +0000
+++ b/Correctness.thy	Mon Feb 20 15:53:22 2017 +0000
@@ -2,6 +2,11 @@
 imports PIPBasics
 begin
 
+lemma actions_of_len_cons [iff]: 
+    "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1"
+      by  (unfold actions_of_def, simp)
+
+
 text {* 
   The following two auxiliary lemmas are used to reason about @{term Max}.
 *}
@@ -1277,9 +1282,15 @@
   *}
   assumes finite_span: 
           "th' \<in> blockers \<Longrightarrow>
-                 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
-                                length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')"
-  -- {* The following @{text BC} is bound of @{term Create}-operations *}
+                 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
+                                  \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"
+
+  -- {*
+    The difference between this @{text finite_span} and the former one is to allow the number
+    of action steps to change with execution paths (i.e. different value of @{term "t'@s"}}).
+    The @{term span} is a upper bound on these step numbers. 
+  *}
+
   fixes BC
   -- {* 
   The following assumption requires the number of @{term Create}-operations is 
@@ -1316,8 +1327,8 @@
   operations take by each particular blocker.
 *}
 definition "span th' = (SOME span.
-         \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
-              length (actions_of {th'} t') = span \<longrightarrow> detached (t' @ s) th')"
+         \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
+                  \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"
 
 text {*
   The following lemmas shows the correctness of @{term span}, i.e. 
@@ -1333,8 +1344,8 @@
   shows "length (actions_of {th'} t) \<le> span th'"
 proof -
   from finite_span[OF assms(1)] obtain span' 
-  where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
-                     length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'")
+  where span': "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> 
+                       \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span'" (is "?P span'")
                      by auto
   have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"
   proof(rule someI2[where a = span'])
@@ -1345,11 +1356,8 @@
       case h: (Cons e t)
         interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
       show ?case
-      proof(cases "length (actions_of {th'} t) < span")
+      proof(cases "detached (t@s) th'")
         case True
-        thus ?thesis by (simp add:actions_of_def)
-      next
-        case False
         have "actor e \<noteq> th'"
         proof
           assume otherwise: "actor e = th'"
@@ -1359,14 +1367,16 @@
           have "th' \<in> running (t @ s)" .
           moreover have "th' \<notin> running (t @ s)"
           proof -
-            from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
-            from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
-            from extend_highest_gen.detached_not_running[OF h(3) this] assms
+            from extend_highest_gen.detached_not_running[OF h(3) True] assms
             show ?thesis by (auto simp:blockers_def)
           qed
           ultimately show False by simp
         qed
         with h show ?thesis by (auto simp:actions_of_def)
+      next
+        case False
+        from fs[rule_format, OF h(3) this] and actions_of_len_cons
+        show ?thesis by (meson discrete order.trans) 
       qed
     qed (simp add: actions_of_def)
   next
@@ -1422,6 +1432,6 @@
 end
 
 
-unused_thms
+
 
 end

--- a/Journal/Paper.thy	Mon Feb 20 13:08:04 2017 +0000
+++ b/Journal/Paper.thy	Mon Feb 20 15:53:22 2017 +0000
@@ -1522,37 +1522,49 @@
 
 section {* A Finite Bound on Priority Inversion *}
 
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
 text {*
 
-  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 not
-  so straightforward to formalise in our model. There are mainly two
+  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 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.
+  corresponding unlocking request for a resource.  Second, we can
+  distinghish between a thread that ``just'' locks a resource for a
+  finite amount of time (even if it is very long) and one that locks
+  it forever. But this seems difficut.
 
   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). However, in this
-  paper we can make an improvement: 
+  paper we can make an improvement: we can look at the \emph{events}
+  that are happening once a Priority Inversion occurs. The events can
+  be seen as a rough abstraction of the ``runtime behaviour'' of
+  threads and also as an abstract notion for ``time''.  We can then
+  prove a more direct result for the absence of indefinite Priority
+  Inversion. For this let us introduce the following definition:
 
-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. We can characterise a 
-  program
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm blockers_def}
+  \end{isabelle}
+
+  \noindent This set contains all treads that can potentially block
+  @{text th} after state @{text s}.
+
 
 *}
-
+(*<*)
+end
+(*>*)
 
 section {* Properties for an Implementation\label{implement} *}
 

Binary file journal.pdf has changed