--- a/Journal/Paper.thy Fri Feb 28 12:49:58 2014 +0000
+++ b/Journal/Paper.thy Mon Mar 03 16:22:48 2014 +0000
@@ -54,7 +54,7 @@
priorities, the problem is called Priority Inversion. It was first
described in \cite{Lampson80} in the context of the
Mesa programming language designed for concurrent programming.
-
+
If the problem of Priority Inversion is ignored, real-time systems
can become unpredictable and resulting bugs can be hard to diagnose.
The classic example where this happened is the software that
@@ -81,17 +81,19 @@
Inversion problem, PIP is one that is widely deployed and
implemented. This includes VxWorks (a proprietary real-time OS used
in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
- ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
+ ASIMO robot, etc.) and ThreadX (another proprietary real-time OS
+ used in HP inkjet printers \cite{ThreadX}), but also
+ the POSIX 1003.1c Standard realised for
example in libraries for FreeBSD, Solaris and Linux.
- Two advantages of PIP are that increasing the priority of a thread
- can be performed dynamically by the scheduler and is deterministic.
+ Two advantages of PIP are that it is deterministic and that increasing the priority of a thread
+ can be performed dynamically by the scheduler.
This is in contrast to \emph{Priority Ceiling}
\cite{Sha90}, another solution to the Priority Inversion problem,
which requires static analysis of the program in order to prevent
- Priority Inversion, and also to the Windows NT scheduler, which avoids
- this problem by randomly boosting the priority of ready (low priority) threads
- (e.g.~\cite{WINDOWSNT}).
+ Priority Inversion, and also in contrast to the Windows NT scheduler, which avoids
+ this problem by randomly boosting the priority of ready low-priority threads
+ (see for instance~\cite{WINDOWSNT}).
However, there has also been strong criticism against
PIP. For instance, PIP cannot prevent deadlocks when lock
dependencies are circular, and also blocking times can be
@@ -147,14 +149,17 @@
so that $H$, say, can proceed, then we still have Priority Inversion
with $H'$ (which waits for the other resource). The correct
behaviour for $L$ is to switch to the highest remaining priority of
- the threads that it blocks. The advantage of formalising the
+ the threads that it blocks. While
+ \cite{Sha90} is the only formal publication we have
+ found that describes the incorrect behaviour, not all, but many
+ informal\footnote{informal as in ``found on the Web''}
+ descriptions of PIP overlook the possibility that another
+ high-priority might wait for a low-priority process to finish.
+ 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).\footnote{While
- \cite{Sha90} is the only formal publication we have
- found that describes the incorrect behaviour, not all, but many
- informal descriptions of PIP overlook the case...}\medskip
+ of threads, i.e.~\emph{traces}, that could possibly happen).\medskip\smallskip
\noindent
{\bf Contributions:} There have been earlier formal investigations
@@ -326,10 +331,8 @@
@{thm cs_depend_def}
\end{isabelle}
- \noindent
- If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:
- \begin{figure}[ph]
+ \begin{figure}[t]
\begin{center}
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
\begin{tikzpicture}[scale=1]
@@ -368,6 +371,9 @@
\end{figure}
\noindent
+ If there is no cycle, then every RAG can be pictured as a forrest of trees, as
+ for example in Figure~\ref{RAGgraph}.
+
We will design our scheduler
so that every thread can be in the possession of several resources, that is
it has potentially several incoming holding edges in the RAG, but has at most one outgoing
@@ -1008,7 +1014,6 @@
text {*
While our formalised proof gives us confidence about the correctness of our model of PIP,
we found that the formalisation can even help us with efficiently implementing it.
-
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}
@@ -1250,12 +1255,7 @@
This lemma states that if an intermediate @{term cp}-value does not change, then
the procedure can also stop, because none of its dependent threads will
have their current precedence changed.
- *}
-(*<*)
-end
-(*>*)
-text {*
- \noindent
+ *}(*<*)end(*>*)text {*
As can be seen, a pleasing byproduct of our formalisation is that the properties in
this section closely inform an implementation of PIP, namely whether the
RAG needs to be reconfigured or current precedences need to
@@ -1288,7 +1288,7 @@
them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
for accessing and updating. In the code we shall describe below, we use the function
@{ML_text "queue_insert"}, for inserting a new element into a priority queue, and
- @{ML_text "queue_update"}, for updating the position of an element that is already
+ the function @{ML_text "queue_update"}, for updating the position of an element that is already
in a queue. Both functions take an extra argument that specifies the
comparison function used for organising the priority queue.
@@ -1314,7 +1314,7 @@
- \begin{figure}[t]
+ \begin{figure}[tph]
\begin{lstlisting}
void lock_acquire (struct lock *lock)
{ ASSERT (lock != NULL);
@@ -1459,6 +1459,12 @@
within reach of current theorem proving technology. We leave this
for future work.
+ To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult
+ if done informally by ``pencil-and-paper''. This is proved by the flawed proof
+ in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who
+ pointed out an error in a paper about Preemption
+ Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
+ invaluable to us in order to feel confident about the correctness of our results.
The most closely related work to ours is the formal verification in
PVS of the Priority Ceiling Protocol done by Dutertre
\cite{dutertre99b}---another solution to the Priority Inversion
@@ -1478,9 +1484,9 @@
is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
definitions and proofs span over 770 lines of code. The properties relevant
for an implementation require 2000 lines.
- %The code of our formalisation
- %can be downloaded from
- %\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
+ The code of our formalisation
+ can be downloaded from the Mercurial repository at
+ \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
%\medskip