(*<*)+
−
theory Paper+
−
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"+
−
begin+
−
ML {*+
−
  open Printer;+
−
  show_question_marks_default := false;+
−
  *}+
−
+
−
notation (latex output)+
−
  Cons ("_::_" [78,77] 73) and+
−
  vt ("valid'_state") and+
−
  runing ("running") and+
−
  birthtime ("last'_set") and+
−
  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and+
−
  Prc ("'(_, _')") and+
−
  holding ("holds") and+
−
  waiting ("waits") and+
−
  Th ("T") and+
−
  Cs ("C") and+
−
  readys ("ready") and+
−
  depend ("RAG") and +
−
  preced ("prec") and+
−
  cpreced ("cprec") and+
−
  dependents ("dependants") and+
−
  cp ("cprec") and+
−
  holdents ("resources") and+
−
  original_priority ("priority") and+
−
  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
  Many real-time systems need to support threads involving priorities and+
−
  locking of resources. Locking of resources ensures mutual exclusion+
−
  when accessing shared data or devices that cannot be+
−
  preempted. Priorities allow scheduling of threads that need to+
−
  finish their work within deadlines.  Unfortunately, both features+
−
  can interact in subtle ways leading to a problem, called+
−
  \emph{Priority Inversion}. Suppose three threads having priorities+
−
  $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread+
−
  $H$ blocks any other thread with lower priority and itself cannot+
−
  be blocked by any thread with lower priority. Alas, in a naive+
−
  implementation of resource looking and priorities this property can+
−
  be violated. Even worse, $H$ can be delayed indefinitely by+
−
  threads with lower priorities. For this let $L$ be in the+
−
  possession of a lock for a resource that also $H$ needs. $H$ must+
−
  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. 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.+
−
+
−
  If the problem of Priority Inversion is ignored, real-time systems+
−
  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+
−
  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+
−
  design).  The reason for the shutdowns was that the scheduling+
−
  software fell victim of Priority Inversion: a low priority thread+
−
  locking a resource prevented a high priority thread from running in+
−
  time leading to a system reset. Once the problem was found, it was+
−
  rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)+
−
  \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority+
−
  Inheritance Protocol} \cite{Sha90} and others sometimes also call it+
−
  \emph{Priority Boosting}.} in the scheduling software.+
−
+
−
  The idea behind PIP is to let the thread $L$ temporarily inherit+
−
  the high priority from $H$ until $L$ leaves the critical section+
−
  unlocking the resource. This solves the problem of $H$ having to+
−
  wait indefinitely, because $L$ cannot be blocked by threads having+
−
  priority $M$. While a few other solutions exist for the Priority+
−
  Inversion problem, PIP is one that is widely deployed and+
−
  implemented. This includes VxWorks (a proprietary real-time OS used+
−
  in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's+
−
  ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for+
−
  example in libraries for FreeBSD, Solaris and Linux.+
−
+
−
  One advantage of PIP is that increasing the priority of a thread+
−
  can be dynamically calculated by the scheduler. This is in contrast+
−
  to, for example, \emph{Priority Ceiling} \cite{Sha90}, another+
−
  solution to the Priority Inversion problem, which requires static+
−
  analysis of the program in order to prevent Priority+
−
  Inversion. However, there has also been strong criticism against+
−
  PIP. For instance, PIP cannot prevent deadlocks when lock+
−
  dependencies are circular, and also blocking times can be+
−
  substantial (more than just the duration of a critical section).+
−
  Though, most criticism against PIP centres around unreliable+
−
  implementations and PIP being too complicated and too inefficient.+
−
  For example, Yodaiken writes in \cite{Yodaiken02}:+
−
+
−
  \begin{quote}+
−
  \it{}``Priority inheritance is neither efficient nor reliable. Implementations+
−
  are either incomplete (and unreliable) or surprisingly complex and intrusive.''+
−
  \end{quote}+
−
+
−
  \noindent+
−
  He suggests to avoid PIP altogether by not allowing critical+
−
  sections to be preempted. Unfortunately, this solution does not+
−
  help in real-time systems with hard deadlines for high-priority +
−
  threads.+
−
+
−
  In our opinion, there is clearly a need for investigating correct+
−
  algorithms for PIP. A few specifications for PIP exist (in English)+
−
  and also a few high-level descriptions of implementations (e.g.~in+
−
  the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little+
−
  with actual implementations. That this is a problem in practise is+
−
  proved by an email from Baker, who wrote on 13 July 2009 on the Linux+
−
  Kernel mailing list:+
−
+
−
  \begin{quote}+
−
  \it{}``I observed in the kernel code (to my disgust), the Linux PIP+
−
  implementation is a nightmare: extremely heavy weight, involving+
−
  maintenance of a full wait-for graph, and requiring updates for a+
−
  range of events, including priority changes and interruptions of+
−
  wait operations.''+
−
  \end{quote}+
−
+
−
  \noindent+
−
  The criticism by Yodaiken, Baker and others suggests to us to look+
−
  again at PIP from a more abstract level (but still concrete enough+
−
  to inform an implementation), and makes PIP an ideal candidate for a+
−
  formal verification. One reason, of course, is that the original+
−
  presentation of PIP~\cite{Sha90}, despite being informally+
−
  ``proved'' correct, is actually \emph{flawed}. +
−
+
−
  Yodaiken \cite{Yodaiken02} points 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+
−
  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 revert to the highest remaining priority of+
−
  the threads that it blocks. The advantage of formalising the+
−
  correctness of a high-level specification of PIP in a theorem prover+
−
  is that such issues clearly show up and cannot be overlooked as in+
−
  informal reasoning (since we have to analyse all possible behaviours+
−
  of threads, i.e.~\emph{traces}, that could possibly happen).\medskip+
−
+
−
  \noindent+
−
  {\bf Contributions:} There have been earlier formal investigations+
−
  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model+
−
  checking techniques. This paper presents a formalised and+
−
  mechanically checked proof for the correctness of PIP (to our+
−
  knowledge the first one; the earlier informal proof by Sha et+
−
  al.~\cite{Sha90} is flawed).  In contrast to model checking, our+
−
  formalisation provides insight into why PIP is correct and allows us+
−
  to prove stronger properties that, as we will show, inform an+
−
  implementation.  For example, we found by ``playing'' with the formalisation+
−
  that the choice of the next thread to take over a lock when a+
−
  resource is released is irrelevant for PIP being correct. Something+
−
  which has not been mentioned in the relevant literature.+
−
*}+
−
+
−
section {* Formal Model of the Priority Inheritance Protocol *}+
−
+
−
text {*+
−
  The Priority Inheritance Protocol, short PIP, is a scheduling+
−
  algorithm for a single-processor system.\footnote{We shall come back+
−
  later to the case of PIP on multi-processor systems.} Our model of+
−
  PIP is based on Paulson's inductive approach to protocol+
−
  verification \cite{Paulson98}, where the \emph{state} of a system is+
−
  given by a list of events that happened so far.  \emph{Events} of PIP fall+
−
  into five categories defined as the datatype:+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}+
−
  \isacommand{datatype} event +
−
  & @{text "="} & @{term "Create thread priority"}\\+
−
  & @{text "|"} & @{term "Exit thread"} \\+
−
  & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\+
−
  & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\+
−
  & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}+
