--- a/Correctness.thy	Fri Mar 17 14:57:30 2017 +0000
+++ b/Correctness.thy	Tue Apr 11 03:03:33 2017 +0800
@@ -1240,13 +1240,15 @@
 proof - 
   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"
   from occs_le[of ?Q t] 
+  thm occs_le
   have "?L \<le> (1 + length t) - occs ?Q t" by simp
   also have "... \<le> ?R"
   proof -
+  thm actions_th_occs actions_split
     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
+      from actions_split 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            
@@ -1280,7 +1282,7 @@
     the particular environment in which it operates. In this particular case,
     we regard the @{term t} as the environment of thread @{term th}.
   *}
-  assumes finite_span: 
+  assumes finite_span:
           "th' \<in> blockers \<Longrightarrow>
                  (\<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)"
@@ -1429,6 +1431,8 @@
   "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"
   using actions_split create_bc len_action_blockers by linarith
 
+thm actions_split
+
 end
 
 

--- a/Journal/Paper.thy	Fri Mar 17 14:57:30 2017 +0000
+++ b/Journal/Paper.thy	Tue Apr 11 03:03:33 2017 +0800
@@ -392,7 +392,27 @@
   \noindent
   In this definition @{term "length s"} stands for the length of the list
   of events @{text s}. Again the default value in this function is @{text 0}
-  for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 
+  for threads that have not been created yet. An actor of an event is
+  defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{lcl}
+  @{thm (lhs) actor.simps(5)} & @{text "\<equiv>"} & 
+    @{thm (rhs) actor.simps(5)}\\
+  @{thm (lhs) actor.simps(1)} & @{text "\<equiv>"} & 
+    @{thm (rhs) actor.simps(1)}\\
+  @{thm (lhs) actor.simps(2)} & @{text "\<equiv>"} & 
+    @{thm (rhs) actor.simps(2)}\\
+  @{thm (lhs) actor.simps(3)} & @{text "\<equiv>"} & 
+    @{thm (rhs) actor.simps(3)}\\
+  \end{tabular}}
+  \end{isabelle}
+
+
+
+
+
+  A \emph{precedence} of a thread @{text th} in a 
   state @{text s} is the pair of natural numbers defined as
   
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1532,10 +1552,10 @@
 (*>*)
 text {*
 
-  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
+  Like in the work by Sha et al.~our result in Thm 1 does not yet
+  guarantee the 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
@@ -1544,30 +1564,32 @@
   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. 
+  it forever (there might be a lookp in between the locking and
+  unlocking requests).
 
   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). 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
-  ``time''---when an event occured, some time must have passed.  We
-  can then prove a more direct bound for the absence of indefinite
-  Priority Inversion. This is what we shall show below.
+  RAG). This leave-it-to-the-programmer 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
+  after a Priority Inversion occurs. The events can be seen as a
+  \textbf{rough} abstraction of the ``runtime behaviour'' of threads
+  and also as an abstract notion of ``time''---when a new event
+  happened, some time must have passed.  In this setting we can prove
+  a more direct bound for the absence of indefinite Priority
+  Inversion. This is what we shall show below.
 
   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. Rather, in our model we can create
-  or exit threads arbitrarily. Consequently, the avoidance of
-  indefinite priority inversion we are trying to establish is in our
-  model not true, unless we require that the number of threads
+  @{term th} is blocked.  For this finiteness bound to exist, 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. Rather, in our model we
+  can create or exit threads arbitrarily. Consequently, the avoidance
+  of indefinite priority inversion we are trying to establish is in
+  our model not true, unless we require that the number of threads
   created is bounded in every valid future state after @{term s}. So
   our first assumption states:
 
@@ -1577,13 +1599,13 @@
   require that the number of created threads is less than
   a bound @{text "BC"}, that is 
 
-  \[@{text "len (filter isCreate (t @ s)) < BC"}\;.\]  
+  \[@{text "len (filter isCreate t) < BC"}\;.\]  
   \end{quote}
 
   \noindent Note that it is not enough 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"} events for
