--- 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 {*