−
  \end{tabular}}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  whereby threads, priorities and (critical) resources are represented+
−
  as natural numbers. 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).  As in Paulson's work, we+
−
  need to define functions that allow us to make some observations+
−
  about states.  One, called @{term threads}, calculates the set of+
−
  ``live'' threads that we have seen so far:+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \mbox{\begin{tabular}{lcl}+
−
  @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & +
−
    @{thm (rhs) threads.simps(1)}\\+
−
  @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) threads.simps(2)[where thread="th"]}\\+
−
  @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) threads.simps(3)[where thread="th"]}\\+
−
  @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\+
−
  \end{tabular}}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  In this definition @{term "DUMMY # DUMMY"} stands for list-cons.+
−
  Another function calculates the priority for a thread @{text "th"}, which is +
−
  defined as+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \mbox{\begin{tabular}{lcl}+
−
  @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\+
−
  @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\+
−
  @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\+
−
  @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\+
−
  \end{tabular}}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  In this definition we set @{text 0} as the default priority for+
−
  threads that have not (yet) been created. The last function we need +
−
  calculates the ``time'', or index, at which time a process had its +
−
  priority last set.+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \mbox{\begin{tabular}{lcl}+
−
  @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\+
−
  @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\+
−
  @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & +
−
    @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\+
−
  @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\+
−
  \end{tabular}}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  In this definition @{term "length s"} stands for the length of the list+
−
  of events @{text s}. Again the default value in this function is @{text 0}+
−
  for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a +
−
  state @{text s} is the pair of natural numbers defined as+
−
  +
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{thm preced_def[where thread="th"]}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The point of precedences is to schedule threads not according to priorities (because what should+
−
  we do in case two threads have the same priority), but according to precedences. +
−
  Precedences allow us to always discriminate between two threads with equal priority by +
−
  taking into account the time when the priority was last set. We order precedences so +
−
  that threads with the same priority get a higher precedence if their priority has been +
−
  set earlier, since for such threads it is more urgent to finish their work. In an implementation+
−
  this choice would translate to a quite natural FIFO-scheduling of processes with +
−
  the same priority.+
−
+
−
  Next, we introduce the concept of \emph{waiting queues}. They are+
−
  lists of threads associated with every resource. The first thread in+
−
  this list (i.e.~the head, or short @{term hd}) is chosen to be the one +
−
  that is in possession of the+
−
  ``lock'' of the corresponding resource. We model waiting queues as+
−
  functions, below abbreviated as @{text wq}. They take a resource as+
−
  argument and return a list of threads.  This allows us to define+
−
  when a thread \emph{holds}, respectively \emph{waits} for, a+
−
  resource @{text cs} given a waiting queue function @{text wq}.+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm cs_holding_def[where thread="th"]}\\+
−
  @{thm cs_waiting_def[where thread="th"]}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  In this definition we assume @{text "set"} converts a list into a set.+
−
  At the beginning, that is in the state where no thread is created yet, +
−
  the waiting queue function will be the function that returns the+
−
  empty list for every resource.+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{abbrev all_unlocked}\hfill\numbered{allunlocked}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} +
−
  (RAG), which represent the dependencies between threads and resources.+
−
  We represent RAGs as relations using pairs of the form+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}+
−
  @{term "(Cs cs, Th th)"}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  where the first stands for a \emph{waiting edge} and the second for a +
−
  \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a +
−
  datatype for vertices). Given a waiting queue function, a RAG is defined +
−
  as+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{thm cs_depend_def}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  Given three threads and three resources, an instance of a RAG is as follows:+
−
+
−
  \begin{center}+
−
  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}+
−
  \begin{tikzpicture}[scale=1]+
−
  %%\draw[step=2mm] (-3,2) grid (1,-1);+
−
+
−
  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};+
−
  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};+
−
  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};+
−
  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};+
−
  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};+
−
  \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};+
−
  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};+
−
+
−
  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);+
−
  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);+
−
  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);+
−
  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);+
−
  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);+
−
  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);+
−
  \end{tikzpicture}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The use of relations for representing RAGs allows us to conveniently define+
−
  the notion of the \emph{dependants} of a thread. This is defined as+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{thm cs_dependents_def}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  This definition needs to account for all threads that wait for a thread to+
−
  release a resource. This means we need to include threads that transitively+
−
  wait for a resource being released (in the picture above this means the dependants+
−
  of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, but also @{text "th\<^isub>3"}, +
−
  which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which+
−
  in turn needs to wait for @{text "th\<^isub>1"} to finish). If there is a circle in a RAG, then clearly+
−
  we have a deadlock. Therefore when a thread requests a resource,+
−
  we must ensure that the resulting RAG is not circular. +
−
+
−
  Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a +
−
  state @{text s}. It is defined as+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{thm cpreced_def2}\hfill\numbered{cpreced}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  While the precedence @{term prec} of a thread is determined by the programmer +
−
  (for example when the thread is+
−
  created), the point of the current precedence is to let scheduler increase this+
−
  priority, if needed according to PIP. Therefore the current precedence of @{text th} is+
−
  given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all +
