# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1486384040 0
# Node ID 188fe0c81ac75896e4ab91ce8d3127a3a8cecfe5
# Parent  e4d151d761c4d30bdb6ab42067ee36393e986d74
updated

diff -r e4d151d761c4 -r 188fe0c81ac7 Correctness.thy
--- a/Correctness.thy	Mon Dec 19 23:43:54 2016 +0000
+++ b/Correctness.thy	Mon Feb 06 12:27:20 2017 +0000
@@ -725,35 +725,11 @@
 
 section {* The existence of `blocking thread` *}
 
-text {* 
-  Suppose @{term th} is not running, it is first shown that
-  there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
-  in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
-
-  Now, since @{term readys}-set is non-empty, there must be
-  one in it which holds the highest @{term cp}-value, which, by definition, 
-  is the @{term running}-thread. However, we are going to show more: this 
-  running thread is exactly @{term "th'"}. *}
-
-
-lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
-                    "th' \<in> running (t @ s)"
+lemma th_ancestor_has_max_ready:
+  assumes th'_in: "th' \<in> readys (t@s)" 
+  and dp: "th' \<in> nancestors (tG (t @ s)) th"
+  shows "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
 proof -
-    -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
-       ready ancestor of @{term th}. *}
-  have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" 
-    using th_kept vat_t.th_chain_to_ready_tG by auto
-  then obtain th' where th'_in: "th' \<in> readys (t@s)"
-                    and dp: "th' \<in> nancestors (tG (t @ s)) th"
-    by blast
-
-  -- {* We are going to first show that this @{term th'} is running. *}
-  have "th' \<in> running (t @ s)"
-  proof -
-    -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
-    have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
-    proof -
       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
             the  @{term cp}-value of @{term th'} is the maximum of 
             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
@@ -776,14 +752,40 @@
         using th_cp_max th_cp_preced th_kept 
               the_preced_def vat_t.max_cp_readys_threads by auto
       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
-    qed 
+ qed 
+
+
+text {* 
+  Suppose @{term th} is not running, it is first shown that
+  there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
+  in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
+
+  Now, since @{term readys}-set is non-empty, there must be
+  one in it which holds the highest @{term cp}-value, which, by definition, 
+  is the @{term running}-thread. However, we are going to show more: this 
+  running thread is exactly @{term "th'"}. *}
+
 
-    -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
-          it is @{term running} by definition. *}
-    with `th' \<in> readys (t @ s)` 
-    show "th' \<in> running (t @ s)" by (simp add: running_def) 
-  qed
+lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
+  obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
+                    "th' \<in> running (t @ s)"
+proof -
+    -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
+       ready ancestor of @{term th}. *}
+  have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" 
+    using th_kept vat_t.th_chain_to_ready_tG by auto
+  then obtain th' where th'_in: "th' \<in> readys (t @ s)"
+                    and dp: "th' \<in> nancestors (tG (t @ s)) th"
+    by blast
 
+  -- {* We are going to first show that this @{term th'} is running. *}
+
+  from th'_in dp
+  have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" 
+    by (rule th_ancestor_has_max_ready)
+  with `th' \<in> readys (t @ s)` 
+  have "th' \<in> running (t @ s)" by (simp add: running_def) 
+ 
   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
   moreover have "th' \<in> nancestors (tG (t @ s)) th"
     using dp unfolding nancestors_def2 by simp
@@ -931,15 +933,15 @@
   thus ?thesis unfolding blockers_def by simp
 qed
 
-text {*
-  The following lemma shows that a blocker may never die
-  as long as the highest thread @{term th} is living. 
+text {* The following lemma shows that a blocker does not die as long as the
+highest thread @{term th} is live.
 
-  The reason for this is that, before a thread can execute an @{term Exit} operation,
-  it must give up all its resource. However, the high priority inherited by a blocker 
-  thread also goes with the resources it once held, and the consequence is the lost of 
-  right to run, the other precondition for it to execute its own  @{term Exit} operation.
-  For this reason, a blocker may never exit before the exit of the highest thread @{term th}.
+  The reason for this is that, before a thread can execute an @{term Exit}
+  operation, it must give up all its resource. However, the high priority
+  inherited by a blocker thread also goes with the resources it once held,
+  and the consequence is the lost of right to run, the other precondition
+  for it to execute its own @{term Exit} operation. For this reason, a
+  blocker may never exit before the exit of the highest thread @{term th}.
 *}
 
 lemma blockers_kept:
diff -r e4d151d761c4 -r 188fe0c81ac7 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Dec 19 23:43:54 2016 +0000
+++ b/Journal/Paper.thy	Mon Feb 06 12:27:20 2017 +0000
@@ -423,18 +423,18 @@
   like our FIFO-scheduling of threads with equal priority reduces the number of
   tasks involved in the inheritance process and thus minimises the number
   of potentially expensive thread-switches. 
-
-  \endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
-  in a state @{term s}. This can be straightforwardly defined in Isabelle as
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  \mbox{\begin{tabular}{@ {}l}
-  @{thm cntP_def}\\
-  @{thm cntV_def}
-  \end{tabular}}
-  \end{isabelle}
-
-  \noindent using the predefined function @{const count} for lists.}
+  
+  %\endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+  %in a state @{term s}. This can be straightforwardly defined in Isabelle as
+  %
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %\mbox{\begin{tabular}{@ {}l}
+  %@{thm cntP_def}\\
+  %@{thm cntV_def}
+  %\end{tabular}}
+  %\end{isabelle}
+  % 
+  %\noindent using the predefined function @{const count} for lists.}
 
   Next, we introduce the concept of \emph{waiting queues}. They are
   lists of threads associated with every resource. The first thread in
@@ -528,23 +528,23 @@
   If there is no cycle, then every RAG can be pictured as a forrest of trees, as
   for example in Figure~\ref{RAGgraph}.
 
-  Because of the RAGs, we will need to formalise some results about graphs.
-  While there are few formalisations for graphs already implemented in
-  Isabelle, we choose to introduce our own library of graphs for
-  PIP. The reason for this is that we wanted to be able to reason with
-  potentially infinite graphs (in the sense of infinitely branching
-  and infinite size): the property that our RAGs are actually forrests
-  of finitely branching trees having only an finite depth should be 
-  something we can \emph{prove} for our model of PIP---it should not
-  be an assumption we build already into our model. It seemed for our
-  purposes the most convenient represeantation of graphs are binary
-  relations given by sets of pairs from \eqref{pairs}. The pairs stand for the edges in
+  Because of the RAGs, we will need to formalise some results about
+  graphs.  While there are few formalisations for graphs already
+  implemented in Isabelle, we choose to introduce our own library of
+  graphs for PIP. The justification for this is that we wanted to be able to
+  reason about potentially infinite graphs (in the sense of infinitely
+  branching and infinite size): the property that our RAGs are
+  actually forrests of finitely branching trees having only an finite
+  depth should be something we can \emph{prove} for our model of
+  PIP---it should not be an assumption we build already into our
+  model. It seemed for our purposes the most convenient
+  represeantation of graphs are binary relations given by sets of
+  pairs shown in \eqref{pairs}. The pairs stand for the edges in
   graphs. This relation-based representation is convenient since we
   can use the notions of transitive closure operations @{term "trancl
-  DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation composition
-  @{term "DUMMY O DUMMY"}.  A \emph{forrest} is defined as the
-  relation @{text rel} that is \emph{single valued} and
-  \emph{acyclic}:
+  DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
+  composition.  A \emph{forrest} is defined as the relation @{text
+  rel} that is \emph{single valued} and \emph{acyclic}:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -554,8 +554,8 @@
   \end{isabelle} 
 
   \noindent
-  The \emph{children}, \emph{subtree} and \emph{ancestors} of a node in a graph are 
-  defined as
+  The \emph{children}, \emph{subtree} and \emph{ancestors} of a node in a graph
+  can be easily defined relationally as 
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -574,13 +574,14 @@
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm rtrancl_path.intros}
   \end{isabelle} 
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{thm rpath_def}
-  \end{isabelle}}
+  
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %@{thm rpath_def}
+  %\end{isabelle}
+  }
 
 
-  \endnote{{\bf Lemma about overlapping paths}}
+  %\endnote{{\bf Lemma about overlapping paths}}
   
   The locking mechanism of PIP ensures that for each thread node,
   there can be many incoming holding edges in the RAG, but at most one
