--- 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.
*}