−
  processes that are dependants of @{text th}. Since the notion @{term "dependants"} is+
−
  defined as the transitive closure of all dependent threads, we deal correctly with the +
−
  problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is+
−
  lowered prematurely.+
−
  +
−
  The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined+
−
  by recursion on the state (a list of events); @{term "schs"} returns a \emph{schedule state}, which +
−
  we represent as a record consisting of two+
−
  functions:+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The first function is a waiting queue function (that is it takes a resource @{text "cs"} and returns the+
−
  corresponding list of threads that wait for it), the second is a function that takes+
−
  a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and +
−
  setter methods for such records.+
−
+
−
  In the initial state, the scheduler starts with all resources unlocked (see \eqref{allunlocked}) and the+
−
  current precedence of every thread is initialised with @{term "Prc 0 0"}; that means +
−
  \mbox{@{abbrev initial_cprec}}. Therefore+
−
  we have+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ +
−
  \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:+
−
  we calculate the waiting queue function of the (previous) state @{text s}; +
−
  this waiting queue function @{text wq} is unchanged in the next schedule state---because+
−
  none of these events lock or release any resources; +
−
  for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function +
−
  @{term cpreced}. This gives the following three clauses for @{term schs}:+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ +
−
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+
−
  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\+
−
  @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\+
−
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+
−
  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\+
−
  @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ +
−
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+
−
  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent +
−
  More interesting are the cases when a resource, say @{text cs}, is locked or released. In these cases+
−
  we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update+
−
  the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th} +
−
  appended to the end of that list (remember the head of this list is seen to be in the possession of this+
−
  resource).+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ +
−
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+
−
  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\+
−
  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function+
−
  so that the thread that possessed the lock is deleted from the corresponding thread list. For this +
−
  list transformation, we use+
−
  the auxiliary function @{term release}. A simple version of @{term release} would+
−
  just delete this thread and return the rest, namely+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lcl}+
−
  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\+
−
  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  In practice, however, often the thread with the highest precedence in the list will get the+
−
  lock next. We have implemented this choice, but later found out that the choice +
−
  of which thread is chosen next is actually irrelevant for the correctness of PIP.+
−
  Therefore we prove the stronger result where @{term release} is defined as+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lcl}+
−
  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\+
−
  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  @{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+
−
  contain the same elements as @{text "qs"}. This gives for @{term V} the clause:+
−
 +
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\+
−
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+
−
  \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\+
−
  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  Having the scheduler function @{term schs} at our disposal, we can ``lift'', or+
−
  overload, the notions+
−
  @{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}rcl}+
−
  @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\+
−
  @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\+
−
  @{thm (lhs) s_depend_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\+
−
  @{thm (lhs) cp_def}        & @{text "\<equiv>"} & @{thm (rhs) cp_def}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  With these abbreviations we can introduce +
−
  the notion of threads being @{term readys} in a state (i.e.~threads+
−
  that do not wait for any resource) and the running thread.+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm readys_def}\\+
−
  @{thm runing_def}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  In this definition @{term "f ` S"} stands for the set @{text S} under the image of the +
−
  function @{text f}. +
−
  Note that in the initial case, that is where the list of events is empty, the set +
−
  @{term threads} is empty and therefore there is no thread ready nor a running.+
−
  If there is one or more threads ready, then there can only be \emph{one} thread+
−
  running, namely the one whose current precedence is equal to the maximum of all ready +
−
  threads. We use the set-comprehension to capture both possibilities.+
−
  We can now also define the set of resources that are locked by a thread in any+
−
  given state.+
−
+
−
  \begin{isabelle}\ \ \ \ \ %%%+
−
  @{thm holdents_def}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  These resources are given by the holding edges in the RAG.+
−
+
−
  Finally we can define what a \emph{valid state} is in our PIP. For+
−
  example we cannot expect to be able to exit a thread, if it was not+
−
  created yet. These validity constraints are characterised by the+
−
  inductive predicate @{term "step"}. We give five inference rules+
−
  relating a state and an event that can happen next.+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}+
−
  @{thm[mode=Rule] thread_exit[where thread=th]}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The first rule states that a thread can only be created, if it does not yet exists.+
−
  Similarly, the second rule states that a thread can only be terminated if it was+
−
  running and does not lock any resources anymore (to simplify ). The event @{text Set} can happen+
−
  if the corresponding thread is running. +
−
+
−
  \begin{center}+
−
  @{thm[mode=Rule] thread_set[where thread=th]}+
−
  \end{center}+
−
+
−
  \noindent+
−
  If a thread wants to lock a resource, then the thread needs to be+
−
  running and also we have to make sure that the resource lock does+
−
  not lead to a cycle in the RAG. In practice, ensuring the latter is+
−
  of course the responsibility of the programmer.  Here in our formal+
−
  model we just exclude such problematic cases in order to make+
−
  some meaningful statements about PIP.\footnote{This situation is+
−
  similar to the infamous occurs check in Prolog: in order to say+
−
  anything meaningful about unification, we need to perform an occurs+
−
  check; but in practice the occurs check is ommited and the+
−
  responsibility to avoid problems rests with the programmer.}+
−
  Similarly, if a thread wants to release a lock on a resource, then+
−
  it must be running and in the possession of that lock. This is+
−
  formally given by the last two inference rules of @{term step}.+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\+
−
  @{thm[mode=Rule] thread_V[where thread=th]}\\+
−
  \end{tabular}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  A valid state of PIP can then be conveniently be defined as follows:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Axiom] vt_nil}\hspace{1cm}+
−
  @{thm[mode=Rule] vt_cons}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  This completes our formal model of PIP. In the next section we present+
−
  properties that show our version of PIP is correct.+
−
*}+
−
+
−
section {* Correctness Proof *}+
−
+
−
+
−
(*<*)+
−
context extend_highest_gen+
−
begin+
−
(*>*)+
−
+
−
print_locale extend_highest_gen+
−
thm extend_highest_gen_def+
−
thm extend_highest_gen_axioms_def+
−
thm highest_gen_def+
−
text {* +
−
  Main lemma+
−
+
−
  \begin{enumerate}+
−
  \item @{term "s"} is a valid state (@{text "vt_s"}):+
−
    @{thm  vt_s}.+
−
  \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):+
