(*<*)

theory Paper

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

begin

ML {*

  open Printer;

  show_question_marks_default := false;

  *}

notation (latex output)

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

  vt ("valid'_state") and

  runing ("running") and

  birthtime ("last'_set") and

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

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

  holding ("holds") and

  waiting ("waits") and

  Th ("T") and

  Cs ("C") and

  readys ("ready") and

  depend ("RAG") and 

  preced ("prec") and

  cpreced ("cprec") and

  dependents ("dependants") and

  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

(*>*)

section {* Introduction *}

text {*

  Many real-time systems need to support threads involving priorities and

  locking of resources. Locking of resources ensures mutual exclusion

  when accessing shared data or devices that cannot be

  preempted. Priorities allow scheduling of threads that need to

  finish their work within deadlines.  Unfortunately, both features

  can interact in subtle ways leading to a problem, called

  \emph{Priority Inversion}. Suppose three threads having priorities

  $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread

  $H$ blocks any other thread with lower priority and itself cannot

  be blocked by any thread with lower priority. Alas, in a naive

  implementation of resource looking and priorities this property can

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

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

  possession of a lock for a resource that also $H$ needs. $H$ must

  therefore wait for $L$ to exit the critical section and release this

  lock. The problem is that $L$ might in turn be blocked by any

  thread with priority $M$, and so $H$ sits there potentially waiting

  indefinitely. Since $H$ is blocked by threads with lower

  priorities, the problem is called Priority Inversion. It was first

  described in \cite{Lampson80} in the context of the

  Mesa programming language designed for concurrent programming.

  If the problem of Priority Inversion is ignored, real-time systems

  can become unpredictable and resulting bugs can be hard to diagnose.

  The classic example where this happened is the software that

  controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.

  Once the spacecraft landed, the software shut down at irregular

  intervals leading to loss of project time as normal operation of the

  craft could only resume the next day (the mission and data already

  collected were fortunately not lost, because of a clever system

  design).  The reason for the shutdowns was that the scheduling

  software fell victim of Priority Inversion: a low priority thread

  locking a resource prevented a high priority thread from running in

  time leading to a system reset. Once the problem was found, it was

  rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)

  \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority

  Inheritance Protocol} \cite{Sha90} and others sometimes also call it

  \emph{Priority Boosting}.} in the scheduling software.

  The idea behind PIP is to let the thread $L$ temporarily inherit

  the high priority from $H$ until $L$ leaves the critical section

  unlocking the resource. This solves the problem of $H$ having to

  wait indefinitely, because $L$ cannot be blocked by threads having

  priority $M$. While a few other solutions exist for the Priority

  Inversion problem, PIP is one that is widely deployed and

  implemented. This includes VxWorks (a proprietary real-time OS used

  in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's

  ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for

  example in libraries for FreeBSD, Solaris and Linux.

  One advantage of PIP is that increasing the priority of a thread

  can be dynamically calculated by the scheduler. This is in contrast

  to, for example, \emph{Priority Ceiling} \cite{Sha90}, another

  solution to the Priority Inversion problem, which requires static

  analysis of the program in order to prevent Priority

  Inversion. However, there has also been strong criticism against

  PIP. For instance, PIP cannot prevent deadlocks when lock

  dependencies are circular, and also blocking times can be

  substantial (more than just the duration of a critical section).

  Though, most criticism against PIP centres around unreliable

  implementations and PIP being too complicated and too inefficient.

  For example, Yodaiken writes in \cite{Yodaiken02}:

  \begin{quote}

  \it{}``Priority inheritance is neither efficient nor reliable. Implementations

  are either incomplete (and unreliable) or surprisingly complex and intrusive.''

  \end{quote}

  \noindent

  He suggests to avoid PIP altogether by not allowing critical

  sections to be preempted. Unfortunately, this solution does not

  help in real-time systems with low latency \emph{requirements}.

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

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

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

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

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

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

  Kernel mailing list:

  \begin{quote}

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

  implementation is a nightmare: extremely heavy weight, involving

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

  range of events, including priority changes and interruptions of

  wait operations.''

  \end{quote}

  \noindent

  The criticism by Yodaiken, Baker and others suggests to us to look

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

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

  formal verification. One reason, of course, is that the original

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

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

  Yodaiken \cite{Yodaiken02} points to a subtlety that had been

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

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

  completes its critical section and releases the lock, it ``returns

  to its original priority level.'' This leads them to believe that an

  implementation of PIP is ``rather straightforward''~\cite{Sha90}.

  Unfortunately, as Yodaiken points out, this behaviour is too

  simplistic.  Consider the case where the low priority thread $L$

  locks \emph{two} resources, and two high-priority threads $H$ and

  $H'$ each wait for one of them.  If $L$ then releases one resource

  so that $H$, say, can proceed, then we still have Priority Inversion

  with $H'$ (which waits for the other resource). The correct

  behaviour for $L$ is to revert to the highest remaining priority of

  the threads that it blocks. The advantage of formalising the

  correctness of a high-level specification of PIP in a theorem prover

  is that such issues clearly show up and cannot be overlooked as in

  informal reasoning (since we have to analyse all possible behaviours

  of threads, i.e.~\emph{traces}, that could possibly happen).

  There have been earlier formal investigations into PIP, but ...\cite{Faria08}

  vt (valid trace) was introduced earlier, cite

  distributed PIP

  Paulson's method has not been used outside security field, except

  work by Zhang et al.

  no clue about multi-processor case according to \cite{Steinberg10} 

*}

