--- a/Journal/Paper.thy Fri Feb 23 21:10:49 2018 +0000
+++ b/Journal/Paper.thy Fri Jul 06 22:18:39 2018 +0100
@@ -84,8 +84,8 @@
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
with priority $M$, and so $H$ sits there potentially waiting
- indefinitely (consider the case where threads with propority $M$
- continously need to be processed). Since $H$ is blocked by threads
+ indefinitely (consider the case where threads with priority $M$
+ continuously need to be processed). Since $H$ is blocked by threads
with lower 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.
@@ -94,9 +94,9 @@
can become unpredictable and resulting bugs can be hard to diagnose.
The classic example where this happened is the software that
controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. On
- Earth the software run mostly without any problem, but once the
+ Earth, the software ran mostly without any problem, but once the
spacecraft landed on Mars, it shut down at irregular, but frequent,
- intervals leading to loss of project time as normal operation of the
+ intervals. This led to loss of project time as normal operation of the
craft could only resume the next day (the mission and data already
collected were fortunately not lost, because of a clever system
design). The reason for the shutdowns was that the scheduling
@@ -190,7 +190,7 @@
remaining priority of the threads that it blocks. A similar error
is made in the textbook \cite[Section 2.3.1]{book} which specifies
for a process that inherited a higher priority and exits a critical
- section ``{\it it resumes the priority it had at the point of entry
+ section that ``{\it it resumes the priority it had at the point of entry
into the critical section}''. This error can also be found in the
textbook \cite[Section 16.4.1]{LiYao03} where the authors write
about this process: ``{\it its priority is immediately lowered to the level originally assigned}'';
@@ -198,7 +198,7 @@
more recent textbook \cite[Page 119]{Laplante11} where the authors
state: ``{\it when [the task] exits the critical section that caused
the block, it reverts to the priority it had when it entered that
- section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
+ section}''. The textbook \cite[Page 286]{Liu00} contains a similar
flawed specification and even goes on to develop pseudo-code based
on this flawed specification. Accordingly, the operating system
primitives for inheritance and restoration of priorities in
@@ -208,7 +208,7 @@
how the thread inherited its current priority}'' \cite[Page
527]{Liu00}. Unfortunately, the important information about actually
computing the priority to be restored solely from this log is not
- explained in \cite{Liu00} but left as an ``{\it excercise}'' to the
+ explained in \cite{Liu00} but left as an ``{\it exercise}'' to the
reader. As we shall see, a correct version of PIP does not need to
maintain this (potentially expensive) log data structure at
all. Surprisingly also the widely read and frequently updated
@@ -222,7 +222,7 @@
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
+ exception is the textbook \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
@@ -249,11 +249,11 @@
in PINTOS. This fact, however, is important for an efficient
implementation of PIP, because we can give the lock to the thread
with the highest priority so that it terminates more quickly. We
- are also being able to generalise the scheduler of Sha et
+ are also able to generalise the scheduler of Sha et
al.~\cite{Sha90} to the practically relevant case where critical
sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
an example of this restriction. In the existing literature there is
- no proof and also no proving method that cover this generalised
+ no proof and also no method for proving which covers this generalised
case.
\begin{figure}
@@ -332,7 +332,8 @@
\noindent
whereby threads, priorities and (critical) resources are represented
- as natural numbers. The event @{term Set} models the situation that
+ as natural numbers. In what follows we shall use @{term cs} as a name for
+ critical resources. The event @{term Set} models the situation that
a thread obtains a new priority given by the programmer or
user (for example via the {\tt nice} utility under UNIX). For states
we define the following type-synonym:
@@ -787,7 +788,7 @@
\noindent where @{text "SOME"} stands for Hilbert's epsilon and
implements an arbitrary choice for the next waiting list. It just
- has to be a list of distinctive threads and contains the same
+ has to be a list of distinct threads and contains the same
elements as @{text "qs"} (essentially @{text "qs'"} can be any
reordering of the list @{text "qs"}). This gives for @{term V} the clause:
@@ -802,7 +803,7 @@
Having the scheduler function @{term schs} at our disposal, we can
``lift'', or overload, the notions @{term waiting}, @{term holding},
- @{term RAG}, %%@ {term dependants}
+ @{term RAG}, @{term "TDG"}, %%@ {term dependants}
and @{term cp} to operate on states only.
\begin{isabelle}\ \ \ \ \ %%%
@@ -1627,7 +1628,7 @@
\cite{ZhangUrbanWu12} to leave out this property and let the
programmer take on the responsibility to program threads in such a
benign manner (in addition to causing no circularity in the
- RAG). This leave-it-to-the-programmer was also the approach taken by
+ RAG). This leave-it-to-the-programmer approach was also taken by
Sha et al.~in their paper. However, in this paper we can make an
improvement by establishing a finite bound on the duration of
Priority Inversion measured by the number of events. The events can
@@ -1662,10 +1663,10 @@
\[@{text "len (filter isCreate es) < BC"}\;\]
- wherby @{text es} is a list of events.
+ whereby @{text es} is a list of events.
\end{quote}
- \noindent Note that it is not enough to just to state that there are
+ \noindent Note that it is not enough to just state that there are
only finite number of threads created up until a single state @{text
"s' @ s"} after @{text s}. Instead, we need to put this bound on
the @{text "Create"} events for all valid states after @{text s}.
@@ -1685,8 +1686,8 @@
\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 Thm.~1 implies that any of
- such threads can all potentially block @{text th} after state
+ some resource in state @{text s} . Our Thm.~1 implies that only
+ these 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:
@@ -1716,7 +1717,7 @@
created. To state our bound formally, we need to make a definition
of what we mean by intermediate states between a state @{text s} and
a future state after @{text s}; they will be the list of states
- starting from @{text s} upto the state \mbox{@{text "es @ s"}}. For
+ starting from @{text s} up to the state \mbox{@{text "es @ s"}}. For
example, suppose $\textit{es} = [\textit{e}_n, \textit{e}_{n-1},
\ldots, \textit{e}_2, \textit{e}_1]$, then the intermediate states
from @{text s} upto @{text "es @ s"} are
@@ -1952,8 +1953,8 @@
\noindent The first property is again telling us we do not need to
change the @{text RAG}. The second shows that the @{term cp}-values
of all threads other than @{text th} are unchanged. The reason for
- this is more subtle: Since @{text th} must be running, that is does
- not wait for any resource to be released, it cannot be in any
+ this is more subtle: Since @{text th} must be running, then it does
+ not wait for any resource to be released and it cannot be in any
subtree of any other thread. So all current precedences of other
threads are unchanged.
@@ -2309,15 +2310,15 @@
area of this method is security protocols.
The second goal of our formalisation is to provide a specification for actually
- implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
+ implementing PIP. Textbooks, for example Vahalia \cite[Section 5.6.5]{Vahalia96},
explain how to use various implementations of PIP and abstractly
discuss their properties, but surprisingly lack most details important for a
programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).
That this is an issue in practice is illustrated by the
email from Baker we cited in the Introduction. We achieved also this
goal: The formalisation allowed us to efficently implement our version
- of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86
- architecture. It also gives the first author enough data to enable
+ of PIP on top of PINTOS, a simple instructional operating system for the x86
+ architecture implemented by Pfaff \cite{PINTOS}. It also gives the first author enough data to enable
his undergraduate students to implement PIP (as part of their OS course).
A byproduct of our formalisation effort is that nearly all
design choices for the implementation of PIP scheduler are backed up with a proved
@@ -2337,13 +2338,13 @@
PIP is a scheduling algorithm for single-processor systems. We are
now living in a multi-processor world. Priority Inversion certainly
- occurs also there, see for example \cite{Brandenburg11,Davis11}.
+ occurs also there, see for example work by Brandenburg, and Davis and Burns \cite{Brandenburg11,Davis11}.
However, there is very little ``foundational''
work about PIP-algorithms on multi-processor systems. We are not
aware of any correctness proofs, not even informal ones. There is an
implementation of a PIP-algorithm for multi-processors as part of the
``real-time'' effort in Linux, including an informal description of the implemented scheduling
- algorithm given in \cite{LINUX}. We estimate that the formal
+ algorithm given by Rostedt in \cite{LINUX}. We estimate that the formal
verification of this algorithm, involving more fine-grained events,
is a magnitude harder than the one we presented here, but still
within reach of current theorem proving technology. We leave this
@@ -2353,12 +2354,11 @@
if done informally by ``pencil-and-paper''. We infer this from the flawed proof
in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr
points out an error in a paper about Preemption
- Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
+ Threshold Scheduling by Wang and Saksena \cite{ThreadX}. The use of a theorem prover was
invaluable to us in order to be confident about the correctness of our reasoning
(for example no corner case can be overlooked).
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
+ PVS of the Priority Ceiling Protocol done by Dutertre~\cite{dutertre99b}---another solution to the Priority Inversion
problem, which however needs static analysis of programs in order to
avoid it. There have been earlier formal investigations
into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model