−
    @{thm threads_s}.+
−
  \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):+
−
    @{thm highest}.+
−
  \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):+
−
    @{thm preced_th}.+
−
 +
−
  \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.+
−
  \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore+
−
    its precedence can not be higher than @{term "th"},  therefore+
−
    @{term "th"} remain to be the one with the highest precedence+
−
    (@{text "create_low"}):+
−
    @{thm [display] create_low}+
−
  \item Any adjustment of priority in +
−
    @{term "t"} does not happen to @{term "th"} and +
−
    the priority set is no higher than @{term "prio"}, therefore+
−
    @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):+
−
    @{thm [display] set_diff_low}+
−
  \item Since we are investigating what happens to @{term "th"}, it is assumed +
−
    @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):+
−
    @{thm [display] exit_diff}+
−
  \end{enumerate}+
−
+
−
  \begin{lemma}+
−
  @{thm[mode=IfThen] moment_blocked}+
−
  \end{lemma}+
−
+
−
  \begin{theorem}+
−
  @{thm[mode=IfThen] runing_inversion_2}+
−
  \end{theorem}+
−
+
−
  \begin{theorem}+
−
  @{thm[mode=IfThen] runing_inversion_3}+
−
  \end{theorem}+
−
  +
−
+
−
+
−
TO DO +
−
+
−
*}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
section {* Properties for an Implementation *}+
−
+
−
text {* TO DO *}+
−
+
−
section {* Conclusion *}+
−
+
−
text {* +
−
  The Priority Inheritance Protocol is a classic textbook algorithm+
−
  used in real-time systems in order to avoid the problem of Priority+
−
  Inversion.+
−
+
−
  A clear and simple understanding of the problem at hand is both a+
−
  prerequisite and a byproduct of such an effort, because everything+
−
  has finally be reduced to the very first principle to be checked+
−
  mechanically.+
−
+
−
  Our formalisation and the one presented+
−
  in \cite{Wang09} are the only ones that employ Paulson's method for+
−
  verifying protocols which are \emph{not} security related. +
−
+
−
  TO DO +
−
+
−
  no clue about multi-processor case according to \cite{Steinberg10} +
−
+
−
*}+
−
+
−
text {*+
−
  \bigskip+
−
  The priority inversion phenomenon was first published in+
−
  \cite{Lampson80}.  The two protocols widely used to eliminate+
−
  priority inversion, namely PI (Priority Inheritance) and PCE+
−
  (Priority Ceiling Emulation), were proposed in \cite{Sha90}. PCE is+
−
  less convenient to use because it requires static analysis of+
−
  programs. Therefore, PI is more commonly used in+
−
  practice\cite{locke-july02}. However, as pointed out in the+
−
  literature, the analysis of priority inheritance protocol is quite+
−
  subtle\cite{yodaiken-july02}.  A formal analysis will certainly be+
−
  helpful for us to understand and correctly implement PI. All+
−
  existing formal analysis of PI+
−
  \cite{Jahier09,Wellings07,Faria08} are based on the+
−
  model checking technology. Because of the state explosion problem,+
−
  model check is much like an exhaustive testing of finite models with+
−
  limited size.  The results obtained can not be safely generalized to+
−
  models with arbitrarily large size. Worse still, since model+
−
  checking is fully automatic, it give little insight on why the+
−
  formal model is correct. It is therefore definitely desirable to+
−
  analyze PI using theorem proving, which gives more general results+
−
  as well as deeper insight. And this is the purpose of this paper+
−
  which gives a formal analysis of PI in the interactive theorem+
−
  prover Isabelle using Higher Order Logic (HOL). The formalization+
−
  focuses on on two issues:+
−
+
−
  \begin{enumerate}+
−
  \item The correctness of the protocol model itself. A series of desirable properties is +
−
    derived until we are fully convinced that the formal model of PI does +
−
    eliminate priority inversion. And a better understanding of PI is so obtained +
−
    in due course. For example, we find through formalization that the choice of +
−
    next thread to take hold when a +
−
    resource is released is irrelevant for the very basic property of PI to hold. +
−
    A point never mentioned in literature. +
−
  \item The correctness of the implementation. A series of properties is derived the meaning +
−
    of which can be used as guidelines on how PI can be implemented efficiently and correctly. +
−
  \end{enumerate} +
−
+
−
  The rest of the paper is organized as follows: Section \ref{overview} gives an overview +
−
  of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} +
−
  discusses a series of basic properties of PI. Section \ref{extension} shows formally +
−
  how priority inversion is controlled by PI. Section \ref{implement} gives properties +
−
  which can be used for guidelines of implementation. Section \ref{related} discusses +
−
  related works. Section \ref{conclusion} concludes the whole paper.+
−
+
−
  The basic priority inheritance protocol has two problems:+
−
+
−
  It does not prevent a deadlock from happening in a program with circular lock dependencies.+
−
  +
−
  A chain of blocking may be formed; blocking duration can be substantial, though bounded.+
−
+
−
+
−
  Contributions+
−
+
−
  Despite the wide use of Priority Inheritance Protocol in real time operating+
−
  system, it's correctness has never been formally proved and mechanically checked. +
−
  All existing verification are based on model checking technology. Full automatic+
−
  verification gives little help to understand why the protocol is correct. +
−
  And results such obtained only apply to models of limited size. +
−
  This paper presents a formal verification based on theorem proving. +
−
  Machine checked formal proof does help to get deeper understanding. We found +
−
  the fact which is not mentioned in the literature, that the choice of next +
−
  thread to take over when an critical resource is release does not affect the correctness+
−
  of the protocol. The paper also shows how formal proof can help to construct +
−
  correct and efficient implementation.\bigskip +