@@ -831,16 +832,16 @@
   @{thm[mode=Rule] thread_set[where thread=th]}
   \end{center}
 
-  \noindent
-  If a thread wants to lock a resource, then the thread needs to be
-  running and also we have to make sure that the resource lock does
-  not lead to a cycle in the RAG. In practice, ensuring the latter
-  is the responsibility of the programmer.  In our formal
-  model we brush aside these problematic cases in order to be able to make
-  some meaningful statements about PIP.\footnote{This situation is
-  similar to the infamous \emph{occurs check} in Prolog: In order to say
-  anything meaningful about unification, one needs to perform an occurs
-  check. But in practice the occurs check is omitted and the
+  \noindent If a thread wants to lock a resource, then the thread
+  needs to be running and also we have to make sure that the resource
+  lock does not lead to a cycle in the RAG (the prurpose of the second
+  premise in the rule below). In practice, ensuring the latter is the
+  responsibility of the programmer.  In our formal model we brush
+  aside these problematic cases in order to be able to make some
+  meaningful statements about PIP.\footnote{This situation is similar
+  to the infamous \emph{occurs check} in Prolog: In order to say
+  anything meaningful about unification, one needs to perform an
+  occurs check. But in practice the occurs check is omitted and the
   responsibility for avoiding problems rests with the programmer.}
 
  
@@ -875,10 +876,13 @@
 
   \noindent
   This completes our formal model of PIP. In the next section we present
-  properties that show our model of PIP is correct.
+  a series of desirable properties derived from our model of PIP. This can
+  be regarded as a validation of the correctness of our model.
 *}
 
