--- a/Correctness.thy	Fri May 05 15:03:30 2017 +0100
+++ b/Correctness.thy	Fri May 12 14:55:35 2017 +0100
@@ -1283,11 +1283,21 @@
 
 fun postfixes where 
   "postfixes [] = []" |
-  "postfixes (x#xs) = (xs)#postfixes xs" 
+  "postfixes (x#xs) = xs # postfixes xs" 
 
 definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)"
 
+fun upto where
+  "upto s [] = []" |
+  "upto s (e # es) = (es @ s) # upto s es"
 
+value "up_to [s3, s2, s1] [e5, e4, e3, e2, e1] "
+value "upto [s3, s2, s1] [e5, e4, e3, e2, e1] "
+
+lemma "upto s t = up_to s t"
+apply(induct t arbitrary: s)
+apply(auto simp add: up_to_def)
+done
 
 
 definition "occs' Q tt = length (filter Q (postfixes tt))"

--- a/Journal/Paper.thy	Fri May 05 15:03:30 2017 +0100
+++ b/Journal/Paper.thy	Fri May 12 14:55:35 2017 +0100
@@ -1018,7 +1018,7 @@
   stronger statement where we also provide the current precedence of
   the blocking thread. 
 
-  However, this correctness criterion hinges upon a number of
+  However, the theorem we are going to prove hinges upon a number of
   natural assumptions about the states @{text s} and @{text "s' @ s"}, the
   thread @{text th} and the events happening in @{text s'}. We list
   them next:
@@ -1583,38 +1583,41 @@
   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 locking request also a
-  corresponding unlocking request for a resource.  Second, we need to
+  ``good'' programs that contain for every locking request for a
+  resource also a corresponding unlocking request.  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 (there might be a lookp in between the locking and
+  it forever (there might be a loop 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
+  programmer take on the responsibility to program threads in such a
   benign manner (in addition to causing no circularity in the
   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.
+  improvement by establishing a finite bound on the duration of
+  Priority Inversion measured by the number of events.  The events can
+  be seen as a \textit{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
+  finite number of states after state @{term s} in which the thread
   @{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:
+  al.~informally make two assumtions: first, there is a finite pool of
+  threads (active or hibernating) and second, each of them giving up
+  its resources after a finite amount of time.  However, we do not
+  have this concept of active or hibernating threads in our model.  In
+  fact we can dispence with the first assumption altogether and allow
+  that 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:
 
   \begin{quote} {\bf Assumption on the number of threads created in
   every valid state after the state {\boldmath@{text s}}:} Given the
@@ -1635,7 +1638,7 @@
   threads that can potentially block @{text th}:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm blockers_def}
+  @{thm blockers_def[THEN eq_reflection]}
   \end{isabelle}
 
   \noindent This set contains all treads that are not detached in
@@ -1661,26 +1664,36 @@
   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 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"}
+  The main reason for these two assumptions is that we can prove the
+  following: The number of states after @{text s} in which the thread
+  @{text th} 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 intermediate 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 states starting from @{text s} upto the state @{text "t @
+  s"}. For example, suppose $\textit{t} = 
+  [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2, \textit{e}_1]$, then
+  the intermediate states from @{text s} upto @{text "t @ s"} are
 
   \begin{center}
-  @{text "t @ s"},\; \ldots,\; @{text "e2 :: e1 :: s"},\;@{text "e1 :: s"},\;@{text "s"}
+  \begin{tabular}{l}
+  $\textit{s}$\\
+  $\textit{e}_1 :: \textit{s}$\\
+  $\textit{e}_2 :: \textit{e}_1 :: \textit{s}$\\
+  \ldots\\
+  $\textit{e}_{n - 1} :: \ldots :: \textit{e}_2 :: \textit{e}_1 :: \textit{s}$\\
+  \end{tabular}
   \end{center}
 
-  \noindent This can be defined by the following recursive functions
+
+  \noindent This can be defined by the following recursive function
 
   \begin{center}
-  \begin{tabular}{rcl}
-  @{text "s upto t"} & $\equiv$ & @{text "if (t = []) then [s]"} \\
-  & & @{text "else (t @ s) :: s upto (tail t)"}
+  \begin{tabular}{lcl}
+  @{text "s upto []"} & $\dn$ & $[]$\\
+  @{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"}
   \end{tabular}
   \end{center}
   

Binary file journal.pdf has changed