−
+
−
*}+
−
+
−
section {* An overview of priority inversion and priority inheritance \label{overview} *}+
−
+
−
text {*+
−
+
−
  Priority inversion refers to the phenomenon when a thread with high priority is blocked +
−
  by a thread with low priority. Priority happens when the high priority thread requests +
−
  for some critical resource already taken by the low priority thread. Since the high +
−
  priority thread has to wait for the low priority thread to complete, it is said to be +
−
  blocked by the low priority thread. Priority inversion might prevent high priority +
−
  thread from fulfill its task in time if the duration of priority inversion is indefinite +
−
  and unpredictable. Indefinite priority inversion happens when indefinite number +
−
  of threads with medium priorities is activated during the period when the high +
−
  priority thread is blocked by the low priority thread. Although these medium +
−
  priority threads can not preempt the high priority thread directly, they are able +
−
  to preempt the low priority threads and cause it to stay in critical section for +
−
  an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. +
−
  +
−
  Priority inheritance is one protocol proposed to avoid indefinite priority inversion. +
−
  The basic idea is to let the high priority thread donate its priority to the low priority +
−
  thread holding the critical resource, so that it will not be preempted by medium priority +
−
  threads. The thread with highest priority will not be blocked unless it is requesting +
−
  some critical resource already taken by other threads. Viewed from a different angle, +
−
  any thread which is able to block the highest priority threads must already hold some +
−
  critical resource. Further more, it must have hold some critical resource at the +
−
  moment the highest priority is created, otherwise, it may never get change to run and +
−
  get hold. Since the number of such resource holding lower priority threads is finite, +
−
  if every one of them finishes with its own critical section in a definite duration, +
−
  the duration the highest priority thread is blocked is definite as well. The key to +
−
  guarantee lower priority threads to finish in definite is to donate them the highest +
−
  priority. In such cases, the lower priority threads is said to have inherited the +
−
  highest priority. And this explains the name of the protocol: +
−
  {\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.+
−
+
−
  The objectives of this paper are:+
−
  \begin{enumerate}+
−
  \item Build the above mentioned idea into formal model and prove a series of properties +
−
    until we are convinced that the formal model does fulfill the original idea. +
−
  \item Show how formally derived properties can be used as guidelines for correct +
−
    and efficient implementation.+
−
  \end{enumerate}+
−
  The proof is totally formal in the sense that every detail is reduced to the +
−
  very first principles of Higher Order Logic. The nature of interactive theorem +
−
  proving is for the human user to persuade computer program to accept its arguments. +
−
  A clear and simple understanding of the problem at hand is both a prerequisite and a +
−
  byproduct of such an effort, because everything has finally be reduced to the very +
−
  first principle to be checked mechanically. The former intuitive explanation of +
−
  Priority Inheritance is just such a byproduct. +
−
  *}+
−
+
−
section {* Formal model of Priority Inheritance \label{model} *}+
−
text {*+
−
  \input{../../generated/PrioGDef}+
−
*}+
−
+
−
section {* General properties of Priority Inheritance \label{general} *}+
−
+
−
text {*+
−
  The following are several very basic prioprites:+
−
  \begin{enumerate}+
−
  \item All runing threads must be ready (@{text "runing_ready"}):+
−
          @{thm[display] "runing_ready"}  +
−
  \item All ready threads must be living (@{text "readys_threads"}):+
−
          @{thm[display] "readys_threads"} +
−
  \item There are finite many living threads at any moment (@{text "finite_threads"}):+
−
          @{thm[display] "finite_threads"} +
−
  \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): +
−
          @{thm[display] "wq_distinct"} +
−
  \item All threads in waiting queues are living threads (@{text "wq_threads"}): +
−
          @{thm[display] "wq_threads"} +
−
  \item The event which can get a thread into waiting queue must be @{term "P"}-events+
−
         (@{text "block_pre"}): +
−
          @{thm[display] "block_pre"}   +
−
  \item A thread may never wait for two different critical resources+
−
         (@{text "waiting_unique"}): +
−
          @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}+
−
  \item Every resource can only be held by one thread+
−
         (@{text "held_unique"}): +
−
          @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}+
−
  \item Every living thread has an unique precedence+
−
         (@{text "preced_unique"}): +
−
          @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}+
−
  \end{enumerate}+
−
*}+
−
+
−
text {* \noindent+
−
  The following lemmas show how RAG is changed with the execution of events:+
−
  \begin{enumerate}+
−
  \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):+
−
    @{thm[display] depend_set_unchanged}+
−
  \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):+
−
    @{thm[display] depend_create_unchanged}+
−
  \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):+
−
    @{thm[display] depend_exit_unchanged}+
−
  \item Execution of @{term "P"} (@{text "step_depend_p"}):+
−
    @{thm[display] step_depend_p}+
−
  \item Execution of @{term "V"} (@{text "step_depend_v"}):+
−
    @{thm[display] step_depend_v}+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  These properties are used to derive the following important results about RAG:+
−
  \begin{enumerate}+
−
  \item RAG is loop free (@{text "acyclic_depend"}):+
−
  @{thm [display] acyclic_depend}+
−
  \item RAGs are finite (@{text "finite_depend"}):+
−
  @{thm [display] finite_depend}+
−
  \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):+
−
  @{thm [display] wf_dep_converse}+
−
  \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):+
−
  @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}+
−
  \item All threads in RAG are living threads +
−
    (@{text "dm_depend_threads"} and @{text "range_in"}):+
−
    @{thm [display] dm_depend_threads range_in}+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  The following lemmas show how every node in RAG can be chased to ready threads:+
−
  \begin{enumerate}+
−
  \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):+
−
    @{thm [display] chain_building[rule_format]}+
−
  \item The ready thread chased to is unique (@{text "dchain_unique"}):+
−
    @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  Properties about @{term "next_th"}:+
−
  \begin{enumerate}+
−
  \item The thread taking over is different from the thread which is releasing+
−
  (@{text "next_th_neq"}):+
−
  @{thm [display] next_th_neq}+
−
  \item The thread taking over is unique+
−
  (@{text "next_th_unique"}):+
−
  @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}  +
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  Some deeper results about the system:+
−
  \begin{enumerate}+
−
  \item There can only be one running thread (@{text "runing_unique"}):+
−
  @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}+
−
  \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):+
−
  @{thm [display] max_cp_eq}+
−
  \item There must be one ready thread having the max @{term "cp"}-value +
−
  (@{text "max_cp_readys_threads"}):+
−
  @{thm [display] max_cp_readys_threads}+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  The relationship between the count of @{text "P"} and @{text "V"} and the number of +
