(*<*)
theory Paper
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
begin

(*
find_unused_assms CpsG 
find_unused_assms ExtGG 
find_unused_assms Moment 
find_unused_assms Precedence_ord 
find_unused_assms PrioG 
find_unused_assms PrioGDef
*)

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{$\_\!\_$}>")

(*abbreviation
 "detached s th \<equiv> cntP s th = cntV s th"
*)
(*>*)

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}.
  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 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} or \emph{Priority Donation}.} 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 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
  the textbook \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
  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 switch 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).  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.
*}

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.} 
  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"}\\
  & @{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 the union of the sets of waiting and holding edges, namely

  \begin{isabelle}\ \ \ \ \ %%%
  @{thm cs_depend_def}
  \end{isabelle}

  \noindent
  Given four threads and three resources, an instance of a RAG can be pictured 
  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 using the transitive closure
  operation for relations. This gives

  \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"}, which wait for resource @{text "cs\<^isub>1"}, 
  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>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

  \begin{isabelle}\ \ \ \ \ %%%
  @{thm cpreced_def2}\hfill\numbered{cpreced}
  \end{isabelle}

  \noindent
  where the dependants of @{text th} are given by the waiting queue function.
  While the precedence @{term prec} of a thread is determined statically 
  (for example when the thread is
  created), the point of the current precedence is to let the scheduler increase this
  precedence, 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 
  threads 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 informal 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); this function 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 lock, respectively wait for, it); the second is a function that
  takes a thread and returns its current precedence (see
  the definition in \eqref{cpreced}). We assume the usual getter and setter methods for
  such records.

  In the initial state, the scheduler starts with all resources unlocked (the corresponding 
  function is defined in \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 for the initial shedule state

  \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 resource; 
  for calculating the next @{term "cprec_fun"}, we use @{text wq} and 
  @{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 where 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 the old thread list plus the thread @{text th} 
  appended to the end of that list (remember the head of this list is assigned to be in the possession of this
  resource). This gives the clause

  \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 remaining threads, 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
  where @{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 in place we can introduce 
  the notion of a thread being @{term ready} 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 the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
  Note that in the initial state, that is where the list of events is empty, the set 
  @{term threads} is empty and therefore there is neither a thread ready nor 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 sets to capture both possibilities.
  We can now also conveniently define the set of resources that are locked by a thread in a
  given state and also when a thread is detached that state (meaning the thread neither 
  holds nor waits for a resource):

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm holdents_def}\\
  @{thm detached_def}
  \end{tabular}
  \end{isabelle}

  %\noindent
  %The second definition states that @{text th}  in @{text s}.
  
  Finally we can define what a \emph{valid state} is in our model of PIP. For
  example we cannot expect to be able to exit a thread, if it was not
  created yet. 
  These validity constraints on states are characterised by the
  inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
  for @{term step} 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 is not alive yet.
  Similarly, the second rule states that a thread can only be terminated if it was
  running and does not lock any resources anymore (this simplifies slightly our model;
  in practice we would expect the operating system releases all locks held by a
  thread that is about to exit). 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 the responsibility of the programmer.  In our formal
  model we brush aside these problematic cases in order to be able to make
  some meaningful statements about PIP.\footnote{This situation is
  similar to the infamous \emph{occurs check} in Prolog: In order to say
  anything meaningful about unification, one needs to perform an occurs
  check. But in practice the occurs check is omitted and the
  responsibility for avoiding problems rests with the programmer.}

 
  \begin{center}
  @{thm[mode=Rule] thread_P[where thread=th]}
  \end{center}
 
  \noindent
  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 inference rule of @{term step}.
 
  \begin{center}
  @{thm[mode=Rule] thread_V[where thread=th]}
  \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 model of PIP is correct.
*}

section {* The Correctness Proof *}

(*<*)
context extend_highest_gen
begin
(*>*)
text {* 
  Sha et al.~state their first correctness criterion for PIP in terms
  of the number of low-priority threads \cite[Theorem 3]{Sha90}: if
  there are @{text n} low-priority threads, then a blocked job with
  high priority can only be blocked a maximum of @{text n} times.
  Their second correctness criterion is given
  in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are
  @{text m} critical resources, then a blocked job with high priority
  can only be blocked a maximum of @{text m} times. Both results on their own, strictly speaking, do
  \emph{not} prevent indefinite, or unbounded, Priority Inversion,
  because if a low-priority thread does not give up its critical
  resource (the one the high-priority thread is waiting for), then the
  high-priority thread can never run.  The argument of Sha et al.~is
  that \emph{if} threads release locked resources in a finite amount
  of time, then indefinite Priority Inversion cannot occur---the high-priority
  thread is guaranteed to run eventually. The assumption is that
  programmers must ensure that threads are programmed in this way.  However, even
  taking this assumption into account, the correctness properties of
  Sha et al.~are
  \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken
  \cite{Yodaiken02} pointed out: If a low-priority thread possesses
  locks to two resources for which two high-priority threads are
  waiting for, then lowering the priority prematurely after giving up
  only one lock, can cause indefinite Priority Inversion for one of the
  high-priority threads, invalidating their two bounds.

  Even when fixed, their proof idea does not seem to go through for
  us, because of the way we have set up our formal model of PIP.  One
  reason is that we allow critical sections, which start with a @{text P}-event
  and finish with a corresponding @{text V}-event, to arbitrarily overlap
  (something Sha et al.~explicitly exclude).  Therefore we have
  designed a different correctness criterion for PIP. The idea behind
  our criterion is as follows: for all states @{text s}, we know the
  corresponding thread @{text th} with the highest precedence; we show
  that in every future state (denoted by @{text "s' @ s"}) in which
  @{text th} is still alive, either @{text th} is running or it is
  blocked by a thread that was alive in the state @{text s} and was waiting 
  for or in the possession of a lock in @{text s}. Since in @{text s}, as in
  every state, the set of alive threads is finite, @{text th} can only
  be blocked a finite number of times. This is independent of how many
  threads of lower priority are created in @{text "s'"}. We will actually prove a
  stronger statement where we also provide the current precedence of
  the blocking thread. However, this correctness criterion hinges upon
  a number of assumptions about the states @{text s} and @{text "s' @
  s"}, the thread @{text th} and the events happening in @{text
  s'}. We list them next:

  \begin{quote}
  {\bf Assumptions on the states {\boldmath@{text s}} and 
  {\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and 
  @{text "s' @ s"} are valid states:
  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{l}
  @{term "vt s"}, @{term "vt (s' @ s)"} 
  \end{tabular}
  \end{isabelle}
  \end{quote}

  \begin{quote}
  {\bf Assumptions on the thread {\boldmath@{text "th"}:}} 
  The thread @{text th} must be alive in @{text s} and 
  has the highest precedence of all alive threads in @{text s}. Furthermore the
  priority of @{text th} is @{text prio} (we need this in the next assumptions).
  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{l}
  @{term "th \<in> threads s"}\\
  @{term "prec th s = Max (cprec s ` threads s)"}\\
  @{term "prec th s = (prio, DUMMY)"}
  \end{tabular}
  \end{isabelle}
  \end{quote}
  
  \begin{quote}
  {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
  be blocked indefinitely. Of course this can happen if threads with higher priority
  than @{text th} are continuously created in @{text s'}. Therefore we have to assume that  
  events in @{text s'} can only create (respectively set) threads with equal or lower 
  priority than @{text prio} of @{text th}. We also need to assume that the
  priority of @{text "th"} does not get reset and also that @{text th} does
  not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. 
  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{l}
  {If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
  {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
  {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
  \end{tabular}
  \end{isabelle}
  \end{quote}

  \noindent
  The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}.
  Under these assumptions we shall prove the following correctness property:

  \begin{theorem}\label{mainthm}
  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
  the thread @{text th} and the events in @{text "s'"},
  if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
  @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 
  @{term "cp (s' @ s) th' = prec th s"}.
  \end{theorem}

  \noindent
  This theorem ensures that the thread @{text th}, which has the
  highest precedence in the state @{text s}, can only be blocked in
  the state @{text "s' @ s"} by a thread @{text th'} that already
  existed in @{text s} and requested or had a lock on at least 
  one resource---that means the thread was not \emph{detached} in @{text s}. 
  As we shall see shortly, that means there are only finitely 
  many threads that can block @{text th} in this way and then they 
  need to run with the same current precedence as @{text th}.

  Like in the argument by Sha et al.~our
  finite bound does not guarantee absence of indefinite Priority
  Inversion. For this we further have to assume that every thread
  gives up its resources after a finite amount of time. We found that
  this assumption is awkward to formalise in our model. Therefore we
  leave it out and let the programmer assume the responsibility to
  program threads in such a benign manner (in addition to causing no 
  circularity in the @{text RAG}). In this detail, we do not
  make any progress in comparison with the work by Sha et al.
  However, we are able to combine their two separate bounds into a
  single theorem improving their bound.

  In what follows we will describe properties of PIP that allow us to prove 
  Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
  It is relatively easy to see that

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
  @{thm[mode=IfThen]  finite_threads}
  \end{tabular}
  \end{isabelle}

  \noindent
  The second property is by induction of @{term vt}. The next three
  properties are 

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
  @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
  @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
  \end{tabular}
  \end{isabelle}

  \noindent
  The first property states that every waiting thread can only wait for a single
  resource (because it gets suspended after requesting that resource); the second 
  that every resource can only be held by a single thread; 
  the third property establishes that in every given valid state, there is
  at most one running thread. We can also show the following properties 
  about the @{term RAG} in @{text "s"}.

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\
  \hspace{5mm}@{thm (concl) acyclic_depend},
  @{thm (concl) finite_depend} and
  @{thm (concl) wf_dep_converse},\\
  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}
  and\\
  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
  \end{tabular}
  \end{isabelle}

  \noindent
  The acyclicity property follows from how we restricted the events in
  @{text step}; similarly the finiteness and well-foundedness property.
  The last two properties establish that every thread in a @{text "RAG"}
  (either holding or waiting for a resource) is a live thread.

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

  \begin{lemma}\label{mainlem}
  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
  the thread @{text th} and the events in @{text "s'"},
  if @{term "th' \<in> threads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
  then @{text "th' \<notin> running (s' @ s)"}.
  \end{lemma}

  \noindent
  The point of this lemma is that a thread different from @{text th} (which has the highest
  precedence in @{text s}) and not holding any resource, cannot be running 
  in the state @{text "s' @ s"}.

  \begin{proof}
  Since thread @{text "th'"} does not hold any resource, no thread can depend on it. 
  Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence
  @{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the 
  state @{text "(s' @ s)"} and precedences are distinct among threads, we have
  @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this 
  we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
  Since @{text "prec th (s' @ s)"} is already the highest 
  @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by 
  definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
  Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
  By defintion of @{text "running"}, @{text "th'"} can not be running in state
  @{text "s' @ s"}, as we had to show.\qed
  \end{proof}

  \noindent
  Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to 
  issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
  one step further, @{text "th'"} still cannot hold any resource. The situation will 
  not change in further extensions as long as @{text "th"} holds the highest precedence.

  From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be 
  blocked by a thread @{text th'} that
  held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
  that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the 
  precedence of @{text th} in @{text "s"}.
  We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
  This theorem gives a stricter bound on the threads that can block @{text th} than the
  one obtained by Sha et al.~\cite{Sha90}:
  only threads that were alive in state @{text s} and moreover held a resource.
  This means our bound is in terms of both---alive threads in state @{text s}
  and number of critical resources. Finally, the theorem establishes that the blocking threads have the
  current precedence raised to the precedence of @{text th}.

  We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"}
  by showing that @{text "running (s' @ s)"} is not empty.

  \begin{lemma}
  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
  the thread @{text th} and the events in @{text "s'"},
  @{term "running (s' @ s) \<noteq> {}"}.
  \end{lemma}

  \begin{proof}
  If @{text th} is blocked, then by following its dependants graph, we can always 
  reach a ready thread @{text th'}, and that thread must have inherited the 
  precedence of @{text th}.\qed
  \end{proof}


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

  %Some deeper results about the system:
  %\begin{enumerate}
  %\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}

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

  %The reason that only threads which already held some resoures
  %can be runing and block @{text "th"} is that if , otherwise, one thread 
  %does not hold any resource, it may never have its prioirty raised
  %and will not get a chance to run. This fact is supported by 
  %lemma @{text "moment_blocked"}:
  %@   {thm [display] moment_blocked}
  %When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
  %resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 
  %any thread which is running after @{text "th"} became the highest must have already held
  %some resource at state @{text "s"}.


  %When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 
  %if a thread releases all its resources at some moment in @{text "t"}, after that, 
  %it may never get a change to run. If every thread releases its resource in finite duration,
  %then after a while, only thread @{text "th"} is left running. This shows how indefinite 
  %priority inversion can be avoided. 

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

  %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 for an Implementation\label{implement} *}

text {*
  While our formalised proof gives us confidence about the correctness of our model of PIP, 
  we found that the formalisation can even help us with efficiently implementing it.

  For example Baker complained that calculating the current precedence
  in PIP is quite ``heavy weight'' in Linux (see the Introduction).
  In our model of PIP the current precedence of a thread in a state @{text s}
  depends on all its dependants---a ``global'' transitive notion,
  which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
  We can however improve upon this. For this let us define the notion
  of @{term children} of a thread @{text th} in a state @{text s} as

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm children_def2}
  \end{tabular}
  \end{isabelle}

  \noindent
  where a child is a thread that is only one ``hop'' away from the thread
  @{text th} in the @{term RAG} (and waiting for @{text th} to release
  a resource). We can prove the following lemma.

  \begin{lemma}\label{childrenlem}
  @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
  \begin{center}
  @{thm (concl) cp_rec}.
  \end{center}
  \end{lemma}
  
  \noindent
  That means the current precedence of a thread @{text th} can be
  computed locally by considering only the children of @{text th}. In
  effect, it only needs to be recomputed for @{text th} when one of
  its children changes its current precedence.  Once the current 
  precedence is computed in this more efficient manner, the selection
  of the thread with highest precedence from a set of ready threads is
  a standard scheduling operation implemented in most operating
  systems.

  Of course the main work for implementing PIP involves the
  scheduler and coding how it should react to events.  Below we
  outline how our formalisation guides this implementation for each
  kind of events.\smallskip
*}

(*<*)
context step_create_cps
begin
(*>*)
text {*
  \noindent
  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and 
  the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
  is allowed to occur). In this situation we can show that

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm eq_dep},\\
  @{thm eq_cp_th}, and\\
  @{thm[mode=IfThen] eq_cp}
  \end{tabular}
  \end{isabelle}

  \noindent
  This means in an implementation we do not have recalculate the @{text RAG} and also none of the
  current precedences of the other threads. The current precedence of the created
  thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
  \smallskip
  *}
(*<*)
end
context step_exit_cps
begin
(*>*)
text {*
  \noindent
  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 
  the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm eq_dep}, and\\
  @{thm[mode=IfThen] eq_cp}
  \end{tabular}
  \end{isabelle}

  \noindent
  This means again we do not have to recalculate the @{text RAG} and
  also not the current precedences for the other threads. Since @{term th} is not
  alive anymore in state @{term "s"}, there is no need to calculate its
  current precedence.
  \smallskip
*}
(*<*)
end
context step_set_cps
begin
(*>*)
text {*
  \noindent
  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and 
  @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm[mode=IfThen] eq_dep}, and\\
  @{thm[mode=IfThen] eq_cp_pre}
  \end{tabular}
  \end{isabelle}

  \noindent
  The first property is again telling us we do not need to change the @{text RAG}. 
  The second shows that the @{term cp}-values of all threads other than @{text th} 
  are unchanged. The reason is that @{text th} is running; therefore it is not in 
  the @{term dependants} relation of any other thread. This in turn means that the 
  change of its priority cannot affect other threads.

  %The second
  %however states that only threads that are \emph{not} dependants of @{text th} have their
  %current precedence unchanged. For the others we have to recalculate the current
  %precedence. To do this we can start from @{term "th"} 
  %and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
  %the @{term "cp"} of every 
  %thread encountered on the way. Since the @{term "depend"}
  %is assumed to be loop free, this procedure will always stop. The following two lemmas show, however, 
  %that this procedure can actually stop often earlier without having to consider all
  %dependants.
  %
  %\begin{isabelle}\ \ \ \ \ %%%
  %\begin{tabular}{@ {}l}
  %@{thm[mode=IfThen] eq_up_self}\\
  %@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
  %@{text "then"} @{thm (concl) eq_up}.
  %\end{tabular}
  %\end{isabelle}
  %
  %\noindent
  %The first lemma states that if the current precedence of @{text th} is unchanged,
  %then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
  %The second states that if an intermediate @{term cp}-value does not change, then
  %the procedure can also stop, because none of its dependent threads will
  %have their current precedence changed.
  \smallskip
  *}
(*<*)
end
context step_v_cps_nt
begin
(*>*)
text {*
  \noindent
  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 
  @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
  subcases: one where there is a thread to ``take over'' the released
  resource @{text cs}, and one where there is not. Let us consider them
  in turn. Suppose in state @{text s}, the thread @{text th'} takes over
  resource @{text cs} from thread @{text th}. We can prove


  \begin{isabelle}\ \ \ \ \ %%%
  @{thm depend_s}
  \end{isabelle}
  
  \noindent
  which shows how the @{text RAG} needs to be changed. The next lemma suggests
  how the current precedences need to be recalculated. For threads that are
  not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
  can show

  \begin{isabelle}\ \ \ \ \ %%%
  @{thm[mode=IfThen] cp_kept}
  \end{isabelle}
  
  \noindent
  For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
  recalculate their current precedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
  \noindent
  In the other case where there is no thread that takes over @{text cs}, we can show how
  to recalculate the @{text RAG} and also show that no current precedence needs
  to be recalculated.

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm depend_s}\\
  @{thm eq_cp}
  \end{tabular}
  \end{isabelle}
  *}
(*<*)
end
context step_P_cps_e
begin
(*>*)
text {*
  \noindent
  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 
  @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
  the one where @{text cs} is not locked, and one where it is. We treat the former case
  first by showing that
  
  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm depend_s}\\
  @{thm eq_cp}
  \end{tabular}
  \end{isabelle}

  \noindent
  This means we need to add a holding edge to the @{text RAG} and no
  current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
  \noindent
  In the second case we know that resource @{text cs} is locked. We can show that
  
  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm depend_s}\\
  @{thm[mode=IfThen] eq_cp}
  \end{tabular}
  \end{isabelle}

  \noindent
  That means we have to add a waiting edge to the @{text RAG}. Furthermore
  the current precedence for all threads that are not dependants of @{text th}
  are unchanged. For the others we need to follow the edges 
  in the @{text RAG} and recompute the @{term "cp"}. To do this we can start from @{term "th"} 
  and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
  the @{term "cp"} of every 
  thread encountered on the way. Since the @{term "depend"}
  is loop free, this procedure will always stop. The following lemma shows, however, 
  that this procedure can actually stop often earlier without having to consider all
  dependants.

  \begin{isabelle}\ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  %%@ {t hm[mode=IfThen] eq_up_self}\\
  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
  @{text "then"} @{thm (concl) eq_up}.
  \end{tabular}
  \end{isabelle}

  \noindent
  This lemma states that if an intermediate @{term cp}-value does not change, then
  the procedure can also stop, because none of its dependent threads will
  have their current precedence changed.
  *}
(*<*)
end
(*>*)
text {*
  \noindent
  As can be seen, a pleasing byproduct of our formalisation is that the properties in
  this section closely inform an implementation of PIP, namely whether the
  @{text RAG} needs to be reconfigured or current precedences need to
  be recalculated for an event. This information is provided by the lemmas we proved.
  We confirmed that our observations translate into practice by implementing
  our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 
  Stanford University \cite{PINTOS}. To implement PIP, we only need to modify the kernel 
  functions corresponding to the events in our formal model. The events translate to the following 
  function interface in PINTOS:

  \begin{center}
  \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
  \hline
  {\bf Event} & {\bf PINTOS function} \\
  \hline
  @{text Create} & @{text "thread_create"}\\
  @{text Exit}   & @{text "thread_exit"}\\
  @{text Set}    & @{text "thread_set_priority"}\\
  @{text P}      & @{text "lock_acquire"}\\
  @{text V}      & @{text "lock_release"}\\ 
  \hline
  \end{tabular}
  \end{center}

  \noindent
  Our implicit assumption that every event is an atomic operation is ensured by the architecture of 
  PINTOS. The case where an unlocked resource is given next to the waiting thread with the
  highest precedence is realised in our implementation by priority queues. We implemented
  them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
  for accessing and updating. Apart from having to implement relatively complex data\-structures in C
  using pointers, our experience with the implementation has been very positive: our specification 
  and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. 
*}

section {* Conclusion *}

text {* 
  The Priority Inheritance Protocol (PIP) is a classic textbook
  algorithm used in many real-time operating systems in order to avoid the problem of
  Priority Inversion.  Although classic and widely used, PIP does have
  its faults: for example it does not prevent deadlocks in cases where threads
  have circular lock dependencies.

  We had two goals in mind with our formalisation of PIP: One is to
  make the notions in the correctness proof by Sha et al.~\cite{Sha90}
  precise so that they can be processed by a theorem prover. The reason is
  that a mechanically checked proof avoids the flaws that crept into their
  informal reasoning. We achieved this goal: The correctness of PIP now
  only hinges on the assumptions behind our formal model. The reasoning, which is
  sometimes quite intricate and tedious, has been checked by Isabelle/HOL. 
  We can also confirm that Paulson's
  inductive method for protocol verification~\cite{Paulson98} is quite
  suitable for our formal model and proof. The traditional application
  area of this method is security protocols. 

  The second goal of our formalisation is to provide a specification for actually
  implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
  explain how to use various implementations of PIP and abstractly
  discuss their properties, but surprisingly lack most details important for a
  programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).  
  That this is an issue in practice is illustrated by the
  email from Baker we cited in the Introduction. We achieved also this
  goal: The formalisation allowed us to efficently implement our version
  of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86 
  architecture. It also gives the first author enough data to enable
  his undergraduate students to implement PIP (as part of their OS course).
  A byproduct of our formalisation effort is that nearly all
  design choices for the PIP scheduler are backed up with a proved
  lemma. We were also able to establish the property that the choice of
  the next thread which takes over a lock is irrelevant for the correctness
  of PIP. 

  PIP is a scheduling algorithm for single-processor systems. We are
  now living in a multi-processor world. Priority Inversion certainly
  occurs also there.  However, there is very little ``foundational''
  work about PIP-algorithms on multi-processor systems.  We are not
  aware of any correctness proofs, not even informal ones. There is an
  implementation of a PIP-algorithm for multi-processors as part of the
  ``real-time'' effort in Linux, including an informal description of the implemented scheduling
  algorithm given in \cite{LINUX}.  We estimate that the formal
  verification of this algorithm, involving more fine-grained events,
  is a magnitude harder than the one we presented here, but still
  within reach of current theorem proving technology. We leave this
  for future work.

  The most closely related work to ours is the formal verification in
  PVS of the Priority Ceiling Protocol done by Dutertre
  \cite{dutertre99b}---another solution to the Priority Inversion
  problem, which however needs static analysis of programs in order to
  avoid it. There have been earlier formal investigations
  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
  checking techniques. The results obtained by them apply,
  however, only to systems with a fixed size, such as a fixed number of 
  events and threads. In contrast, our result applies to systems of arbitrary
  size. Moreover, our result is a good 
  witness for one of the major reasons to be interested in machine checked 
  reasoning: gaining deeper understanding of the subject matter.

  Our formalisation
  consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
  code with a few apply-scripts interspersed. The formal model of PIP
  is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
  definitions and proofs span over 770 lines of code. The properties relevant
  for an implementation require 2000 lines. 
  %The code of our formalisation 
  %can be downloaded from
  %\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.\medskip

  \noindent
  {\bf Acknowledgements:}
  We are grateful for the comments we received from anonymous
  referees.

  \bibliographystyle{plain}
  \bibliography{root}
*}


(*<*)
end
(*>*)