--- a/Journal/Paper.thy Tue Mar 04 09:40:40 2014 +0000
+++ b/Journal/Paper.thy Tue Mar 04 15:27:59 2014 +0000
@@ -28,7 +28,7 @@
original_priority ("priority") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
-
+
(*>*)
section {* Introduction *}
@@ -59,7 +59,8 @@
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}.
- Once the spacecraft landed, the software shut down at irregular
+ On Earth the software run mostly without any problem, but
+ once the spacecraft landed on Mars, it shut down at irregular
intervals leading 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
@@ -136,22 +137,28 @@
presentation of PIP~\cite{Sha90}, despite being informally
``proved'' correct, is actually \emph{flawed}.
- Yodaiken \cite{Yodaiken02} points to a subtlety that had been
+ Yodaiken \cite{Yodaiken02} and also Moylan et al.~\cite{deinheritance}
+ point to a subtlety that had been
overlooked in the informal proof by Sha et al. They specify in
\cite{Sha90} that after the thread (whose priority has been raised)
completes its critical section and releases the lock, it ``returns
to its original priority level.'' This leads them to believe that an
implementation of PIP is ``rather straightforward''~\cite{Sha90}.
- Unfortunately, as Yodaiken points out, this behaviour is too
+ Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too
simplistic. Consider the case where the low priority thread $L$
locks \emph{two} resources, and two high-priority threads $H$ and
$H'$ each wait for one of them. If $L$ releases one resource
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. While
- \cite{Sha90} is the only formal publication we have
- found that describes the incorrect behaviour, not all, but many
+ 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 resumes
+ the priority it had at the point of entry into the critical section''.
+
+ While \cite{book} and
+ \cite{Sha90} are the only formal publication we have
+ found that describe 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.
@@ -683,7 +690,7 @@
taking this assumption into account, the correctness properties of
Sha et al.~are
\emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken
- \cite{Yodaiken02} pointed out: If a low-priority thread possesses
+ \cite{Yodaiken02} and Moylan et al.~\cite{deinheritance} pointed out: If a low-priority thread possesses
locks to two resources for which two high-priority threads are
waiting for, then lowering the priority prematurely after giving up
only one lock, can cause indefinite Priority Inversion for one of the
--- a/Journal/document/root.bib Tue Mar 04 09:40:40 2014 +0000
+++ b/Journal/document/root.bib Tue Mar 04 15:27:59 2014 +0000
@@ -149,6 +149,25 @@
}
+
+
+@TechReport{deinheritance,
+ author = {P.~J.~Moylan and R.~E.~Betz and R.~H.~Middleton},
+ title = {{T}he {P}riority {D}isinheritance {P}roblem},
+ institution = {University of Newcastle},
+ number = {EE9345},
+ year = {1993}
+}
+
+
+@Book{book,
+ author = {R.~Rajkumar},
+ title = {{S}ynchronization in {R}eal-{T}ime {S}ystems:
+ {A} {P}riority {I}nheritance {A}pproach},
+ publisher = {Kluwer},
+ year = {1991}
+}
+
@Article{Lampson80,
author = "B.~W.~Lampson and D.~D.~Redell",
title = "{{E}xperiences with {P}rocesses and {M}onitors in {M}esa}",
Binary file journal.pdf has changed