(*<*)

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

  implementation of resource locking and priorities this property can

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

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

  possession of a lock for a resource that $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}.} 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. ({\bf Is this True?})

  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 not allowing critical

  sections to be preempted. Unfortunately, this solution does not

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

  threads.

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

  algorithms for PIP. A few specifications for PIP exist (in English)

  and also a few high-level descriptions of implementations (e.g.~in

  the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little

  with actual implementations. That this is a problem in practice is

  proved by an email from Baker, who wrote on 13 July 2009 on the Linux

  Kernel mailing list:

  \begin{quote}

  \it{}``I observed in the kernel code (to my disgust), the Linux PIP

  implementation is a nightmare: extremely heavy weight, involving

  maintenance of a full wait-for graph, and requiring updates for a

  range of events, including priority changes and interruptions of

  wait operations.''

  \end{quote}

  \noindent

  The criticism by Yodaiken, Baker and others suggests 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 inform an

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

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

  resource is released is irrelevant for PIP being correct---a fact

*}

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

  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,

  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.

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