−
  critical resources held by a thread is given as follows:+
−
  \begin{enumerate}+
−
  \item The @{term "V"}-operation decreases the number of critical resources +
−
    one thread holds (@{text "cntCS_v_dec"})+
−
     @{thm [display]  cntCS_v_dec}+
−
  \item The number of @{text "V"} never exceeds the number of @{text "P"} +
−
    (@{text "cnp_cnv_cncs"}):+
−
    @{thm [display]  cnp_cnv_cncs}+
−
  \item The number of @{text "V"} equals the number of @{text "P"} when +
−
    the relevant thread is not living:+
−
    (@{text "cnp_cnv_eq"}):+
−
    @{thm [display]  cnp_cnv_eq}+
−
  \item When a thread is not living, it does not hold any critical resource +
−
    (@{text "not_thread_holdents"}):+
−
    @{thm [display] not_thread_holdents}+
−
  \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant +
−
    thread does not hold any critical resource, therefore no thread can depend on it+
−
    (@{text "count_eq_dependents"}):+
−
    @{thm [display] count_eq_dependents}+
−
  \end{enumerate}+
−
  *}+
−
+
−
section {* Key properties \label{extension} *}+
−
+
−
(*<*)+
−
context extend_highest_gen+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this +
−
  purpose, we need to investigate what happens after one thread takes the highest precedence. +
−
  A locale is used to describe such a situation, which assumes:+
−
  \begin{enumerate}+
−
  \item @{term "s"} is a valid state (@{text "vt_s"}):+
−
    @{thm  vt_s}.+
−
  \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):+
−
    @{thm threads_s}.+
−
  \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):+
−
    @{thm highest}.+
−
  \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):+
−
    @{thm preced_th}.+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  Under these assumptions, some basic priority can be derived for @{term "th"}:+
−
  \begin{enumerate}+
−
  \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):+
−
    @{thm [display] eq_cp_s_th}+
−
  \item The current precedence of @{term "th"} is the highest precedence in +
−
    the system (@{text "highest_cp_preced"}):+
−
    @{thm [display] highest_cp_preced}+
−
  \item The precedence of @{term "th"} is the highest precedence +
−
    in the system (@{text "highest_preced_thread"}):+
−
    @{thm [display] highest_preced_thread}+
−
  \item The current precedence of @{term "th"} is the highest current precedence +
−
    in the system (@{text "highest'"}):+
−
    @{thm [display] highest'}+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  To analysis what happens after state @{term "s"} a sub-locale is defined, which +
−
  assumes:+
−
  \begin{enumerate}+
−
  \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.+
−
  \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore+
−
    its precedence can not be higher than @{term "th"},  therefore+
−
    @{term "th"} remain to be the one with the highest precedence+
−
    (@{text "create_low"}):+
−
    @{thm [display] create_low}+
−
  \item Any adjustment of priority in +
−
    @{term "t"} does not happen to @{term "th"} and +
−
    the priority set is no higher than @{term "prio"}, therefore+
−
    @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):+
−
    @{thm [display] set_diff_low}+
−
  \item Since we are investigating what happens to @{term "th"}, it is assumed +
−
    @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):+
−
    @{thm [display] exit_diff}+
−
  \end{enumerate}+
−
*}+
−
+
−
text {* \noindent+
−
  All these assumptions are put into a predicate @{term "extend_highest_gen"}. +
−
  It can be proved that @{term "extend_highest_gen"} holds +
−
  for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):+
−
  @{thm [display] red_moment}+
−
  +
−
  From this, an induction principle can be derived for @{text "t"}, so that +
−
  properties already derived for @{term "t"} can be applied to any prefix +
−
  of @{text "t"} in the proof of new properties +
−
  about @{term "t"} (@{text "ind"}):+
−
  \begin{center}+
−
  @{thm[display] ind}+
−
  \end{center}+
−
+
−
  The following properties can be proved about @{term "th"} in @{term "t"}:+
−
  \begin{enumerate}+
−
  \item In @{term "t"}, thread @{term "th"} is kept live and its +
−
    precedence is preserved as well+
−
    (@{text "th_kept"}): +
−
    @{thm [display] th_kept}+
−
  \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among +
−
    all living threads+
−
    (@{text "max_preced"}): +
−
    @{thm [display] max_preced}+
−
  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence+
−
    among all living threads+
−
    (@{text "th_cp_max_preced"}): +
−
    @{thm [display] th_cp_max_preced}+
−
  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current +
−
    precedence among all living threads+
−
    (@{text "th_cp_max"}): +
−
    @{thm [display] th_cp_max}+
−
  \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment +
−
    @{term "s"}+
−
    (@{text "th_cp_preced"}): +
−
    @{thm [display] th_cp_preced}+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  The main theorem of this part is to characterizing the running thread during @{term "t"} +
−
  (@{text "runing_inversion_2"}):+
−
  @{thm [display] runing_inversion_2}+
−
  According to this, if a thread is running, it is either @{term "th"} or was+
−
  already live and held some resource +
−
  at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).+
−
+
−
  Since there are only finite many threads live and holding some resource at any moment,+
−
  if every such thread can release all its resources in finite duration, then after finite+
−
  duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen+
−
  then.+
−
  *}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
