53   can interact in subtle ways leading to a problem, called

    53   can interact in subtle ways leading to a problem, called

    54   \emph{Priority Inversion}. Suppose three threads having priorities

    54   \emph{Priority Inversion}. Suppose three threads having priorities

    55   $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread

    55   $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread

    56   $H$ blocks any other thread with lower priority and itself cannot

    56   $H$ blocks any other thread with lower priority and itself cannot

    57   be blocked by any thread with lower priority. Alas, in a naive

    57   be blocked by any thread with lower priority. Alas, in a naive

    59   be violated. Even worse, $H$ can be delayed indefinitely by

    59   be violated. Even worse, $H$ can be delayed indefinitely by

    60   threads with lower priorities. For this let $L$ be in the

    60   threads with lower priorities. For this let $L$ be in the

    62   therefore wait for $L$ to exit the critical section and release this

    62   therefore wait for $L$ to exit the critical section and release this

    63   lock. The problem is that $L$ might in turn be blocked by any

    63   lock. The problem is that $L$ might in turn be blocked by any

    64   thread with priority $M$, and so $H$ sits there potentially waiting

    64   thread with priority $M$, and so $H$ sits there potentially waiting

    65   indefinitely. Since $H$ is blocked by threads with lower

    65   indefinitely. Since $H$ is blocked by threads with lower

    66   priorities, the problem is called Priority Inversion. It was first

    66   priorities, the problem is called Priority Inversion. It was first

    74   Once the spacecraft landed, the software shut down at irregular

    74   Once the spacecraft landed, the software shut down at irregular

    75   intervals leading to loss of project time as normal operation of the

    75   intervals leading to loss of project time as normal operation of the

    76   craft could only resume the next day (the mission and data already

    76   craft could only resume the next day (the mission and data already

    77   collected were fortunately not lost, because of a clever system

    77   collected were fortunately not lost, because of a clever system

    78   design).  The reason for the shutdowns was that the scheduling

    78   design).  The reason for the shutdowns was that the scheduling

    80   locking a resource prevented a high priority thread from running in

    80   locking a resource prevented a high priority thread from running in

    82   rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)

    82   rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)

    83   \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority

    83   \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority

    84   Inheritance Protocol} \cite{Sha90} and others sometimes also call it

    84   Inheritance Protocol} \cite{Sha90} and others sometimes also call it

    85   \emph{Priority Boosting}.} in the scheduling software.

    85   \emph{Priority Boosting}.} in the scheduling software.

    86 

    86 

   112   \it{}``Priority inheritance is neither efficient nor reliable. Implementations

   112   \it{}``Priority inheritance is neither efficient nor reliable. Implementations

   113   are either incomplete (and unreliable) or surprisingly complex and intrusive.''

   113   are either incomplete (and unreliable) or surprisingly complex and intrusive.''

   114   \end{quote}

   114   \end{quote}

   115 

   115 

   116   \noindent

   116   \noindent

   118   sections to be preempted. Unfortunately, this solution does not

   118   sections to be preempted. Unfortunately, this solution does not

   119   help in real-time systems with hard deadlines for high-priority 

   119   help in real-time systems with hard deadlines for high-priority 

   120   threads.

   120   threads.

   121 

   121 

   122   In our opinion, there is clearly a need for investigating correct

   122   In our opinion, there is clearly a need for investigating correct

   134   range of events, including priority changes and interruptions of

   134   range of events, including priority changes and interruptions of

   135   wait operations.''

   135   wait operations.''

   136   \end{quote}

   136   \end{quote}

   137 

   137 

   138   \noindent

   138   \noindent

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

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

   144   ``proved'' correct, is actually \emph{flawed}. 

   144   ``proved'' correct, is actually \emph{flawed}. 

   145 

   145 

   146   Yodaiken \cite{Yodaiken02} points to a subtlety that had been

   146   Yodaiken \cite{Yodaiken02} points to a subtlety that had been

   147   overlooked in the informal proof by Sha et al. They specify in

   147   overlooked in the informal proof by Sha et al. They specify in

   153   simplistic.  Consider the case where the low priority thread $L$

   153   simplistic.  Consider the case where the low priority thread $L$

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

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

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

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

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

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

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

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

   159   the threads that it blocks. The advantage of formalising the

   159   the threads that it blocks. The advantage of formalising the

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

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

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

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

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

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

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

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

   171   al.~\cite{Sha90} is flawed).  In contrast to model checking, our

   171   al.~\cite{Sha90} is flawed).  In contrast to model checking, our

   172   formalisation provides insight into why PIP is correct and allows us

   172   formalisation provides insight into why PIP is correct and allows us

   173   to prove stronger properties that, as we will show, can inform an

   173   to prove stronger properties that, as we will show, can inform an

   174   efficient implementation.  For example, we found by ``playing'' with the formalisation

   174   efficient implementation.  For example, we found by ``playing'' with the formalisation

   175   that the choice of the next thread to take over a lock when a

   175   that the choice of the next thread to take over a lock when a

   178 *}

   178 *}

   179 

   179 

   180 section {* Formal Model of the Priority Inheritance Protocol *}

   180 section {* Formal Model of the Priority Inheritance Protocol *}

   181 

   181 

   182 text {*

   182 text {*

   510   \end{tabular}

   510   \end{tabular}

   511   \end{isabelle}

   511   \end{isabelle}

   512 

   512 

   513   \noindent

   513   \noindent

   514   With these abbreviations in place we can introduce 

   514   With these abbreviations in place we can introduce 

   516   that do not wait for any resource) and the running thread.

   516   that do not wait for any resource) and the running thread.

   517 

   517 

   518   \begin{isabelle}\ \ \ \ \ %%%

   518   \begin{isabelle}\ \ \ \ \ %%%

   519   \begin{tabular}{@ {}l}

   519   \begin{tabular}{@ {}l}

   520   @{thm readys_def}\\

   520   @{thm readys_def}\\

   536   @{thm holdents_def}

   536   @{thm holdents_def}

   537   \end{isabelle}

   537   \end{isabelle}

   538 

   538 

   539   Finally we can define what a \emph{valid state} is in our model of PIP. For

   539   Finally we can define what a \emph{valid state} is in our model of PIP. For

   540   example we cannot expect to be able to exit a thread, if it was not

   540   example we cannot expect to be able to exit a thread, if it was not

   542   These validity constraints on states are characterised by the

   542   These validity constraints on states are characterised by the

   543   inductive predicate @{term "step"} and @{term vt}. We first give five inference rules

   543   inductive predicate @{term "step"} and @{term vt}. We first give five inference rules

   544   for @{term step} relating a state and an event that can happen next.

   544   for @{term step} relating a state and an event that can happen next.

   545 

   545 

   546   \begin{center}

   546   \begin{center}

   625   of time, then indefinite Priority Inversion cannot occur---the high-priority

   625   of time, then indefinite Priority Inversion cannot occur---the high-priority

   626   thread is guaranteed to run eventually. The assumption is that

   626   thread is guaranteed to run eventually. The assumption is that

   627   programmers must ensure that threads are programmed in this way.  However, even

   627   programmers must ensure that threads are programmed in this way.  However, even

   628   taking this assumption into account, the correctness properties of

   628   taking this assumption into account, the correctness properties of

   629   Sha et al.~are

   629   Sha et al.~are

   631   \cite{Yodaiken02} pointed out: If a low-priority thread possesses

   631   \cite{Yodaiken02} pointed out: If a low-priority thread possesses

   632   locks to two resources for which two high-priority threads are

   632   locks to two resources for which two high-priority threads are

   633   waiting for, then lowering the priority prematurely after giving up

   633   waiting for, then lowering the priority prematurely after giving up

   634   only one lock, can cause indefinite Priority Inversion for one of the

   634   only one lock, can cause indefinite Priority Inversion for one of the

   635   high-priority threads, invalidating their two bounds.

   635   high-priority threads, invalidating their two bounds.

   732   However, we are able to combine their two separate bounds into a

   732   However, we are able to combine their two separate bounds into a

   733   single theorem improving their bound.

   733   single theorem improving their bound.

   734 

   734 

   735   In what follows we will describe properties of PIP that allow us to prove 

   735   In what follows we will describe properties of PIP that allow us to prove 

   736   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 

   736   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 

   738 

   738 

   739   \begin{isabelle}\ \ \ \ \ %%%

   739   \begin{isabelle}\ \ \ \ \ %%%

   740   \begin{tabular}{@ {}l}

   740   \begin{tabular}{@ {}l}

   741   @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\

   741   @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\

   742   @{thm[mode=IfThen]  finite_threads}

   742   @{thm[mode=IfThen]  finite_threads}

   774   \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.

   774   \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.

   775   \end{tabular}

   775   \end{tabular}

   776   \end{isabelle}

   776   \end{isabelle}

   777 

   777 

   778   \noindent

   778   \noindent

   780   @{text step}; similarly the finiteness and well-foundedness property.

   780   @{text step}; similarly the finiteness and well-foundedness property.

   781   The last two properties establish that every thread in a @{text "RAG"}

   781   The last two properties establish that every thread in a @{text "RAG"}

   782   (either holding or waiting for a resource) is a live thread.

   782   (either holding or waiting for a resource) is a live thread.

   783 

   783 

   784   The key lemma in our proof of Theorem~\ref{mainthm} is as follows:

   784   The key lemma in our proof of Theorem~\ref{mainthm} is as follows:

   785 

   785 

   786   \begin{lemma}\label{mainlem}

   786   \begin{lemma}\label{mainlem}

   787   Given the assumptions about states @{text "s"} and @{text "s' @ s"},

   787   Given the assumptions about states @{text "s"} and @{text "s' @ s"},

   788   the thread @{text th} and the events in @{text "s'"},

   788   the thread @{text th} and the events in @{text "s'"},

   790   then @{text "th' \<notin> running (s' @ s)"}.

   790   then @{text "th' \<notin> running (s' @ s)"}.

   791   \end{lemma}

   791   \end{lemma}

   792 

   792 

   793   \noindent

   793   \noindent

   794   The point of this lemma is that a thread different from @{text th} (which has the highest

   794   The point of this lemma is that a thread different from @{text th} (which has the highest

   976   @{thm children_def2}

   976   @{thm children_def2}

   977   \end{tabular}

   977   \end{tabular}

   978   \end{isabelle}

   978   \end{isabelle}

   979 

   979 

   980   \noindent

   980   \noindent

   982   @{text th} in the @{term RAG} (and waiting for @{text th} to release

   982   @{text th} in the @{term RAG} (and waiting for @{text th} to release

   983   a resource). We can prove the following lemma.

   983   a resource). We can prove the following lemma.

   984 

   984 

   985   \begin{lemma}\label{childrenlem}

   985   \begin{lemma}\label{childrenlem}

   986   @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}

   986   @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}

  1188 text {*

  1188 text {*

  1189   \noindent

  1189   \noindent

  1190   As can be seen, a pleasing byproduct of our formalisation is that the properties in

  1190   As can be seen, a pleasing byproduct of our formalisation is that the properties in

  1191   this section closely inform an implementation of PIP, namely whether the

  1191   this section closely inform an implementation of PIP, namely whether the

  1192   @{text RAG} needs to be reconfigured or current precedences need to

  1192   @{text RAG} needs to be reconfigured or current precedences need to

  1194 *}

  1194 *}

  1195 

  1195 

  1196 section {* Conclusion *}

  1196 section {* Conclusion *}

  1197 

  1197 

  1198 text {* 

  1198 text {* 

  1267   code with a few apply-scripts interspersed. The formal model of PIP

  1267   code with a few apply-scripts interspersed. The formal model of PIP

  1268   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1268   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1269   definitions and proofs span over 770 lines of code. The properties relevant

  1269   definitions and proofs span over 770 lines of code. The properties relevant

  1270   for an implementation require 2000 lines. The code of our formalisation 

  1270   for an implementation require 2000 lines. The code of our formalisation 

  1271   can be downloaded from

  1271   can be downloaded from

  1273 

  1273 

  1274   \bibliographystyle{plain}

  1274   \bibliographystyle{plain}

  1275   \bibliography{root}

  1275   \bibliography{root}

  1276 *}

  1276 *}

  1277 

  1277