section {* Formal Model of the Priority Inheritance Protocol *}

text {*

  The Priority Inheritance Protocol, short PIP, is a scheduling

  algorithm for a single-processor system.\footnote{We shall come back

  later to the case of PIP on multi-processor systems.} Our model of

  PIP is based on Paulson's inductive approach to protocol

  verification \cite{Paulson98}, where the \emph{state} of a system is

  given by a list of events that happened so far.  \emph{Events} in 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 one to make some observations

  ``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

  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 (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 process is created yet, 

  the waiting queue function will be the function that just returns the

  empty list for every resource.

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

  @{abbrev all_unlocked}

  \end{isabelle}

  \noindent

  Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 

  (RAG), which represent the dependencies between threads and resources.

  We represent RAGs as relations using pairs of the form

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

  @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}

  @{term "(Cs cs, Th th)"}

  \end{isabelle}

  \noindent

  where the first stands for a \emph{waiting edge} and the second for a 

  \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 

  datatype for vertices). Given a waiting queue function, a RAG is defined 

  as

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

  @{thm cs_depend_def}

  \end{isabelle}

  \noindent

  An instance of a RAG is as follows:

  \begin{center}

  \begin{tikzpicture}[scale=1]

  \end{tikzpicture}

  \end{center}

  \noindent

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

  the notion of the \emph{dependants} of a thread. This is defined as

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

  @{thm cs_dependents_def}

  \end{isabelle}

  \noindent

  This definition needs to account for all threads that wait for a thread to

  release a resource. This means we need to include threads that transitively

  wait for a resource being released (in the picture above this means also @{text "th\<^isub>3"}, 

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

  in turn needs to wait for @{text "th\<^isub>1"}). If there is a circle in a RAG, then clearly

  we have a deadlock. Therefore when a thread requests a resource,

  we must ensure that the resulting RAG is not not circular. 

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

  state @{text s}, which is defined as

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

  @{thm cpreced_def2}

  \end{isabelle}

  \noindent

  While the precedence @{term prec} of a thread is determined by the programmer 

  (for example when the thread is

  created), the point of the current precedence is to let scheduler increase this

  priority, if needed according to PIP. Therefore the current precedence of @{text th} is

  given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 

  processes that are dependants of @{text th}. Since the notion @{term "dependants"} is

  defined as the transitive closure of all dependent threads, we deal correctly with the 

  problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is

  lowered prematurely.

  The next function, called @{term schs}, defines the behaviour of the scheduler. It is defined

  by recursion on the state (a list of events); @{term "schs"} takes a state as argument

  and returns a \emph{schedule state}, which we define as a record consisting of two

  functions:

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

  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}

  \end{isabelle}

  \noindent

  The first is a waiting queue function (that is takes a @{text "cs"} and returns the

  corresponding list of threads that wait for it), the second is a function that takes

  a thread and returns its current precedence (see ???). We have the usual getter and 

  setter methods for such records.

  In the initial state, the scheduler starts with all resources unlocked and the

  precedence of every thread is initialised with @{term "Prc 0 0"}. Therefore

  we have

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

  \begin{tabular}{@ {}l}

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

  \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}

  \end{tabular}

  \end{isabelle}

  \noindent

  The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:

  we calculate the waiting queue function of the (previous) state @{text s}; 

  this waiting queue function @{text wq} is unchanged in the next schedule state; 

  for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function 

  @{term cpreced}. This gives the following three clauses:

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

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

  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\

  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\

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

  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\

  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}

  \end{tabular}

  \end{isabelle}

  \noindent 

  More interesting are the cases when a resource, say @{text cs}, is locked or released. In this case

  we need to calculate a new waiting queue function. In case of @{term P}, we update

  the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th} 

  appended to the end (remember the head of this list is in the possession of the

  resource).

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

  \begin{tabular}{@ {}l}

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

  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\

  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\

  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}

  \end{tabular}

  \end{isabelle}

  \noindent

  The case for @{term V} is similar, except that we need to update the waiting queue function

  so that the thread that possessed the lock is eliminated. For this we use

  the auxiliary function @{term release}. A simple version of @{term release} would

  just delete this thread and return the rest like so

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

  \begin{tabular}{@ {}lcl}

  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\

  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\

  \end{tabular}

  \end{isabelle}

  \noindent

  However in practice often the thread with the highest precedence will get the

  lock next. We have implemented this choice, but later found out that the choice 

  about which thread is chosen next is actually irrelevant for the correctness of PIP.

  Therefore we prove the stronger result where @{term release} is defined as

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

  \begin{tabular}{@ {}lcl}

  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\

  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\

  \end{tabular}

  \end{isabelle}

  \noindent

  @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary

  choice for the next waiting list, it just has to be a distinct list and

  contain the same elements as @{text "qs"}. This gives for @{term V} and @{term schs} 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}

  TODO

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

  \begin{tabular}{@ {}l}

  @{thm s_depend_def}\\

  \end{tabular}

  \end{isabelle}

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

  \begin{tabular}{@ {}l}

  @{thm readys_def}\\

  \end{tabular}

  \end{isabelle}

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

  \begin{tabular}{@ {}l}

  @{thm runing_def}\\

  \end{tabular}

  \end{isabelle}