-  all valid states after @{text s}.
+  only finite number of threads created in a single state @{text "s' @
+  s"} after @{text s}.  Instead, we need to put this bound on the
+  @{text "Create"} events for all valid states after @{text s}.
 
   For our second assumption about giving up resources after a finite
   amount of ``time'', let us introduce the following definition about
@@ -1594,58 +1616,109 @@
   \end{isabelle}
 
   \noindent This set contains all treads that are not detached in
-  state @{text s} (i.e.~have a lock on a resource) and therefore can
-  potentially block @{text th} after state @{text s}. We need to make
-  the following assumption about the threads in this set:
+  state @{text s} (i.e.~they have a lock on a resource) and therefore
+  can potentially block @{text th} after state @{text s}. We need to
+  make the following assumption about the threads in this set:
 
   \begin{quote}
   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
-  For each @{text "th'"} there exists a finite bound @{text "BND(th')"} 
+  For each such @{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 
-  \[@{text "len(actions_of th' (t @ s)) < BND(th')"}\] 
+  we have that if \mbox{@{term "\<not>(detached (t @ s) th')"}}, then 
+  \[@{text "len (actions_of {th'} t) < BND(th')"}\] 
   \end{quote} 
 
   \noindent By this assumption we enforce that any thread potentially
-  blocking @{term th} must become detached (that is lock 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 in our model correspond to the system calls made by thread. Our @{text
-  "BND(th')"} binds the number of these calls.
+  blocking @{term th} must become detached (that is lock no resource
+  anymore) after a finite number of events in @{text "t @ s"}. Again
+  we have to state 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 in our model correspond to the system calls made by
+  thread. Our @{text "BND(th')"} binds the number of these calls.
   
   The main reason for these two assumptions is that we can prove: the
   number of states after @{text s} in which the thread @{text th} is
-  is not running (that is where PI occurs) can be bounded by the
-  number of actions the threads in @{text blockers} perform and how
-  many threads are newly created. This bound can be stated for all
-  valid states @{term "t @ s"} that can happen after @{text s}. To
-  state our bound we use the definition @{term "Postfixes t \<equiv> {p. \<exists> s'. t = s' @ p}"}.
+  is not running (that is where Priority Inversion occurs) can be
+  bounded by the number of actions the threads in @{text blockers}
+  perform and how many threads are newly created. This bound can be
+  stated for all valid states @{term "t @ s"} that can happen after
+  @{text s}. To state our bound we need to make a definition of what we
+  mean by intermediate states: it will be the list of traces/states starting 
+  from @{text s} ending in @{text "t @ s"}
 
+  \begin{center}
+  @{text "t @ s"},\; \ldots,\; @{text "e2 :: e1 :: s"},\;@{text "e1 :: s"},\;@{text "s"}
+  \end{center}
 
-To state this we use the 
+  \noindent This can be defined by the following recursive functions
+
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{text "s upto t"} & $\equiv$ & @{text "if (t = []) then [s]"} \\
+  & & @{text "else (t @ s) :: s upto (tail t)"}
+  \end{tabular}
+  \end{center}
   
 
+  \noindent Assume you have an extension @{text t}, this essentially 
+  defines in out list representation of states all the postfixes of 
+  @{text t}.
+
+  Theorem: 
+
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm bound_priority_inversion}
+  @{text "len (filter (\<lambda>t'. th \<notin> running t') (s upto t)) \<le>
+  1 + len (actions_of blockers t) + len (filter isCreate t)"}
   \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. 
-   
+  Proof:
+  
+  Consider the states @{text "s upto t"}. It holds that all the states where
+  @{text "th"} runs and all the states where @{text "th"} does not run is 
+  equalt to @{text "1 + len t"}. That means
+
+  \begin{center}
+  @{text "states where th does not run = 1 + len t - states where th runs"} (*)
+  \end{center}
+
+  It also holds that all the actions of @{text "th"} are less or equal to 
+  the states where @{text th} runs. That is
+
+  \begin{center}
+  @{text "len (actions_of {th} t) \<le> states where th runs"}
+  \end{center}
+  
+  That means in $(*)$ we have 
+
+  \begin{center}
+  @{text "states where th does not run \<le> 1 + len t - len (actions_of {th} t)"}
+  \end{center}
 
- Now we can prove a lemma which gives a upper bound
-  of the occurrence number when the most urgent thread @{term th} is blocked.
+  If we look at all the events that can occur in @{text "s upto t"}, we have that
 
+  \begin{center}
+  @{text "len t = len (action_of {th}) + len (action_of blockers t) + 
+  len (filter isCreate t)"}
+  \end{center}
+
+  This gives us finally our theorem. \hfill\qed\medskip
 
-  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. 
+  \noindent In order to now show the absence of indefinite Priority
+  Inversion, we need to show that the number of actions of the @{text
+  "blockers"} is bounded---the number of @{text "Creates"} is clearly
+  bounded by our first assumption. The number of actions of each
+  individual thread in @{text "blockers"} is bound by our second
+  assumption.  Since there can only be a finite number of @{text
+  blockers} in state @{text s} their overall sum is also bounded.
+  This is actually the main conclusion we obtain for the Priority
+  Inheritance Protocol: this above theorem shows is that set of @{text
+  blockers} is fixed at state @{text s} when the Priority Inversion
+  occured and no additional blocker of @{text th} can appear after the
+  state @{text s}. And in this way we can bound the number of states
+  where the thread @{text th} with the highest priority is prevented
+  fropm running.
 
 
 *}

Binary file journal.pdf has changed