59   once the spacecraft landed on Mars, it shut down at irregular

    59   once the spacecraft landed on Mars, it shut down at irregular, but frequent,

   115   the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little

   115   the textbooks \cite[Section 12.3.1]{Liu00} and \cite[Section 5.6.5]{Vahalia96}), 

   116   with actual implementations. That this is a problem in practice is

   116   but they help little with actual implementations. That this is a problem in 

   117   proved by an email by Baker, who wrote on 13 July 2009 on the Linux

   117   practice is proved by an email by Baker, who wrote on 13 July 2009 on the Linux

   133   presentation of PIP~\cite{Sha90}, despite being informally

   133   specification of PIP~\cite{Sha90}, despite being informally

   135 

   135   

   136   Yodaiken \cite{Yodaiken02} and also Moylan et al.~\cite{deinheritance} 

   136 

   137   point to a subtlety that had been

   137   Yodaiken \cite{Yodaiken02} and also Moylan et

   138   al.~\cite{deinheritance} point to a subtlety that had been

   140   completes its critical section and releases the lock, it ``{\it returns

   141   completes its critical section and releases the lock, it ``{\it

   141   to its original priority level}''. This leads them to believe that an

   142   returns to its original priority level}''. This leads them to

   142   implementation of PIP is ``{\it rather straightforward}''~\cite{Sha90}.

   143   believe that an implementation of PIP is ``{\it rather

   143   Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too

   144   straightforward}''~\cite{Sha90}.  Unfortunately, as Yodaiken and

   144   simplistic. Moylan et al.~write that there are ``{\it some hidden traps}''. 

   145   Moylan et al.~point out, this behaviour is too simplistic. Moylan et

   145   Consider the case where the low priority thread $L$

   146   al.~write that there are ``{\it some hidden traps}''~\cite{deinheritance}.  Consider the

   146   locks \emph{two} resources, and two high-priority threads $H$ and

   147   case where the low priority thread $L$ locks \emph{two} resources,

   147   $H'$ each wait for one of them.  If $L$ releases one resource

   148   and two high-priority threads $H$ and $H'$ each wait for one of

   148   so that $H$, say, can proceed, then we still have Priority Inversion

   149   them.  If $L$ releases one resource so that $H$, say, can proceed,

   149   with $H'$ (which waits for the other resource). The correct

   150   then we still have Priority Inversion with $H'$ (which waits for the

   150   behaviour for $L$ is to switch to the highest remaining priority of

   151   other resource). The correct behaviour for $L$ is to switch to the

   151   the threads that it blocks. A similar error is made in the textbook

   152   highest remaining priority of the threads that it blocks. 

   152   \cite[Section 2.3.1]{book} which specifies for a process that 

   153   A similar

   153   inherited a higher priority and exits a critical section ``{\it it resumes 

   154   error is made in the textbook \cite[Section 2.3.1]{book} which

   154   the priority it had at the point of entry into the critical section}''.

   155   specifies for a process that inherited a higher priority and exits a

   155   The same error can also be found in the more recent textbook 

   156   critical section ``{\it it resumes the priority it had at the point

   156   \cite[Page 119]{Laplante11} which states ``{\it when [the task] exits the critical 

   157   of entry into the critical section}''.  The same error can also be

   157   section that caused the block, it reverts to the priority it had when 

   158   found in the more recent textbook \cite[Page 119]{Laplante11} where the

   158   it entered that section}''.

   159   authors state: ``{\it when [the task] exits the critical section that caused

   159    

   160   the block, it reverts to the priority it had when it entered that

   160   While \cite{Laplante11,book,Sha90} are the only formal publications we have 

   161   section}''. The textbook \cite[Page 286]{Liu00} contains a simlar

   161   found that describe the incorrect behaviour, not all, but many

   162   flawed specification and even goes on to develop pseudo-code based on this

   162   informal\footnote{informal as in ``found on the Web''} 

   163   flawed specification. Accordingly, the operating system primitives

   163   descriptions of PIP overlook the possibility that another

   164   for inheritance and restoration of priorities in \cite{Liu00} depend on

   165   maintaining a  data structure called \emph{inheritance log}. This log

   166   is maintained for every thread and broadly specified as containing ``{\it

   167   [h]istorical information on how the thread inherited its current

   168   priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important

   169   information about actually

   170   computing the priority to be restored solely from this log is  not explained in

   171   \cite{Liu00} but left as an ``{\it excercise}'' to the reader.

   172   Of course, a correct version of PIP does not need to maintain

   173   this (potentially expensive) data structure at all. 

   174 

   175   

   176   While \cite{Laplante11,Liu00,book,Sha90} are the only formal publications we have 

   177   found that specify the incorrect behaviour, it seems also many

   178   informal descriptions of PIP overlook the possibility that another

   165   The advantage of formalising the

   180   A notable exception is the texbook \cite{buttazzo}, which gives the correct 

   166   correctness of a high-level specification of PIP in a theorem prover

   181   behaviour of resetting the priority of a thread to the highest remaining priority of the 

   167   is that such issues clearly show up and cannot be overlooked as in

   182   threads it blocks. This textbook also gives an informal proof for 

   168   informal reasoning (since we have to analyse all possible behaviours

   183   the correctness of PIP in the style of Sha et al. Unfortunately, this informal 

   169   of threads, i.e.~\emph{traces}, that could possibly happen).\medskip\smallskip

   184   proof is too vague to be useful for formalising the correctness of PIP

   185   and the specification leaves out nearly all details in order 

   186   to implement PIP efficiently.\medskip\smallskip

   187   %

   188   %The advantage of formalising the

   189   %correctness of a high-level specification of PIP in a theorem prover

   190   %is that such issues clearly show up and cannot be overlooked as in

   191   %informal reasoning (since we have to analyse all possible behaviours

   192   %of threads, i.e.~\emph{traces}, that could possibly happen).

   189   sections can overlap; see Figure~\ref{overlap} below for an example of 

   212   sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of 

   190   this restriction. In the existing literature there is no 

   213   this restriction. %In the existing literature there is no 

   191   proof and also no proving method that cover this generalised case.

   214   %proof and also no proving method that cover this generalised case.