section {* Properties to guide implementation \label{implement} *}+
−
+
−
text {*+
−
  The properties (especially @{text "runing_inversion_2"}) convinced us that the model defined +
−
  in Section \ref{model} does prevent indefinite priority inversion and therefore fulfills +
−
  the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper +
−
  is to show how this model can be used to guide a concrete implementation. As discussed in+
−
  Section 5.6.5 of \cite{Vahalia96}, the implementation of Priority Inheritance in Solaris +
−
  uses sophisticated linking data structure. Except discussing two scenarios to show how+
−
  the data structure should be manipulated, a lot of details of the implementation are missing. +
−
  In \cite{Faria08,Jahier09,Wellings07} the protocol is described formally +
−
  using different notations, but little information is given on how this protocol can be +
−
  implemented efficiently, especially there is no information on how these data structure +
−
  should be manipulated. +
−
+
−
  Because the scheduling of threads is based on current precedence, +
−
  the central issue in implementation of Priority Inheritance is how to compute the precedence+
−
  correctly and efficiently. As long as the precedence is correct, it is very easy to +
−
  modify the scheduling algorithm to select the correct thread to execute. +
−
+
−
  First, it can be proved that the computation of current precedence @{term "cp"} of a threads+
−
  only involves its children (@{text "cp_rec"}):+
−
  @{thm [display] cp_rec} +
−
  where @{term "children s th"} represents the set of children of @{term "th"} in the current+
−
  RAG: +
−
  \[+
−
  @{thm (lhs) children_def} @{text "\<equiv>"} @{thm (rhs) children_def}+
−
  \]+
−
  where the definition of @{term "child"} is: +
−
  \[ @{thm (lhs) child_def} @{text "\<equiv>"}  @{thm (rhs) child_def}+
−
  \]+
−
+
−
  The aim of this section is to fill the missing details of how current precedence should+
−
  be changed with the happening of events, with each event type treated by one subsection,+
−
  where the computation of @{term "cp"} uses lemma @{text "cp_rec"}.+
−
  *}+
−
 +
−
subsection {* Event @{text "Set th prio"} *}+
−
+
−
(*<*)+
−
context step_set_cps+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The context under which event @{text "Set th prio"} happens is formalized as follows:+
−
  \begin{enumerate}+
−
    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.+
−
    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies +
−
      event @{text "Set th prio"} is eligible to happen under state @{term "s'"} and+
−
      state @{term "s'"} is a valid state.+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  Under such a context, we investigated how the current precedence @{term "cp"} of +
−
  threads change from state @{term "s'"} to @{term "s"} and obtained the following+
−
  conclusions:+
−
  \begin{enumerate}+
−
  %% \item The RAG does not change (@{text "eq_dep"}): @{thm "eq_dep"}.+
−
  \item All threads with no dependence relation with thread @{term "th"} have their+
−
    @{term "cp"}-value unchanged (@{text "eq_cp"}):+
−
    @{thm [display] eq_cp}+
−
    This lemma implies the @{term "cp"}-value of @{term "th"}+
−
    and those threads which have a dependence relation with @{term "th"} might need+
−
    to be recomputed. The way to do this is to start from @{term "th"} +
−
    and follow the @{term "depend"}-chain to recompute the @{term "cp"}-value of every +
−
    encountered thread using lemma @{text "cp_rec"}. +
−
    Since the @{term "depend"}-relation is loop free, this procedure +
−
    can always stop. The the following lemma shows this procedure actually could stop earlier.+
−
  \item The following two lemma shows, if a thread the re-computation of which+
−
    gives an unchanged @{term "cp"}-value, the procedure described above can stop. +
−
    \begin{enumerate}+
−
      \item Lemma @{text "eq_up_self"} shows if the re-computation of+
−
        @{term "th"}'s @{term "cp"} gives the same result, the procedure can stop:+
−
        @{thm [display] eq_up_self}+
−
      \item Lemma @{text "eq_up"}) shows if the re-computation at intermediate threads+
−
        gives unchanged result, the procedure can stop:+
−
        @{thm [display] eq_up}+
−
  \end{enumerate}+
−
  \end{enumerate}+
−
  *}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
subsection {* Event @{text "V th cs"} *}+
−
+
−
(*<*)+
−
context step_v_cps_nt+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The context under which event @{text "V th cs"} happens is formalized as follows:+
−
  \begin{enumerate}+
−
    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.+
−
    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies +
−
      event @{text "V th cs"} is eligible to happen under state @{term "s'"} and+
−
      state @{term "s'"} is a valid state.+
−
  \end{enumerate}+
−
  *}+
−
+
−
text {* \noindent+
−
  Under such a context, we investigated how the current precedence @{term "cp"} of +
−
  threads change from state @{term "s'"} to @{term "s"}. +
−
+
−
+
−
  Two subcases are considerted, +
−
  where the first is that there exits @{term "th'"} +
−
  such that +
−
  @{thm [display] nt} +
−
  holds, which means there exists a thread @{term "th'"} to take over+
−
  the resource release by thread @{term "th"}. +
−
  In this sub-case, the following results are obtained:+
−
  \begin{enumerate}+
−
  \item The change of RAG is given by lemma @{text "depend_s"}: +
−
  @{thm [display] "depend_s"}+
−
  which shows two edges are removed while one is added. These changes imply how+
−
  the current precedences should be re-computed.+
−
  \item First all threads different from @{term "th"} and @{term "th'"} have their+
−
  @{term "cp"}-value kept, therefore do not need a re-computation+
−
  (@{text "cp_kept"}): @{thm [display] cp_kept}+
−
  This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"}+
−
  need to be recomputed.+
−
  \end{enumerate}+
−
  *}+
−
+
−
(*<*)+
−
end+
−
+
−
context step_v_cps_nnt+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The other sub-case is when for all @{text "th'"}+
−
  @{thm [display] nnt}+
−
  holds, no such thread exists. The following results can be obtained for this +
−
  sub-case:+
−
  \begin{enumerate}+
−
  \item The change of RAG is given by lemma @{text "depend_s"}:+
−
  @{thm [display] depend_s}+
−
  which means only one edge is removed.+
−
  \item In this case, no re-computation is needed (@{text "eq_cp"}):+
−
  @{thm [display] eq_cp}+
−
  \end{enumerate}+
−
  *}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
+
−
subsection {* Event @{text "P th cs"} *}+
−
+
−
(*<*)+
−
context step_P_cps_e+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The context under which event @{text "P th cs"} happens is formalized as follows:+
−
  \begin{enumerate}+
−
    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.+
−
    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies +
−
      event @{text "P th cs"} is eligible to happen under state @{term "s'"} and+
−
      state @{term "s'"} is a valid state.+
−
  \end{enumerate}+
−
+
−
  This case is further divided into two sub-cases. The first is when @{thm ee} holds.+
−
  The following results can be obtained:+
−
  \begin{enumerate}+
−
  \item One edge is added to the RAG (@{text "depend_s"}):+
−
    @{thm [display] depend_s}+
−
  \item No re-computation is needed (@{text "eq_cp"}):+
−
    @{thm [display] eq_cp}+
−
  \end{enumerate}+
