(*<*)

theory Paper

imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"

begin

declare [[show_question_marks = false]]

notation (latex output)

  Cons ("_::_" [78,77] 73) and

  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

  vt ("valid'_state") and

  runing ("running") and

  Prc ("'(_, _')") and

  holding ("holds") and

  waiting ("waits") and

  Th ("T") and

  Cs ("C") and

  readys ("ready") and

  preced ("prec") and

  preceds ("precs") and

  cpreced ("cprec") and

  cp ("cprec") and

  holdents ("resources") 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 the thread itself cannot

  be blocked indefinitely by threads with lower priority. Alas, in a naive

  implementation of resource locking and priorities this property can

  be violated. For this let $L$ be in the

  possession of a lock for a resource that $H$ also 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}.

  On Earth the software run mostly without any problem, but

  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 to 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}, \emph{Priority Donation} or \emph{Priority Lending}.} 

  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.) and ThreadX (another proprietary real-time OS

  used in nearly all HP inkjet printers \cite{ThreadX}), but also

  the POSIX 1003.1c Standard realised for

  example in libraries for FreeBSD, Solaris and Linux. 

  Two advantages of PIP are that it is deterministic and that increasing the priority of a thread

  can be performed dynamically by the scheduler.

  This is in contrast to \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, and also in contrast to the approach taken in the Windows NT scheduler, which avoids

  this problem by randomly boosting the priority of ready low-priority threads

  (see for instance~\cite{WINDOWSNT}).

  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 avoiding PIP altogether by designing the system so that no 

  priority inversion may happen in the first place. However, such ideal designs may 

  not always be achievable in practice.

  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

  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 another look

  at PIP from a more abstract level (but still concrete enough

  to inform an implementation), and makes PIP a good candidate for a

  formal verification. An additional reason is that the original

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

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

  \cite{Sha90} that after the thread (whose priority has been raised)

  high-priority might wait for a low-priority process to finish.

  \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. For this we 

  needed to design a new correctness criterion for PIP. 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, can help with an

  efficient implementation of PIP in the educational PINTOS operating

  system \cite{PINTOS}.  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---a

  fact that has not been mentioned in the literature and not been used

  in the reference implementation of PIP in PINTOS.  This fact, however, is important

  for an efficient implementation of PIP, because we can give the lock

  to the thread with the highest priority so that it terminates more

  quickly.  We were also being able to generalise the scheduler of Sha

  et al.~\cite{Sha90} to the practically relevant case where critical 

  \begin{figure}

  \begin{center}

  \begin{tikzpicture}[scale=1]

  %%\draw[step=2mm] (0,0) grid (10,2);

  \draw [->,line width=0.6mm] (0,0) -- (10,0);

  \draw [->,line width=0.6mm] (0,1.5) -- (10,1.5);

  \draw [line width=0.6mm, pattern=horizontal lines] (0.8,0) rectangle (4,0.5);

  \draw [line width=0.6mm, pattern=north east lines] (3.0,0) rectangle (6,0.5);

  \draw [line width=0.6mm, pattern=vertical lines] (5.0,0) rectangle (9,0.5);

  \draw [line width=0.6mm, pattern=horizontal lines] (0.6,1.5) rectangle (4.0,2); 

  \draw [line width=0.6mm, pattern=north east lines] (1.0,1.5) rectangle (3.4,2); 

  \draw [line width=0.6mm, pattern=vertical lines] (5.0,1.5) rectangle (8.8,2); 

  \node at (0.8,-0.3) {@{term "P\<^sub>1"}};

  \node at (3.0,-0.3) {@{term "P\<^sub>2"}};

  \node at (4.0,-0.3) {@{term "V\<^sub>1"}}; 

  \node at (5.0,-0.3) {@{term "P\<^sub>3"}};

  \node at (6.0,-0.3) {@{term "V\<^sub>2"}};

  \node at (9.0,-0.3) {@{term "V\<^sub>3"}};

  \node at (0.6,1.2) {@{term "P\<^sub>1"}};

  \node at (1.0,1.2) {@{term "P\<^sub>2"}};

  \node at (3.4,1.2) {@{term "V\<^sub>2"}};

  \node at (4.0,1.2) {@{term "V\<^sub>1"}};

  \node at (5.0,1.2) {@{term "P\<^sub>3"}};

  \node at (8.8,1.2) {@{term "V\<^sub>3"}};

  \node at (10.3,0) {$t$};

  \node at (10.3,1.5) {$t$};

  \node at (-0.3,0.2) {$b)$};

  \node at (-0.3,1.7) {$a)$};

  \end{tikzpicture}\mbox{}\\[-10mm]\mbox{}

  \end{center}

  \caption{Assume a process is over time locking and unlocking, say, three resources.

  The locking requests are labelled @{term "P\<^sub>1"}, @{term "P\<^sub>2"}, and @{term "P\<^sub>3"} 

  respectively, and the corresponding unlocking operations are labelled

  @{term "V\<^sub>1"}, @{term "V\<^sub>2"}, and @{term "V\<^sub>3"}. 

  Then graph $a)$ shows \emph{properly nested} critical sections as required 

  by Sha et al.~\cite{Sha90} in their proof---the sections must either be contained within 

  each other

  (the section @{term "P\<^sub>2"}--@{term "V\<^sub>2"} is contained in @{term "P\<^sub>1"}--@{term "V\<^sub>1"}) or

  be independent (@{term "P\<^sub>3"}--@{term "V\<^sub>3"} is independent from the other 

  two). Graph $b)$ shows the general case where 

  the locking and unlocking of different critical sections can 

  overlap.\label{overlap}}

  \end{figure}

