--- a/Journal/Paper.thy Tue May 23 15:10:48 2017 +0100
+++ b/Journal/Paper.thy Fri Jun 02 14:36:44 2017 +0100
@@ -1588,7 +1588,7 @@
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 loop in between the locking and
+ it forever (there might be an unbounded loop in between the locking and
unlocking requests).
Because of these problems, we decided in our earlier paper
@@ -1601,24 +1601,25 @@
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.
+ ``time''---when a new event happens, some time must have passed.
What we will establish in this section is that there can only be a
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.~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
+ @{term th} is blocked (recall for this that a state is a list of
+ events). For this finiteness bound to exist, Sha et 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 new threads or exit existing threads
arbitrarily. Consequently, the avoidance of indefinite priority
inversion we are trying to establish is in our model not true,
- unless we put up an upper bound on the number of threads that
- have been created upto any valid future state after @{term
- s}. Otherwise our PIP scheduler could be ``swamped'' with @{text
- "Create"}-requests. So our first assumption states:
+ unless we stipulate an upper bound on the number of threads that
+ have been created during the time leading to any future state
+ after @{term s}. Otherwise our PIP scheduler could be ``swamped''
+ with @{text "Create"}-requests. So our first assumption states:
\begin{quote} {\bf Assumption on the number of threads created
after the state {\boldmath@{text s}}:} Given the
@@ -1638,7 +1639,7 @@
This ensures that no matter which ``future'' state is reached, the
number of @{text "Create"}-events is finite. We use @{text "es @ s"}
to stand for \emph{future states} after @{text s}---it is @{text s}
- extended with some list of events.
+ extended with some list @{text es} of events.
For our second assumption about giving up resources after a finite
amount of ``time'', let us introduce the following definition about
@@ -1651,9 +1652,10 @@
\noindent This set contains all treads that are not detached in
state @{text s}. According to our definiton of @{text "detached"},
this means a thread in @{text "blockers"} either holds or waits for
- some resource. Our Theorem~1 implies that they can all potentially
- block @{text th} after state @{text s}. We need to make the
- following assumption about the threads in this set:
+ some resource in state @{text s} . Our Them~1 implies that any of
+ those threads can all potentially block @{text th} after state
+ @{text s}. We need to make the following assumption about the
+ threads in the @{text "blockers"}-set:
\begin{quote}
{\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:}
@@ -1671,19 +1673,20 @@
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''.
+ a thread. Our @{text "BND(th')"} binds the number of these ``calls''.
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. To state
- our bound formally, 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 "es @ s"}. For example, suppose
- $\textit{es} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
- \textit{e}_1]$, then the intermediate states from @{text s} upto
- @{text "es @ s"} are
+ blockers} perform (i.e.~events) and how many threads are newly
+ created. To state our bound formally, we need to make a definition
+ of what we mean by intermediate states between a state @{text s} and
+ a future state after @{text s}; they will be the list of states
+ starting from @{text s} upto the state \mbox{@{text "es @ s"}}. For
+ example, suppose $\textit{es} = [\textit{e}_n, \textit{e}_{n-1},
+ \ldots, \textit{e}_2, \textit{e}_1]$, then the intermediate states
+ from @{text s} upto @{text "es @ s"} are
\begin{center}
\begin{tabular}{l}
@@ -1711,59 +1714,77 @@
\begin{theorem}
Given our assumptions about bounds, we have that
-
\[
@{text "len"}\,[@{text "s'"}
\leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \;\;\leq\;\;
@{text "BC"} + \sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}\;.
\]
+ \end{theorem}
- \end{theorem}
+ \noindent This theorem uses Isabelle's list-comprehension notation,
+ which lists all intermediate states between @{text s} and @{text "es
+ @ s"}, and then filters this list according to states in which
+ @{text th} is not running. By calculating the number of elements in
+ the filtered list using the function @{text len}, we have the number
+ of intermediate states in which @{text th} is not running and which
+ by the theorem is bounded by the term on the right-hand side.
\begin{proof} There are two characterisations for the number of
- events in @{text es}: First, for each corresponding state in @{text
- "s upto es"}, either @{text th} is running or not running. That
- means
-
- \begin{equation}\label{firsteq}
- @{text "len es"} =
- @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}] +
- @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+ events in @{text es}: First, in each state in
+ @{text "s upto es"}, clearly either @{text th} is running or
+ not running. Together with @{text "len es = len (s upto es)"}, that
+ implies %
+
+ \begin{equation}
+ \label{firsteq}
+ \begin{array}{lcl}
+ @{text "len es"} & \;=\; &
+ @{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]\\
+ & & +\;
+ @{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+ \end{array}
\end{equation}
\noindent Second by Thm~\ref{mainthm}, the events are either the
actions of @{text th} or @{text "Create"}-events or actions of the
threads in blockers. That is
-
+ %
\begin{equation}\label{secondeq}
- @{text "len es"} = @{text "len (actions_of {th} es)"} +
- @{text "len (filter isCreate es)"} +
- @{text "len (actions_of blockers es)"}
+ \begin{array}{lcl}
+ @{text "len es"} & \;=\; & @{text "len (actions_of {th} es)"}\\
+ & & +\; @{text "len (filter isCreate es)"}\\
+ & & +\; @{text "len (actions_of blockers es)"}
+ \end{array}
\end{equation}
- \noindent
- Further we know that an action of @{text th} can only be taken when @{text th} is running. Therefore
-
+ \noindent Furthermore we know that an action of @{text th} in the
+ intermediate states @{text "s upto es"} can only be taken when
+ @{text th} is running. Therefore
+ %
\[
- @{text "len (actions_of {th} es)"} \leq
- @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
+ @{text "len (actions_of {th} es)"} \;\leq\;
+ @{text len}\,[@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
\]
- \noindent Substituting this into \eqref{firsteq} gives
-
+ \noindent holds. Substituting this into \eqref{firsteq} gives
+ %
\[
- @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
- \leq @{text "len es"} - @{text "len (actions_of {th} es)"}
+ @{text len}\,[@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+ \;\leq\; @{text "len es"} - @{text "len (actions_of {th} es)"}
\]
+ \noindent
into which we can substitute \eqref{secondeq} yielding
-
+ %
\[
- @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq
- @{text "len (filter isCreate es)"} + @{text "len (actions_of blockers es)"}
+ \begin{array}{rcl}
+ @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] & \;\;\leq\;\; &
+ @{text "len (filter isCreate es)"}\\
+ & & \quad + @{text "len (actions_of blockers es)"}
+ \end{array}
\]
- \noindent By our first assumption we know that the @{text
+ \noindent By our first assumption we know that the number of @{text
"Create"}-events are bounded by the bound @{text BC}. By our second
assumption we can prove that the actions of all blockers is bounded
by the sum of bounds of the individual blocking threads, that is
@@ -1777,16 +1798,15 @@
\end{proof}
\noindent This theorem is the main conclusion we obtain for the
- Priority Inheritance Protocol: it shows that the set of @{text blockers}
- is fixed at state @{text s} when @{text th} becomes the thread with
- highest priority. Then 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 from running.
-*}
-(*<*)
-end
-(*>*)
+ Priority Inheritance Protocol. It is based on the fact that the set of
+ @{text blockers} is fixed at state @{text s} when @{text th} becomes
+ the thread with highest priority. Then 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 from running.
+ Our bound does not depend on the restriction of well-nested critical
+ sections in the Priority Inheritance Protocol as imposed by Sha et al.
+ *} (*<*) end (*>*)
section {* Properties for an Implementation\label{implement} *}
@@ -1803,7 +1823,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- HERE?? %%@ {thm children_def2}
+ ?? @{thm children_def}
\end{tabular}
\end{isabelle}
@@ -1813,7 +1833,7 @@
a resource). We can prove the following lemma.
\begin{lemma}\label{childrenlem}
- HERE %@{text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
+ HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
\begin{center}
%@ {thm (concl) cp_rec}.
\end{center}