# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1489670446 0
# Node ID 550ab0f68960c0c5da4c340ffe0eb1ed98042aa3
# Parent  eae86cba8b89a1ba8f0c1a400aae3c68b967fabb
updasted

diff -r eae86cba8b89 -r 550ab0f68960 Correctness.thy
--- a/Correctness.thy	Mon Mar 06 13:11:16 2017 +0000
+++ b/Correctness.thy	Thu Mar 16 13:20:46 2017 +0000
@@ -1255,6 +1255,30 @@
   finally show ?thesis .
 qed
 
+value "sublists [a,b,cThe]"
+
+theorem bound_priority_inversion:
+  "card { s' @ s | s'. s' \<in> set t \<and>  th \<notin> running (s'@s) } \<le> 
+          1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
+   (is "?L \<le> ?R")
+proof - 
+  let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"
+  from occs_le[of ?Q t] 
+  have "?L \<le> (1 + length t) - occs ?Q t" by simp
+  also have "... \<le> ?R"
+  proof -
+    have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
+              \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")
+    proof -
+      have "?L1 = length (actions_of {th} t)" using actions_split by arith
+      also have "... \<le> ?R1" using actions_th_occs by simp
+      finally show ?thesis .
+    qed            
+    thus ?thesis by simp
+  qed
+  finally show ?thesis .
+qed
+
 end
 
 text {*
diff -r eae86cba8b89 -r 550ab0f68960 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Mar 06 13:11:16 2017 +0000
+++ b/Journal/Paper.thy	Thu Mar 16 13:20:46 2017 +0000
@@ -1550,7 +1550,8 @@
   \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: we can look
+  RAG). This was also the approach taken by Sha et al.~in their paper.
+  However, in this 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 of
@@ -1565,7 +1566,7 @@
   hibernating threads in our model, but we can create or exit threads
   arbitrarily. Consequently, in our model the avoidance of indefinite
   priority inversion we are trying to establish is not true, unless we
-  require that there number of threads is bounded in every
+  require that there number of threads created is bounded in every
   valid future state after @{term s}. So our first assumption 
   states
 
@@ -1578,11 +1579,11 @@
 
   \noindent Note that it is not enough for us to just to state that there
   are only finite number of threads created in the state @{text "s' @ s"}.  Instead, we
-  need to put a bound on the @{text "Create"} event for all valid 
+  need to put a bound on the @{text "Create"} events for all valid 
   states after @{text s}. 
 
-  For our assumption about giving up resources after a finite amount of ``time'',
-  let us introduce the following definition:
+  For our second assumption about giving up resources after a finite
+  amount of ``time'', let us introduce the following definition:
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm blockers_def}
@@ -1594,27 +1595,36 @@
 
   \begin{quote}
   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
-  There exists a finite bound @{text BND} such that for all future 
+  For each @{text "th'"} there exists a finite bound @{text "BND(th')"} 
+  such that for all future 
   valid states @{text "t @ s"},
   we have that if @{term "\<not>(detached (t @ s) th')"}, then 
-  @{term "len(actions_of th' (t @ s)) < BND"}. 
-  \end{quote}
+  @{text "len(actions_of th' (t @ s)) < BND(th')"}. 
+  \end{quote} 
 
-  \noindent
-  By this we mean that any thread that can block @{term th} must become
-  detached (that is hold no resource) after a finite number of events 
-  in @{text "t @ s"}.
+  \noindent By this assumption we enforce that any thread blocking
+  @{term th} must become detached (that is hold no resource) after a
+  finite number of events in @{text "t @ s"}. Again we have to require
+  this bound to hold in all valid states after @{text s}. The bound
+  reflects how each thread @{text "th'"} is programmed: Though we cannot
+  express what instructions a thread is executing, the events correspond 
+  to the system calls made by thread. Our @{text "BND(th')"} bounds 
+  the number of these calls.
   
-  Now we can prove a lemma which gives a upper bound
-  of the occurrence number when the most urgent thread @{term th} is blocked.
+  The main reason for these two assumptions is that we can prove: 
+  
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm bound_priority_inversion}
+  \end{isabelle}
 
   It says, the occasions when @{term th} is blocked during period @{term t} 
   is no more than the number of @{term Create}-operations and 
   the operations taken by blockers plus one. 
+   
 
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{thm bound_priority_inversion}
-  \end{isabelle}
+ Now we can prove a lemma which gives a upper bound
+  of the occurrence number when the most urgent thread @{term th} is blocked.
 
 
   Since the length of @{term t} may extend indefinitely, if @{term t} is full
diff -r eae86cba8b89 -r 550ab0f68960 journal.pdf
Binary file journal.pdf has changed