--- 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.
--- a/Journal/document/root.tex Mon Dec 18 14:52:48 2017 +0000
+++ b/Journal/document/root.tex Tue Dec 19 14:20:29 2017 +0000
@@ -68,25 +68,26 @@
\maketitle
\begin{abstract}
-In real-time systems with threads, resource locking and priority
-sched\-uling, one faces the problem of Priority Inversion. This
-problem can make the behaviour of threads unpredictable and the
-resulting bugs can be hard to find. The Priority Inheritance Protocol
-is one solution implemented in many systems for solving this problem,
-but the correctness of this solution has never been formally verified
-in a theorem prover. As already pointed out in the literature, the
-original informal investigation of the Property Inheritance Protocol
-presents a correctness ``proof'' for an \emph{incorrect} algorithm. In
-this paper we fix the problem of this proof by making all notions
-precise and implementing a variant of a solution proposed earlier. We
-also generalise the scheduling problem to the practically relevant case where
-critical sections can overlap. Our formalisation in Isabelle/HOL not
-just uncovers facts not mentioned in the literature, but also helps
-with implementing efficiently this protocol. Earlier correct
-implementations were criticised as too inefficient. Our formalisation
-is based on Paulson's inductive approach to verifying protocols; our
-implementation builds on top of the small PINTOS operating system used
-for teaching.\medskip
+ In real-time systems with threads, resource locking and priority
+ sched\-uling, one faces the problem of Priority Inversion. This
+ problem can make the behaviour of threads unpredictable and the
+ resulting bugs can be hard to find. The Priority Inheritance
+ Protocol is one solution implemented in many systems for solving
+ this problem, but the correctness of this solution has never been
+ formally verified in a theorem prover. As already pointed out in the
+ literature, the original informal investigation of the Property
+ Inheritance Protocol presents a correctness ``proof'' for an
+ \emph{incorrect} algorithm. In this paper we fix the problem of this
+ proof by making all notions precise and implementing a variant of a
+ solution proposed earlier. We also generalise the scheduling problem
+ to the practically relevant case where critical sections can
+ overlap. Our formalisation in Isabelle/HOL is based on Paulson's
+ inductive approach to verifying protocols. The formalisation not
+ only uncovers facts overlooked in the literature, but also helps
+ with an efficient implementation of this protocol. Earlier correct
+ implementations were criticised as too inefficient. Our
+ implementation builds on top of the small PINTOS operating system
+ used for teaching.\medskip
{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof,
real-time systems, Isabelle/HOL
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/answers.tex Tue Dec 19 14:20:29 2017 +0000
@@ -0,0 +1,121 @@
+\documentclass{article}
+
+\begin{document}
+
+%%%%
+% Reviewer 1.
+\section*{Comments by Reviewer \#1}
+
+
+\begin{itemize}
+\item {\it 1.) I don't see the point of working with a more general
+ library of possibly infinite graphs when it is clear that no
+ (necessarily finite) evolution of the state could ever generate an
+ infinite graph.}
+
+ It seemed the most convenient approach for us and we added the following
+ comment on page 8 about justifying our choice. There was already a
+ comment about having finiteness as a property, rather than a built-in
+ assumption.
+
+ \begin{quote}
+ It seems for our purposes the most convenient representation of
+ graphs are binary relations given by sets of pairs. The pairs
+ stand for the edges in graphs. This relation-based representation
+ has the advantage that the notions \textit{waiting} and
+ \textit{holding} are already defined in terms of relations
+ amongst threads and resources. Also, we can easily re-use the
+ standard notions of transitive closure operations $\_*$ and $\_+$,
+ as well as relation composition for our graphs.
+ \end{quote}
+
+\item {\it 2.) Later, the release function is defined using Hilbert
+ choice (Isabelle/HOL's \texttt{SOME} function) as a method for emulating
+ non-determinism. This is horrid. The highest level generation of
+ traces handles non-determinism beautifully; using choice at a
+ lower level lets you keep things functional, but hides the fact
+ that you want to model non-determinism at the lower level as
+ well. I agree that the final theorem does imply that the way in
+ which the new waiting list is chosen is irrelevant, but this
+ implication is only apparent through a close reading of that
+ definition. Better I think to lift the non-determinism and make it
+ more apparent at the top level.}
+
+ \begin{quote}
+ We generally agree with the reviewer about the use of
+ \texttt{SOME}, but we cannot see a way to make this nondeterminism
+ explicit without complicating too much the topelevel rules.
+ \end{quote}
+
+\item {\it 3. In \S 4, there is an assumption made about the number of
+ threads allowed to be created. Given the form of theorem 2, this
+ seems to me to be unnecessary. It's certainly extremely weird and
+ ugly because it says that there are at most BC many thread
+ creation events in all possible future traces (of which there are
+ of course infinitely many). \ldots}
+
+ We think this mis-reads our theorem: Although the constrains we
+ put on thread creation prohibit the creation of higher priority
+ threads, the creation of lower priority threads may still consume
+ CPU time and prevent \textit{th} from accomplishing its task. That
+ is the purpose we put in the \textit{BC} constraint to limit the
+ overall number of thread creations. We slightly augmented the
+ sentence on page 15 by:
+
+ \begin{quote}
+ Otherwise our PIP scheduler could be ``swamped'' with
+ \textit{Create}-requests of lower priority threads.
+ \end{quote}
+
+
+\item {\it Why are variables corresponding to resources given the name
+ \textit{cs}. This is confusing. \textit{rsc} or \textit{r} would be
+ better.}
+
+ \begin{quote}
+ \textit{cs} stands for ``critical section'', which is the original name
+ used by Sha et al to represent ``critical resources''.
+ \end{quote}
+
+\item All other comments of the reviewer have been implemented.
+
+\end{itemize}
+
+%%%%
+% Reviever 2.
+\section*{Comments by Reviewer \#2}
+
+\begin{itemize}
+\item Well-founded comment: We adpated the paragraph where \textit{acyclic}
+ and \textit{well-founded} are used for the first time.
+
+ \begin{quote}
+ Note that forests can have trees with infinte depth and containing
+ nodes with infinitely many children. A \emph{finite forest} is a
+ forest whose underlying relation is well-founded and every node
+ has finitely many children (is only finitely branching).
+ \end{quote}
+
+ We also added a footnote that we are using the standard definition of
+ well-foundedness from Isabelle.
+
+\item Comment about graph-library: This point was also raised by
+ Reviewer~\#1 and we gave a better justification on page 8 (see
+ answer to first point of Reviewer~\#1).
+
+
+\item {\it 20.) In the case of "Set th prio:", it is not declared what
+ the cprec (e::s) th should be (presumably it is something like
+ Max((prio,|s|),prec th s) or possibly just prec th (e::s) given
+ the assumptions on Set events listed before).}
+
+ We note the concern of the reviewer about the effect of the
+ Set-operation on the \textit{cprec} value of a thread. According to
+ equation (6) on page 11, the \textit{cprec} of a thread is
+ determined by the precedence values in its subtree, while the Set
+ operation only changes the precedence of the `Set' thread. If the
+ reviewer thinks we should add this explanation again, then we are
+ happy to do so.
+
+\end{itemize}
+\end{document}
\ No newline at end of file