+(*
 section {* Preliminaries *}
+*)
 
 (*<*)
 context valid_trace
@@ -981,7 +985,7 @@
   the blocking thread. 
 
   However, this correctness criterion hinges upon a number of
-  assumptions about the states @{text s} and @{text "s' @ s"}, the
+  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:
 
@@ -1016,7 +1020,8 @@
   than @{text th} are continuously created in @{text s'}. Therefore we have to assume that  
   events in @{text s'} can only create (respectively set) threads with equal or lower 
   priority than @{text prio} of @{text th}. We also need to assume that the
-  priority of @{text "th"} does not get reset and also that @{text th} does
+  priority of @{text "th"} does not get reset and all other reset priorities are either
+  less or equal. Moreover, we assume  that @{text th} does
   not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
@@ -1048,33 +1053,13 @@
   the highest precedence in the state @{text s}, is either running in
   state @{term "s' @ s"}, or can only be blocked in the state @{text
   "s' @ s"} by a thread @{text th'} that already existed in @{text s}
-  and requested or had a lock on at least one resource---that means
+  and requested a resource or had a lock on at least one resource---that means
   the thread was not \emph{detached} in @{text s}.  As we shall see
   shortly, that means there are only finitely many threads that can
   block @{text th} in this way and then they need to run with the same
   precedence as @{text th}.
 
-  Like in the argument by Sha et al.~our finite bound does not
-  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
-  awkward 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.  Therefore we decided
-  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). 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.
-
+  
 %% HERE
 
   Given our assumptions (on @{text th}), the first property we can
@@ -1094,7 +1079,7 @@
   \end{center}
 
   \noindent
-  We also know that this is equal to the current precedences of all threads,
+  We also know that this is equal to the maximum of current precedences of all threads,
   that is
 
   \begin{center}
@@ -1119,7 +1104,7 @@
   hold a resource in state @{text s}.
 
   \begin{lemma}\label{notdetached}
-  If @{term "th' \<in> running (s' @ s)"} then @{term "\<not>detached s th'"}.
+  If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}.
   \end{lemma}
 
   \begin{proof} Let us assume @{text "th'"} is detached in state
@@ -1516,7 +1501,8 @@
   %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
   %then.
 
-  NOTE: about bounds in sha et al and ours:
+  NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual
+  blocages. We prove a bound for the overall-blockage.
 
   There are low priority threads, 
   which do not hold any resources, 
@@ -1534,6 +1520,33 @@
 end
 (*>*)
 
+section {* Avoiding Indefinite Priority Inversion *}
+
+text {*
+     Like in the argument by Sha et al.~our finite bound does not
+  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
+  awkward 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.  Therefore we decided
+  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). 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.
+
+*}
+
+
 section {* Properties for an Implementation\label{implement} *}
 
 text {*
diff -r e4d151d761c4 -r 188fe0c81ac7 journal.pdf
Binary file journal.pdf has changed