pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:e4d151d761c4
+:188fe0c81ac7
 ``time-slicing'' threads with equal priority, but found that it does not lead to
 advantages in practice. On the contrary, according to their work having a policy
 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}
+%\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
+%in a state @{term s}. This can be straightforwardly defined in Isabelle as
+%
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-\mbox{\begin{tabular}{@ {}l}
+%\mbox{\begin{tabular}{@ {}l}
-@{thm cntP_def}\\
+%@{thm cntP_def}\\
-@{thm cntV_def}
+%@{thm cntV_def}
-\end{tabular}}
+%\end{tabular}}
-\end{isabelle}
+%\end{isabelle}
+%
-\noindent using the predefined function @{const count} for lists.}
+%\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
 this list (i.e.~the head, or short @{term hd}) is chosen to be the one
 that is in possession of the
 \noindent
 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.
+Because of the RAGs, we will need to formalise some results about
-While there are few formalisations for graphs already implemented in
+graphs.  While there are few formalisations for graphs already
-Isabelle, we choose to introduce our own library of graphs for
+implemented in Isabelle, we choose to introduce our own library of
-PIP. The reason for this is that we wanted to be able to reason with
+graphs for PIP. The justification for this is that we wanted to be able to
-potentially infinite graphs (in the sense of infinitely branching
+reason about potentially infinite graphs (in the sense of infinitely
-and infinite size): the property that our RAGs are actually forrests
+branching and infinite size): the property that our RAGs are
-of finitely branching trees having only an finite depth should be
+actually forrests of finitely branching trees having only an finite
-something we can \emph{prove} for our model of PIP---it should not
+depth should be something we can \emph{prove} for our model of
-be an assumption we build already into our model. It seemed for our
+PIP---it should not be an assumption we build already into our
-purposes the most convenient represeantation of graphs are binary
+model. It seemed for our purposes the most convenient
-relations given by sets of pairs from \eqref{pairs}. The pairs stand for the edges in
+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
+DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
-@{term "DUMMY O DUMMY"}.  A \emph{forrest} is defined as the
+composition.  A \emph{forrest} is defined as the relation @{text
-relation @{text rel} that is \emph{single valued} and
+rel} that is \emph{single valued} and \emph{acyclic}:
-\emph{acyclic}:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm single_valued_def[where ?r="rel", THEN eq_reflection]}\\
 @{thm acyclic_def[where ?r="rel", THEN eq_reflection]}
 \end{tabular}
 \end{isabelle}
 \noindent
-The \emph{children}, \emph{subtree} and \emph{ancestors} of a node in a graph are
+The \emph{children}, \emph{subtree} and \emph{ancestors} of a node in a graph
-defined as
+can be easily defined relationally as
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm children_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
 @{thm subtree_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
 \endnote{
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm rtrancl_path.intros}
 \end{isabelle}
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-@{thm rpath_def}
+%@{thm rpath_def}
-\end{isabelle}}
+%\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
 out going waiting edge.  The reason is that when a thread asks for
 resource that is locked already, then the thread is blocked and
 \begin{center}
 @{thm[mode=Rule] thread_set[where thread=th]}
 \end{center}
-\noindent
+\noindent If a thread wants to lock a resource, then the thread
-If a thread wants to lock a resource, then the thread needs to be
+needs to be running and also we have to make sure that the resource
-running and also we have to make sure that the resource lock does
+lock does not lead to a cycle in the RAG (the prurpose of the second
-not lead to a cycle in the RAG. In practice, ensuring the latter
+premise in the rule below). In practice, ensuring the latter is the
-is the responsibility of the programmer.  In our formal
+responsibility of the programmer.  In our formal model we brush
-model we brush aside these problematic cases in order to be able to make
+aside these problematic cases in order to be able to make some
-some meaningful statements about PIP.\footnote{This situation is
+meaningful statements about PIP.\footnote{This situation is similar
-similar to the infamous \emph{occurs check} in Prolog: In order to say
+to the infamous \emph{occurs check} in Prolog: In order to say
-anything meaningful about unification, one needs to perform an occurs
+anything meaningful about unification, one needs to perform an
-check. But in practice the occurs check is omitted and the
+occurs check. But in practice the occurs check is omitted and the
 responsibility for avoiding problems rests with the programmer.}
 \begin{center}
 @{thm[mode=Rule] thread_P[where thread=th]}
 \end{tabular}
 \end{center}
 \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
 begin
 (*>*)
 priority are created in @{text "s'"}. We will actually prove a
 stronger statement where we also provide the current precedence of
 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:
 \begin{quote}
 {\bf Assumptions on the states {\boldmath@{text s}} and
 {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
 be blocked indefinitely. Of course this can happen if threads with higher priority
 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}
 {If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
 {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
 \noindent This theorem ensures that the thread @{text th}, which has
 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
 show is that any running thread, say @{text "th'"}, has the same
 precedence as @{text th}:
 \begin{center}
 @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}
 \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}
 @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
 \end{center}
 Next we show that a running thread @{text "th'"} must either wait for or
 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
 @{text "s"}, then, according to the definition of detached, @{text
 "th’"} does not hold or wait for any resource. Hence the @{text
 %Since there are only finite many threads live and holding some resource at any moment,
 %if every such thread can release all its resources in finite duration, then after finite
 %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,
 such thread will not block th.
 Their Theorem 3 does not exclude such threads.
 *}
 (*<*)
 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 {*
 While our formalised proof gives us confidence about the correctness of our model of PIP,

changeset 145	188fe0c81ac7
parent 144	e4d151d761c4
child 152	15f4481bc0c9