(*<*)

theory Paper

imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) 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 ("inception") and

  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) 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 call it

  also \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 by

  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. While this might have been a reasonable

  solution in 2002, in our modern multiprocessor world, this seems out

  of date. The reason is that this precludes other high-priority 

  threads from running even when they do not make any use of the locked

  resource.

  However, 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

*}

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

text {*

  We follow the original work by Sha et al.~\cite{Sha90} by modelling

  first a classical single CPU system where only one \emph{thread} is

  active at any given moment. We shall discuss later how to lift this

  restriction. 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} fall into four 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 proprity 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. As in Paulson's work, we need to define 

  functions that allow one to make some observations about states.

  One is the ``live'' threads we have seen so far in a state:

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

  \mbox{\begin{tabular}{lcl}

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

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

  @{thm (lhs) threads.simps(2)[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 is that given a thread @{text "th"}, what is the original priority was at 

  its inception. 

  \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 

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

  \begin{center}

  threads, original-priority, birth time, precedence.

  \end{center}

  resources

  step relation:

  \begin{center}

  \begin{tabular}{c}

  @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}

  @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\

  @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\

  @{thm[mode=Rule] thread_V[where thread=th]}\\

  \end{tabular}

  \end{center}

  valid state:

  \begin{center}

  \begin{tabular}{c}

  @{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm}

  @{thm[mode=Rule] vt_cons[where cs=step]}

  \end{tabular}

  \end{center}

  To define events, the identifiers of {\em threads},

  {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) 

  need to be represented. All three are represetned using standard 

  Isabelle/HOL type @{typ "nat"}:

*}

text {*

  \bigskip

  The priority inversion phenomenon was first published in

  \cite{Lampson80}.  The two protocols widely used to eliminate

  priority inversion, namely PI (Priority Inheritance) and PCE

  (Priority Ceiling Emulation), were proposed in \cite{Sha90}. PCE is

  less convenient to use because it requires static analysis of

  programs. Therefore, PI is more commonly used in

  practice\cite{locke-july02}. However, as pointed out in the

  literature, the analysis of priority inheritance protocol is quite

  subtle\cite{yodaiken-july02}.  A formal analysis will certainly be

  helpful for us to understand and correctly implement PI. All

  existing formal analysis of PI

  \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the

  model checking technology. Because of the state explosion problem,

  model check is much like an exhaustive testing of finite models with

  limited size.  The results obtained can not be safely generalized to

  models with arbitrarily large size. Worse still, since model

  checking is fully automatic, it give little insight on why the

  formal model is correct. It is therefore definitely desirable to

  analyze PI using theorem proving, which gives more general results

  as well as deeper insight. And this is the purpose of this paper

  which gives a formal analysis of PI in the interactive theorem

  prover Isabelle using Higher Order Logic (HOL). The formalization

  focuses on on two issues:

  \begin{enumerate}

  \item The correctness of the protocol model itself. A series of desirable properties is 

    derived until we are fully convinced that the formal model of PI does 

    eliminate priority inversion. And a better understanding of PI is so obtained 

    in due course. For example, we find through formalization that the choice of 

    next thread to take hold when a 

    resource is released is irrelevant for the very basic property of PI to hold. 

    A point never mentioned in literature. 

  \item The correctness of the implementation. A series of properties is derived the meaning 

    of which can be used as guidelines on how PI can be implemented efficiently and correctly. 

  \end{enumerate} 

  The rest of the paper is organized as follows: Section \ref{overview} gives an overview 

  of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} 

  discusses a series of basic properties of PI. Section \ref{extension} shows formally 

  how priority inversion is controlled by PI. Section \ref{implement} gives properties 

  which can be used for guidelines of implementation. Section \ref{related} discusses 

  related works. Section \ref{conclusion} concludes the whole paper.

  The basic priority inheritance protocol has two problems:

  It does not prevent a deadlock from happening in a program with circular lock dependencies.

  A chain of blocking may be formed; blocking duration can be substantial, though bounded.

  Contributions

  Despite the wide use of Priority Inheritance Protocol in real time operating

  system, it's correctness has never been formally proved and mechanically checked. 

  All existing verification are based on model checking technology. Full automatic

  verification gives little help to understand why the protocol is correct. 

  And results such obtained only apply to models of limited size. 

  This paper presents a formal verification based on theorem proving. 

  Machine checked formal proof does help to get deeper understanding. We found 

  the fact which is not mentioned in the literature, that the choice of next 

  thread to take over when an critical resource is release does not affect the correctness

  of the protocol. The paper also shows how formal proof can help to construct 

  correct and efficient implementation.\bigskip 

*}

section {* An overview of priority inversion and priority inheritance \label{overview} *}

