(*<*)

theory Paper

imports "../Implementation" 

        "../Correctness" 

        "~~/src/HOL/Library/LaTeXsugar"

begin

ML {* Scan.succeed *}

ML {*

 fun strip_quants ctxt trm =

   case trm of 

      Const("HOL.Trueprop", _) $ t => strip_quants ctxt t 

    | Const("Pure.imp", _) $ _ $ t => strip_quants ctxt t

    | Const("Pure.all", _) $ Abs(n, T, t) =>

         strip_quants ctxt (subst_bound (Free (n, T), t)) 

    | Const("HOL.All", _) $ Abs(n, T, t) =>

         strip_quants ctxt (subst_bound (Free (n, T), t)) 

    | Const("HOL.Ex", _) $ Abs(n, T, t) =>

         strip_quants ctxt (subst_bound (Free (n, T), t)) 

    | _ => trm

*}

setup {* Term_Style.setup @{binding "no_quants"} (Scan.succeed strip_quants) *}

declare [[show_question_marks = false]]

notation (latex output)

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

notation (latex output)

  vt ("valid'_state") and

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

  holding_raw ("holds") and

  holding ("holds") and

  waiting_raw ("waits")

notation (latex output)

  waiting ("waits") and

  tG_raw ("TDG") and

  tG ("TDG") and

  RAG_raw ("RAG") and 

  RAG ("RAG") and

  Th ("T") 

notation (latex output)

  Cs ("C") and

  readys ("ready") and

  preced ("prec") and

  preceds ("precs") and

  cpreced ("cprec") and

  cpreceds ("cprecs") and

  cp ("cprec") and

  holdents ("resources") and  

  cntP ("c\<^bsub>P\<^esub>") and

  cntV ("c\<^bsub>V\<^esub>")

notation (latex output)

  DUMMY  ("\<^latex>\<open>\\mbox{$\\_\\!\\_$}\<close>")

notation (latex output)

  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10)

