# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1488805876 0
# Node ID eae86cba8b89a1ba8f0c1a400aae3c68b967fabb
# Parent  9756a51f22235af0a2cd42a26bebf871b4074ba8
updated

diff -r 9756a51f2223 -r eae86cba8b89 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Feb 20 15:53:22 2017 +0000
+++ b/Journal/Paper.thy	Mon Mar 06 13:11:16 2017 +0000
@@ -1520,6 +1520,10 @@
 end
 (*>*)
 
+text {*
+   explan why Thm1 roughly corresponds to Sha's Thm 3
+*}
+
 section {* A Finite Bound on Priority Inversion *}
 
 (*<*)
@@ -1528,37 +1532,96 @@
 (*>*)
 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
+  Like in the work by Sha et al.~our result in Thm 1 does not yet guarantee
+  absence of indefinite Priority Inversion. For this we further need the property
+  that every thread gives up its resources after a finite
+  amount of time. We found that this property 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 can
+  ``good'' programs that contain for every locking request also a
+  corresponding unlocking request for a resource.  Second, we need to
   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.
+  it forever. 
+
+  Because of these problems, 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: 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
+  ``time''.  We can then prove a more direct bound for the absence of
+  indefinite Priority Inversion.
 
-  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: 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:
+  What we will establish in this section is that there can only be a
+  finite amount of states after state @{term s} in which the thread
+  @{term th} is blocked. For this to be true, Sha et al.~assume in
+  their work that there is a finite pool of threads (active or
+  hibernating). However, we do not have this concept of active or
+  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
+  valid future state after @{term s}. So our first assumption 
+  states
+
+  \begin{quote} {\bf Assumption on the number of threads created in
+  every valid state after the state {\boldmath@{text s}}:} Given the
+  state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
+  require that the number of created threads is less than
+  @{text "BC"}, that is @{text "len (filter isCreate (t @ s)) <
+  BC"}.  \end{quote}
+
+  \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 
+  states after @{text s}. 
+
+  For our assumption about giving up resources after a finite amount of ``time'',
+  let us introduce the following definition:
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm blockers_def}
   \end{isabelle}
 
   \noindent This set contains all treads that can potentially block
-  @{text th} after state @{text s}.
+  @{text th} after state @{text s}. We need to make the following
+  assumption for the threads in this set:
+
+  \begin{quote}
+  {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
+  There exists a finite bound @{text BND} 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}
+
+  \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"}.
+  
+  Now we can prove a lemma which gives a upper bound
+  of the occurrence number when the most urgent thread @{term th} is blocked.
+
+  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}
+
+
+  Since the length of @{term t} may extend indefinitely, if @{term t} is full
+  of the above mentioned blocking operations, @{term th} may have not chance to run. 
+  And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely 
+  with the growth of @{term t}. Therefore, this lemma alone does not ensure 
+  the correctness of PIP. 
 
 
 *}
diff -r 9756a51f2223 -r eae86cba8b89 journal.pdf
Binary file journal.pdf has changed