diff -r 6f50e6a8c6e0 -r a9c0eeb00cc3 Journal/Paper.thy
--- 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