(*>*)

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 (consider the case where threads with propority $M$

  continously need to be processed). 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 once the

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

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

  \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 informal

  English) and also a few high-level descriptions of implementations

  (e.g.~in the textbooks \cite[Section 12.3.1]{Liu00} and

  \cite[Section 5.6.5]{Vahalia96}), but they help little with actual

  implementations. That this is a problem in practice is proved by an

  email by 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

  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

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

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

  Yodaiken \cite{Yodaiken02} and also Moylan et

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

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

  \cite[Section III]{Sha90} so that after the thread (whose priority has been

  raised) completes its critical section and releases the lock, it

  ``{\it returns to its original priority level}''. This leads them to

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

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

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

  al.~write that there are ``{\it some hidden

  traps}''~\cite{deinheritance}.  Consider the case where the low

  priority thread $L$ locks \emph{two} resources, and two

  high-priority threads $H$ and $H'$ each wait for one of them.  If

  $L$ releases one resource so that $H$, say, can proceed, then we

  still have Priority Inversion with $H'$ (which waits for the other

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

  remaining priority of the threads that it blocks.  A similar error

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

  for a process that inherited a higher priority and exits a critical

  section ``{\it it resumes the priority it had at the point of entry

  into the critical section}''.  This error can also be found in the

  textbook \cite[Section 16.4.1]{LiYao03} where the authors write

  about this process: ``{\it its priority is immediately lowered to the level originally assigned}'';

  and also in the 

  more recent textbook \cite[Page 119]{Laplante11} where the authors

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

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

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

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

  on this flawed specification. Accordingly, the operating system

  primitives for inheritance and restoration of priorities in

  \cite{Liu00} depend on maintaining a data structure called

  \emph{inheritance log}. This log is maintained for every thread and

  broadly specified as containing ``{\it [h]istorical information on

  how the thread inherited its current priority}'' \cite[Page

  527]{Liu00}. Unfortunately, the important information about actually

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

  explained in \cite{Liu00} but left as an ``{\it excercise}'' to the

  reader.  As we shall see, a correct version of PIP does not need to

  maintain this (potentially expensive) data structure at

  all. Surprisingly also the widely read and frequently updated

  textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the

  lock, the [low-priority] thread will revert to its original

  priority.}'' The same error is also repeated later in this popular textbook.

  While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are

  the only formal publications we have found that specify the

  incorrect behaviour, it seems also many informal descriptions of the

  PIP protocol overlook the possibility that another high-priority

  process might wait for a low-priority process to finish.  A notable

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

  behaviour of resetting the priority of a thread to the highest

  remaining priority of the threads it blocks. This textbook also

  gives an informal proof for the correctness of PIP in the style of

  Sha et al. Unfortunately, this informal proof is too vague to be

  useful for formalising the correctness of PIP and the specification

  leaves out nearly all details in order to implement PIP

  efficiently.\medskip\smallskip % %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).

  \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. We

  illustrate this with an 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

  are also being able to generalise the scheduler of Sha et

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

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

  an example of this restriction. In the existing literature there is

  no proof and also no proving method that cover this generalised

  case.

  \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 for 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 Isabelle 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>"} & 

  @{text thread} {\rm resets its own priority} \\

  & @{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).  For states

  we define the following type-synonym:

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

  \isacommand{type\_synonym} @{text "state = event list"}

  \end{isabelle}    

  \noindent As in Paulson's work, we need to define functions that

  allow us to make some observations about states.  One function,

  called @{term threads}, calculates the set of ``live'' threads that

  we have seen so far in a state:

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

  \mbox{\begin{tabular}{lcl}

  @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & 

    @{thm (rhs) threads.simps(1)}\\

  @{thm (lhs) threads.simps(2)} & @{text "\<equiv>"} & 

    @{thm (rhs) threads.simps(2)}\\

  @{thm (lhs) threads.simps(3)} & @{text "\<equiv>"} & 

    @{thm (rhs) threads.simps(3)}\\

  @{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)} & @{text "\<equiv>"} & 

    @{thm (rhs) priority.simps(1)}\\

  @{thm (lhs) priority.simps(2)} & @{text "\<equiv>"} & 

    @{thm (rhs) priority.simps(2)}\\

  @{thm (lhs) priority.simps(3)} & @{text "\<equiv>"} & 

    @{thm (rhs) priority.simps(3)}\\

  @{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)} & @{text "\<equiv>"} & 

    @{thm (rhs) last_set.simps(1)}\\

  @{thm (lhs) last_set.simps(2)} & @{text "\<equiv>"} & 

    @{thm (rhs) last_set.simps(2)}\\

  @{thm (lhs) last_set.simps(3)} & @{text "\<equiv>"} & 

    @{thm (rhs) last_set.simps(3)}\\

  @{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. An \emph{actor} of an event is

  defined as

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

  \mbox{\begin{tabular}{lcl}

  @{thm (lhs) actor.simps(5)} & @{text "\<equiv>"} & 

    @{thm (rhs) actor.simps(5)}\\

  @{thm (lhs) actor.simps(1)} & @{text "\<equiv>"} & 

    @{thm (rhs) actor.simps(1)}\\

  @{thm (lhs) actor.simps(4)} & @{text "\<equiv>"} & 

    @{thm (rhs) actor.simps(4)}\\

  @{thm (lhs) actor.simps(2)} & @{text "\<equiv>"} & 

    @{thm (rhs) actor.simps(2)}\\

  @{thm (lhs) actor.simps(3)} & @{text "\<equiv>"} & 

    @{thm (rhs) actor.simps(3)}\\

  \end{tabular}}

  \end{isabelle}

  \noindent

  This allows us to filter out the actions a set of threads @{text ths} 

  perform in a list of events @{text s}, namely

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

  @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}.

  \end{isabelle}

  \noindent

  where we use Isabelle's notation for list-comprehensions. This

  notation is very similar to notation used in Haskell for list-comprehensions.  

  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}

  \end{isabelle}

  \noindent

  We also use the abbreviation 

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

  @{abbrev "preceds ths s"}

  \end{isabelle}

  \noindent

  for the precedences of a set 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 straightforward 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. 

  %\endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}

  %in a state @{term s}. This can be straightforwardly defined in Isabelle as

  %

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

  %\mbox{\begin{tabular}{@ {}l}

  %@ {thm cntP_def}\\

  %@ {thm cntV_def}

  %\end{tabular}}

  %\end{isabelle}

  % 

  %\noindent using the predefined function @{const count} for lists.}

  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 holding_raw_def[where thread="th"]}\\

  @{thm waiting_raw_def[where thread="th"]}

  \end{tabular}

  \end{isabelle}

  \noindent In this definition we assume that @{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