text {*

  Priority inversion refers to the phenomenon when a thread with high priority is blocked 

  by a thread with low priority. Priority happens when the high priority thread requests 

  for some critical resource already taken by the low priority thread. Since the high 

  priority thread has to wait for the low priority thread to complete, it is said to be 

  blocked by the low priority thread. Priority inversion might prevent high priority 

  thread from fulfill its task in time if the duration of priority inversion is indefinite 

  and unpredictable. Indefinite priority inversion happens when indefinite number 

  of threads with medium priorities is activated during the period when the high 

  priority thread is blocked by the low priority thread. Although these medium 

  priority threads can not preempt the high priority thread directly, they are able 

  to preempt the low priority threads and cause it to stay in critical section for 

  an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. 

  Priority inheritance is one protocol proposed to avoid indefinite priority inversion. 

  The basic idea is to let the high priority thread donate its priority to the low priority 

  thread holding the critical resource, so that it will not be preempted by medium priority 

  threads. The thread with highest priority will not be blocked unless it is requesting 

  some critical resource already taken by other threads. Viewed from a different angle, 

  any thread which is able to block the highest priority threads must already hold some 

  critical resource. Further more, it must have hold some critical resource at the 

  moment the highest priority is created, otherwise, it may never get change to run and 

  get hold. Since the number of such resource holding lower priority threads is finite, 

  if every one of them finishes with its own critical section in a definite duration, 

  the duration the highest priority thread is blocked is definite as well. The key to 

  guarantee lower priority threads to finish in definite is to donate them the highest 

  priority. In such cases, the lower priority threads is said to have inherited the 

  highest priority. And this explains the name of the protocol: 

  {\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.

  The objectives of this paper are:

  \begin{enumerate}

  \item Build the above mentioned idea into formal model and prove a series of properties 

    until we are convinced that the formal model does fulfill the original idea. 

  \item Show how formally derived properties can be used as guidelines for correct 

    and efficient implementation.

  \end{enumerate}

  The proof is totally formal in the sense that every detail is reduced to the 

  very first principles of Higher Order Logic. The nature of interactive theorem 

  proving is for the human user to persuade computer program to accept its arguments. 

  A clear and simple understanding of the problem at hand is both a prerequisite and a 

  byproduct of such an effort, because everything has finally be reduced to the very 

  first principle to be checked mechanically. The former intuitive explanation of 

  Priority Inheritance is just such a byproduct. 

  *}

section {* Formal model of Priority Inheritance \label{model} *}

text {*

  \input{../../generated/PrioGDef}

*}

section {* General properties of Priority Inheritance \label{general} *}

text {*

  The following are several very basic prioprites:

  \begin{enumerate}

  \item All runing threads must be ready (@{text "runing_ready"}):

          @{thm[display] "runing_ready"}  

  \item All ready threads must be living (@{text "readys_threads"}):

          @{thm[display] "readys_threads"} 

  \item There are finite many living threads at any moment (@{text "finite_threads"}):

          @{thm[display] "finite_threads"} 

  \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): 

          @{thm[display] "wq_distinct"} 

  \item All threads in waiting queues are living threads (@{text "wq_threads"}): 

          @{thm[display] "wq_threads"} 

  \item The event which can get a thread into waiting queue must be @{term "P"}-events

         (@{text "block_pre"}): 

          @{thm[display] "block_pre"}   

  \item A thread may never wait for two different critical resources

         (@{text "waiting_unique"}): 

          @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}

  \item Every resource can only be held by one thread

         (@{text "held_unique"}): 

          @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}

  \item Every living thread has an unique precedence

         (@{text "preced_unique"}): 

          @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}

  \end{enumerate}

*}

text {* \noindent

  The following lemmas show how RAG is changed with the execution of events:

  \begin{enumerate}

  \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):

    @{thm[display] depend_set_unchanged}

  \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):

    @{thm[display] depend_create_unchanged}

  \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):

    @{thm[display] depend_exit_unchanged}

  \item Execution of @{term "P"} (@{text "step_depend_p"}):

    @{thm[display] step_depend_p}

  \item Execution of @{term "V"} (@{text "step_depend_v"}):

    @{thm[display] step_depend_v}

  \end{enumerate}

  *}

text {* \noindent

  These properties are used to derive the following important results about RAG:

  \begin{enumerate}

  \item RAG is loop free (@{text "acyclic_depend"}):

  @{thm [display] acyclic_depend}

  \item RAGs are finite (@{text "finite_depend"}):

  @{thm [display] finite_depend}

  \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):

  @{thm [display] wf_dep_converse}

  \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):

  @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}

  \item All threads in RAG are living threads 

    (@{text "dm_depend_threads"} and @{text "range_in"}):

    @{thm [display] dm_depend_threads range_in}

  \end{enumerate}

  *}

text {* \noindent

  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}

  *}

text {* \noindent

  Properties about @{term "next_th"}:

  \begin{enumerate}

  \item The thread taking over is different from the thread which is releasing

  (@{text "next_th_neq"}):

  @{thm [display] next_th_neq}

  \item The thread taking over is unique

  (@{text "next_th_unique"}):

  @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}  

  \end{enumerate}

  *}

text {* \noindent

  Some deeper results about the system:

  \begin{enumerate}

  \item There can only be one running thread (@{text "runing_unique"}):

  @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}

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

  *}

text {* \noindent

  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