*}

section {* Formal Model of the Priority Inheritance Protocol\label{model} *}

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.} 

  Following good experience in earlier work \cite{Wang09},  

  our model of PIP is based on Paulson's inductive approach to protocol

  verification \cite{Paulson98}. In this approach a \emph{state} of a system is

  given by a list of events that happened so far (with new events prepended to the list). 

  \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\<iota>"}\\

  & @{text "|"} & @{term "Exit thread"} \\

  & @{text "|"} & @{term "Set thread priority\<iota>"} & {\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 and @{term "[]"} for the empty list.

  Another function calculates the priority for a thread @{text "th"}, which is 

  defined as

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

  \mbox{\begin{tabular}{lcl}

  @{thm (lhs) priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 

    @{thm (rhs) priority.simps(1)[where thread="th"]}\\

  @{thm (lhs) priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 

    @{thm (rhs) priority.simps(2)[where thread="th" and thread'="th'"]}\\

  @{thm (lhs) priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 

    @{thm (rhs) priority.simps(3)[where thread="th" and thread'="th'"]}\\

  @{term "priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "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 thread had its 

  priority last set.

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

  \mbox{\begin{tabular}{lcl}

  @{thm (lhs) last_set.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 

    @{thm (rhs) last_set.simps(1)[where thread="th"]}\\

  @{thm (lhs) last_set.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 

    @{thm (rhs) last_set.simps(2)[where thread="th" and thread'="th'"]}\\

  @{thm (lhs) last_set.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 

    @{thm (rhs) last_set.simps(3)[where thread="th" and thread'="th'"]}\\

  @{term "last_set th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "last_set 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

  We also use the abbreviation 

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

  @{abbrev "preceds s ths"}

  \end{isabelle}

  \noindent

  for the set of precedences of threads @{text ths} in state @{text s}.

  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 threads with 

  the same priority. 

  Moylan et al.~\cite{deinheritance} considered the alternative of 

  ``time-slicing'' threads with equal priority, but found that it does not lead to 

  advantages in practice. On the contrary, according to their work having a policy 

  like our FIFO-scheduling of threads with equal priority reduces the number of

  tasks involved in the inheritance process and thus minimises the number

  of potentially expensive thread-switches. 

  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.

  Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow

  from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL. 

  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 the union of the sets of waiting and holding edges, namely

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

  @{thm cs_RAG_def}

  \end{isabelle}

  \begin{figure}[t]

  \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\<^sub>0"}};

  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>1"}};

  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>1"}};

  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>2"}};

  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>2"}};

  \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>3"}};

  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>3"}};

  \node (X) at (0,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>4"}};

  \node (Y) at (2,-2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>4"}};

  \node (Z) at (2,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>5"}};

  \node (U1) at (4,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>5"}};

  \node (U2) at (4,-2.9) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>6"}};

   \node (R) at (6,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>6"}};

  \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);

  \draw [->,line width=0.6mm] (U1) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (Y);

  \draw [->,line width=0.6mm] (U2) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (Z);

  \draw [<-,line width=0.6mm] (X) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (Z);

  \draw [<-,line width=0.6mm] (X) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (Y);

  \draw [<-,line width=0.6mm] (U2) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (R);

  \end{tikzpicture}

  \end{center}

  \caption{An instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}

  \end{figure}

  \noindent

  If there is no cycle, then every RAG can be pictured as a forrest of trees, as

  for example in Figure~\ref{RAGgraph}.

  We will design our scheduler  

  so that every thread can be in the possession of several resources, that is 

  it has potentially several incoming holding edges in the RAG, but has at most one outgoing  

  waiting edge. The reason is that when a thread asks for resource that is locked

  already, then the thread is blocked and cannot ask for another resource.

  Clearly, also every resource can only have at most one outgoing holding edge---indicating

  that the resource is locked. In this way we can always start at a thread waiting for a 

  resource and ``chase'' outgoing arrows leading to a single root of a tree. 

  The use of relations for representing RAGs allows us to conveniently define

  the notion of the \emph{dependants} of a thread using the transitive closure

  operation for relations, written ~@{term "trancl DUMMY"}. This gives

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

  @{thm cs_dependants_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 to be released (in the picture above this means the dependants

  of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"}, 

  but also @{text "th\<^sub>3"}, 

  which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which

  in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies 

  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. In practice, the 

  programmer has to ensure this.

  Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 

  state @{text s}. It is defined as