−
*}+
−
+
−
(*<*)+
−
end+
−
+
−
context step_P_cps_ne+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The second is when @{thm ne} holds.+
−
  The following results can be obtained:+
−
  \begin{enumerate}+
−
  \item One edge is added to the RAG (@{text "depend_s"}):+
−
    @{thm [display] depend_s}+
−
  \item Threads with no dependence relation with @{term "th"} do not need a re-computation+
−
    of their @{term "cp"}-values (@{text "eq_cp"}):+
−
    @{thm [display] eq_cp}+
−
    This lemma implies all threads with a dependence relation with @{term "th"} may need +
−
    re-computation.+
−
  \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier+
−
    (@{text "eq_up"}):+
−
    @{thm [display] eq_up}+
−
  \end{enumerate}+
−
+
−
  *}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
subsection {* Event @{text "Create th prio"} *}+
−
+
−
(*<*)+
−
context step_create_cps+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The context under which event @{text "Create th prio"} happens is formalized as follows:+
−
  \begin{enumerate}+
−
    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.+
−
    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies +
−
      event @{text "Create th prio"} is eligible to happen under state @{term "s'"} and+
−
      state @{term "s'"} is a valid state.+
−
  \end{enumerate}+
−
  The following results can be obtained under this context:+
−
  \begin{enumerate}+
−
  \item The RAG does not change (@{text "eq_dep"}):+
−
    @{thm [display] eq_dep}+
−
  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):+
−
    @{thm [display] eq_cp}+
−
  \item The @{term "cp"}-value of @{term "th"} equals its precedence +
−
    (@{text "eq_cp_th"}):+
−
    @{thm [display] eq_cp_th}+
−
  \end{enumerate}+
−
+
−
*}+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
subsection {* Event @{text "Exit th"} *}+
−
+
−
(*<*)+
−
context step_exit_cps+
−
begin+
−
(*>*)+
−
+
−
text {*+
−
  The context under which event @{text "Exit th"} happens is formalized as follows:+
−
  \begin{enumerate}+
−
    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.+
−
    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies +
−
      event @{text "Exit th"} is eligible to happen under state @{term "s'"} and+
−
      state @{term "s'"} is a valid state.+
−
  \end{enumerate}+
−
  The following results can be obtained under this context:+
−
  \begin{enumerate}+
−
  \item The RAG does not change (@{text "eq_dep"}):+
−
    @{thm [display] eq_dep}+
−
  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):+
−
    @{thm [display] eq_cp}+
−
  \end{enumerate}+
−
  Since @{term th} does not live in state @{term "s"}, there is no need to compute +
−
  its @{term cp}-value.+
−
*}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−
+
−
+
−
section {* Related works \label{related} *}+
−
+
−
text {*+
−
  \begin{enumerate}+
−
  \item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}+
−
    \cite{Wellings07} models and verifies the combination of Priority Inheritance (PI) and +
−
    Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine +
−
    using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed +
−
    formal model of combined PI and PCE is given, the number of properties is quite +
−
    small and the focus is put on the harmonious working of PI and PCE. Most key features of PI +
−
    (as well as PCE) are not shown. Because of the limitation of the model checking technique+
−
    used there, properties are shown only for a small number of scenarios. Therefore, +
−
    the verification does not show the correctness of the formal model itself in a +
−
    convincing way.  +
−
  \item {\em Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC}+
−
    \cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown +
−
    for PI using model checking. The limitation of model checking is intrinsic to the work.+
−
  \item {\em Synchronous modeling and validation of priority inheritance schedulers}+
−
    \cite{Jahier09}. Gives a formal model+
−
    of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked +
−
    several properties using model checking. The number of properties shown there is +
−
    less than here and the scale is also limited by the model checking technique. +
−
  \item {\em The Priority Ceiling Protocol: Formalization and Analysis Using PVS}+
−
    \cite{dutertre99b}. Formalized another protocol for Priority Inversion in the +
−
    interactive theorem proving system PVS.+
−
\end{enumerate}+
−
+
−
+
−
  There are several works on inversion avoidance:+
−
  \begin{enumerate}+
−
  \item {\em Solving the group priority inversion problem in a timed asynchronous system}+
−
    \cite{Wang:2002:SGP}. The notion of Group Priority Inversion is introduced. The main +
−
    strategy is still inversion avoidance. The method is by reordering requests +
−
    in the setting of Client-Server.+
−
  \item {\em A Formalization of Priority Inversion} \cite{journals/rts/BabaogluMS93}. +
−
    Formalized the notion of Priority +
−
    Inversion and proposes methods to avoid it. +
−
  \end{enumerate}+
−
+
−
  {\em Examples of inaccurate specification of the protocol ???}.+
−
+
−
*}+
−
+
−
section {* Conclusions \label{conclusion} *}+
−
+
−
text {*+
−
  The work in this paper only deals with single CPU configurations. The+
−
  "one CPU" assumption is essential for our formalisation, because the+
−
  main lemma fails in multi-CPU configuration. The lemma says that any+
−
  runing thead must be the one with the highest prioirty or already held+
−
  some resource when the highest priority thread was initiated. When+
−
  there are multiple CPUs, it may well be the case that a threads did+
−
  not hold any resource when the highest priority thread was initiated,+
−
  but that thread still runs after that moment on a separate CPU. In+
−
  this way, the main lemma does not hold anymore.+
−
+
−
+
−
  There are some works deals with priority inversion in multi-CPU+
−
  configurations[???], but none of them have given a formal correctness+
−
  proof. The extension of our formal proof to deal with multi-CPU+
−
  configurations is not obvious. One possibility, as suggested in paper+
−
  [???], is change our formal model (the defiintion of "schs") to give+
−
  the released resource to the thread with the highest prioirty. In this+
−
  way, indefinite prioirty inversion can be avoided, but for a quite+
−
  different reason from the one formalized in this paper (because the+
−
  "mail lemma" will be different). This means a formal correctness proof+
−
  for milt-CPU configuration would be quite different from the one given+
−
  in this paper. The solution of prioirty inversion problem in mult-CPU+
−
  configurations is a different problem which needs different solutions+
−
  which is outside the scope of this paper.+
−
+
−
*}+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−