--- a/Journal/Paper.thy Mon Dec 18 14:52:48 2017 +0000
+++ b/Journal/Paper.thy Tue Dec 19 14:20:29 2017 +0000
@@ -79,7 +79,7 @@
$H$ blocks any other thread with lower priority and the thread
itself cannot be blocked indefinitely by threads with lower
priority. Alas, in a naive implementation of resource locking and
- priorities this property can be violated. For this let $L$ be in the
+ priorities, this property can be violated. For this let $L$ be in the
possession of a lock for a resource that $H$ also needs. $H$ must
therefore wait for $L$ to exit the critical section and release this
lock. The problem is that $L$ might in turn be blocked by any thread
@@ -218,24 +218,24 @@
priority.}'' The same error is also repeated later in this popular textbook.
- While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only
- formal publications we have found that specify the incorrect
- behaviour, it seems also many informal descriptions of PIP overlook
- the possibility that another high-priority might wait for a
- low-priority process to finish. A notable exception is the texbook
- \cite{buttazzo}, which gives the correct behaviour of resetting the
- priority of a thread to the highest remaining priority of the
- threads it blocks. This textbook also gives an informal proof for
- the correctness of PIP in the style of Sha et al. Unfortunately,
- this informal proof is too vague to be useful for formalising the
- correctness of PIP and the specification leaves out nearly all
- details in order to implement PIP efficiently.\medskip\smallskip
- %
- %The advantage of formalising the
- %correctness of a high-level specification of PIP in a theorem prover
- %is that such issues clearly show up and cannot be overlooked as in
- %informal reasoning (since we have to analyse all possible behaviours
- %of threads, i.e.~\emph{traces}, that could possibly happen).
+ While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are
+ the only formal publications we have found that specify the
+ incorrect behaviour, it seems also many informal descriptions of the
+ PIP protocol overlook the possibility that another high-priority
+ process might wait for a low-priority process to finish. A notable
+ exception is the texbook \cite{buttazzo}, which gives the correct
+ behaviour of resetting the priority of a thread to the highest
+ remaining priority of the threads it blocks. This textbook also
+ gives an informal proof for the correctness of PIP in the style of
+ Sha et al. Unfortunately, this informal proof is too vague to be
+ useful for formalising the correctness of PIP and the specification
+ leaves out nearly all details in order to implement PIP
+ efficiently.\medskip\smallskip % %The advantage of formalising the
+ %correctness of a high-level specification of PIP in a theorem
+ prover %is that such issues clearly show up and cannot be overlooked
+ as in %informal reasoning (since we have to analyse all possible
+ behaviours %of threads, i.e.~\emph{traces}, that could possibly
+ happen).
\noindent {\bf Contributions:} There have been earlier formal
investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
@@ -452,7 +452,7 @@
taking into account the time when the priority was last set. We order precedences so
that threads with the same priority get a higher precedence if their priority has been
set earlier, since for such threads it is more urgent to finish their work. In an implementation
- this choice would translate to a quite natural FIFO-scheduling of threads with
+ this choice would translate to a quite straightforward FIFO-scheduling of threads with
the same priority.
Moylan et al.~\cite{deinheritance} considered the alternative of
@@ -567,21 +567,21 @@
for example in Figure~\ref{RAGgraph}.
Because of the @{text RAG}s, we will need to formalise some results
- about graphs. While there are few formalisations for graphs already
+ about graphs. While there are a 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 have
a more general theory of graphs which is capable of representing
potentially infinite graphs (in the sense of infinitely branching
and infinite size): the property that our @{text RAG}s are actually
- forests of finitely branching trees having only an finite depth
+ forests of finitely branching trees having only a 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
+ seems for our purposes the most convenient representation 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 has the advantage that the notions
- @{text "waiting"} and @{text "holiding"} are already defined in
- terms of relations amongst theads and resources. Also, we can easily
+ @{text "waiting"} and @{text "holding"} are already defined in
+ terms of relations amongst threads and resources. Also, we can easily
re-use the standard notions for transitive closure operations @{term
"trancl DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
composition for our graphs. A \emph{forest} is defined in our
@@ -632,7 +632,7 @@
The locking mechanism of PIP ensures that for each thread node,
there can be many incoming holding edges in the @{text 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
+ a resource that is locked already, then the thread is blocked and
cannot ask for another resource. Clearly, also every resource can
only have at most one outgoing holding edge---indicating that the
resource is locked. So if the @{text "RAG"} is well-founded and
@@ -684,7 +684,7 @@
threads in the @{text TDG}, we deal correctly with the problem in the informal
algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
lowered prematurely (see Introduction). We again introduce an abbreviation for current
- precedeces of a set of threads, written @{text "cprecs wq s ths"}.
+ precedences of a set of threads, written @{text "cprecs wq s ths"}.
\begin{isabelle}\ \ \ \ \ %%%
@{thm cpreceds_def}
@@ -702,7 +702,7 @@
\noindent
The first function is a waiting queue function (that is, it takes a
resource @{text "cs"} and returns the corresponding list of threads
- that lock, respectively wait for, it); the second is a function that
+ that lock or wait for it); the second is a function that
takes a thread and returns its current precedence (see
the definition in \eqref{cpreced}). We assume the usual getter and setter methods for
such records.
@@ -822,8 +822,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}rcl}
- @{thm (lhs) tG_alt_def} & @{text "\<equiv>"} & @{thm (rhs) tG_alt_def}\\
- @{thm (lhs) cp_s_def} & @{text "\<equiv>"} & @{thm (rhs) cp_s_def}\\
+ @{thm (lhs) tG_alt_def} & @{text "="} & @{thm (rhs) tG_alt_def}\\
+ @{thm (lhs) cp_s_def} & @{text "="} & @{thm (rhs) cp_s_def}\\
\end{tabular}\\
\mbox{}\hfill\numbered{overloaded}
\end{isabelle}
@@ -896,7 +896,7 @@
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
+ lock does not lead to a cycle in the RAG (the purpose 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
@@ -1641,7 +1641,7 @@
@{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 assumptions: first, there is a finite pool of threads
- (active or hibernating) and second, each of them giving up its
+ (active or hibernating) and second, each of these threads will give 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 dispense with the first assumption altogether and allow that
@@ -1649,10 +1649,10 @@
arbitrarily. Consequently, the avoidance of indefinite priority
inversion we are trying to establish is in our model not true,
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 from of lower priority threads.
-So our first assumption states:
+ 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 of lower priority threads. So our first
+ assumption states:
\begin{quote} {\bf Assumption on the number of threads created
after the state {\boldmath@{text s}}:} Given the
@@ -1682,10 +1682,10 @@
@{thm blockers_def[THEN eq_reflection]}
\end{isabelle}
- \noindent This set contains all treads that are not detached in
+ \noindent This set contains all threads 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 in state @{text s} . Our Them~1 implies that any of
+ some resource in state @{text s} . Our Thm.~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:
@@ -1849,7 +1849,7 @@
For example Baker complained that calculating the current precedence
in PIP is quite ``heavy weight'' in Linux (see the Introduction).
In our model of PIP the current precedence of a thread in a state @{text s}
- depends on the precedenes of all threads in its subtree---a ``global'' transitive notion,
+ depends on the precedences of all threads in its subtree---a ``global'' transitive notion,
which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}).
We can however improve upon this. For this recall the notion
of @{term children} of a thread @{text th} defined in \eqref{children}.
@@ -1871,17 +1871,17 @@
computed by considering the static precedence of @{text th}
and
the current precedences of the children of @{text th}. Their
- @{text "cprec"}s, in general general, need to be computed by recursively decending into
+ @{text "cprec"}s, in general, need to be computed by recursively decending into
deeper ``levels'' of the @{text TDG}.
However, the current precedence of a thread @{text th}, say,
only needs to be recomputed when @{text "(i)"} its static
precedence is re-set or when @{text "(ii)"} one of
its children changes its current precedence or when @{text "(iii)"} the children set changes
- (for example in an @{text "V"}-event).
+ (for example in a @{text "V"}-event).
If only the static precedence or the children-set changes, then we can
avoid the recursion and compute the @{text cprec} of @{text th} locally.
In such cases
- the recursion does not need to decend into the corresponding subtree.
+ the recursion does not need to descend into the corresponding subtree.
Once the current
precedence is computed in this more efficient manner, the selection
of the thread with highest precedence from a set of ready threads is
@@ -2044,9 +2044,9 @@
text {*
\noindent
In the other case where there is no thread that takes over @{text cs},
- we can show how
- to recalculate the @{text RAG} and also show that no current precedence needs
- to be recalculated for any thread @{text "th''"}.
+ we can prove that the updated @{text RAG} merely deletes the relevant edge and
+ that no current precedence needs to be recalculated
+ for any thread @{text "th''"}.
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -2235,7 +2235,7 @@
\end{figure}
- Line 6 and 7 of {\tt lock\_acquire} make the operation of acquiring a lock atomic by disabling all
+ Lines 6 and 7 of {\tt lock\_acquire} make the operation of acquiring a lock atomic by disabling all
interrupts, but saving them for resumption at the end of the function (Line 31).
In Line 8, the interesting code with respect to scheduling starts: we
first check whether the lock is already taken (its value is then 0 indicating ``already
@@ -2279,9 +2279,9 @@
Similar operations need to be implementated for the @{ML_text lock_release} function, which
we however do not show. The reader should note though that we did \emph{not} verify our C-code.
This is in contrast, for example, to the work on seL4, which actually verified in Isabelle/HOL
- that their C-code satisfies its specification, thought this specification does not contain
+ that their C-code satisfies its specification, though this specification does not contain
anything about PIP \cite{sel4}.
- Our verification of PIP however provided us with the justification for designing
+ Our verification of PIP however provided us with (formally proven) insights on how to design
the C-code. It gave us confidence that leaving the ``chase'' early, whenever
there is no change in the calculated current precedence, does not break the
correctness of the algorithm.