(*<*)theory Paperimports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"beginML {* 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{$\_\!\_$}>")(*>*)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 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 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$ 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).\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; the earlier informal proof by Sha et al.~\cite{Sha90} is flawed). 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, inform an 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. Something which has not been mentioned in the relevant literature.*}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} 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 \begin{isabelle}\ \ \ \ \ %%% @{thm cs_depend_def} \end{isabelle} \noindent Given three threads and three resources, an instance of a RAG is 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. 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 the dependants of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, 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>1"} to finish). 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 circular. 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 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 will be defined by recursion on the state (a list of events); @{term "schs"} 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 wait for it), the second is a function that takes a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and setter methods for such records. In the initial state, the scheduler starts with all resources unlocked (see \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 \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 resources; for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function @{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 when 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 old thread list plus the thread @{text th} appended to the end of that list (remember the head of this list is seen to be in the possession of this 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 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 rest, 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 @{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 we can introduce the notion of threads being @{term readys} 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 this definition @{term "f ` S"} stands for the set @{text S} under the image of the function @{text f}. Note that in the initial case, that is where the list of events is empty, the set @{term threads} is empty and therefore there is no thread ready nor a 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 the set-comprehension to capture both possibilities. We can now also define the set of resources that are locked by a thread in any given state. \begin{isabelle}\ \ \ \ \ %%% @{thm holdents_def} \end{isabelle} \noindent These resources are given by the holding edges in the RAG. Finally we can define what a \emph{valid state} is in our PIP. For example we cannot expect to be able to exit a thread, if it was not created yet. These validity constraints are characterised by the inductive predicate @{term "step"}. We give five inference rules 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 does not yet exists. Similarly, the second rule states that a thread can only be terminated if it was running and does not lock any resources anymore (to simplify ). 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 of course the responsibility of the programmer. Here in our formal model we just exclude such problematic cases in order to make some meaningful statements about PIP.\footnote{This situation is similar to the infamous occurs check in Prolog: in order to say anything meaningful about unification, we need to perform an occurs check; but in practice the occurs check is ommited and the responsibility to avoid problems rests with the programmer.} 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 two inference rules of @{term step}. \begin{center} \begin{tabular}{c} @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\ @{thm[mode=Rule] thread_V[where thread=th]}\\ \end{tabular} \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 version of PIP is correct.*}section {* Correctness Proof *}(*<*)context extend_highest_genbegin(*>*)print_locale extend_highest_genthm extend_highest_gen_defthm extend_highest_gen_axioms_defthm highest_gen_deftext {* Main lemma \begin{enumerate} \item @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}): @{thm threads_s}. \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}): @{thm highest}. \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}): @{thm preced_th}. \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}. \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore its precedence can not be higher than @{term "th"}, therefore @{term "th"} remain to be the one with the highest precedence (@{text "create_low"}): @{thm [display] create_low} \item Any adjustment of priority in @{term "t"} does not happen to @{term "th"} and the priority set is no higher than @{term "prio"}, therefore @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}): @{thm [display] set_diff_low} \item Since we are investigating what happens to @{term "th"}, it is assumed @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}): @{thm [display] exit_diff} \end{enumerate} \begin{lemma} @{thm[mode=IfThen] moment_blocked} \end{lemma} \begin{theorem} @{thm[mode=IfThen] runing_inversion_2} \end{theorem} \begin{theorem} @{thm[mode=IfThen] runing_inversion_3} \end{theorem}TO DO *}(*<*)end(*>*)section {* Properties for an Implementation *}text {* TO DO *}section {* Conclusion *}text {* The Priority Inheritance Protocol is a classic textbook algorithm used in real-time systems in order to avoid the problem of Priority Inversion. 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. Our formalisation and the one presented in \cite{Wang09} are the only ones that employ Paulson's method for verifying protocols which are \emph{not} security related. TO DO no clue about multi-processor case according to \cite{Steinberg10} *}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{Jahier09,Wellings07,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 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} *}section {* Key properties \label{extension} *}(*<*)context extend_highest_genbegin(*>*)text {* The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this purpose, we need to investigate what happens after one thread takes the highest precedence. A locale is used to describe such a situation, which assumes: \begin{enumerate} \item @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}): @{thm threads_s}. \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}): @{thm highest}. \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}): @{thm preced_th}. \end{enumerate} *}text {* \noindent Under these assumptions, some basic priority can be derived for @{term "th"}: \begin{enumerate} \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}): @{thm [display] eq_cp_s_th} \item The current precedence of @{term "th"} is the highest precedence in the system (@{text "highest_cp_preced"}): @{thm [display] highest_cp_preced} \item The precedence of @{term "th"} is the highest precedence in the system (@{text "highest_preced_thread"}): @{thm [display] highest_preced_thread} \item The current precedence of @{term "th"} is the highest current precedence in the system (@{text "highest'"}): @{thm [display] highest'} \end{enumerate} *}text {* \noindent To analysis what happens after state @{term "s"} a sub-locale is defined, which assumes: \begin{enumerate} \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}. \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore its precedence can not be higher than @{term "th"}, therefore @{term "th"} remain to be the one with the highest precedence (@{text "create_low"}): @{thm [display] create_low} \item Any adjustment of priority in @{term "t"} does not happen to @{term "th"} and the priority set is no higher than @{term "prio"}, therefore @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}): @{thm [display] set_diff_low} \item Since we are investigating what happens to @{term "th"}, it is assumed @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}): @{thm [display] exit_diff} \end{enumerate}*}text {* \noindent 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} *}text {* \noindent 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 to guide implementation \label{implement} *}text {* The properties (especially @{text "runing_inversion_2"}) convinced us that the model defined in Section \ref{model} does prevent indefinite priority inversion and therefore fulfills the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper is to show how this model can be used to guide a concrete implementation. As discussed in Section 5.6.5 of \cite{Vahalia96}, the implementation of Priority Inheritance in Solaris uses sophisticated linking data structure. Except discussing two scenarios to show how the data structure should be manipulated, a lot of details of the implementation are missing. In \cite{Faria08,Jahier09,Wellings07} the protocol is described formally using different notations, but little information is given on how this protocol can be implemented efficiently, especially there is no information on how these data structure should be manipulated. Because the scheduling of threads is based on current precedence, the central issue in implementation of Priority Inheritance is how to compute the precedence correctly and efficiently. As long as the precedence is correct, it is very easy to modify the scheduling algorithm to select the correct thread to execute. First, it can be proved that the computation of current precedence @{term "cp"} of a threads only involves its children (@{text "cp_rec"}): @{thm [display] cp_rec} where @{term "children s th"} represents the set of children of @{term "th"} in the current RAG: \[ @{thm (lhs) children_def} @{text "\<equiv>"} @{thm (rhs) children_def} \] where the definition of @{term "child"} is: \[ @{thm (lhs) child_def} @{text "\<equiv>"} @{thm (rhs) child_def} \] The aim of this section is to fill the missing details of how current precedence should be changed with the happening of events, with each event type treated by one subsection, where the computation of @{term "cp"} uses lemma @{text "cp_rec"}. *}subsection {* Event @{text "Set th prio"} *}(*<*)context step_set_cpsbegin(*>*)text {* The context under which event @{text "Set th prio"} happens is formalized as follows: \begin{enumerate} \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}. \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies event @{text "Set th prio"} is eligible to happen under state @{term "s'"} and state @{term "s'"} is a valid state. \end{enumerate} *}text {* \noindent Under such a context, we investigated how the current precedence @{term "cp"} of threads change from state @{term "s'"} to @{term "s"} and obtained the following conclusions: \begin{enumerate} %% \item The RAG does not change (@{text "eq_dep"}): @{thm "eq_dep"}. \item All threads with no dependence relation with thread @{term "th"} have their @{term "cp"}-value unchanged (@{text "eq_cp"}): @{thm [display] eq_cp} This lemma implies the @{term "cp"}-value of @{term "th"} and those threads which have a dependence relation with @{term "th"} might need to be recomputed. The way to do this is to start from @{term "th"} and follow the @{term "depend"}-chain to recompute the @{term "cp"}-value of every encountered thread using lemma @{text "cp_rec"}. Since the @{term "depend"}-relation is loop free, this procedure can always stop. The the following lemma shows this procedure actually could stop earlier. \item The following two lemma shows, if a thread the re-computation of which gives an unchanged @{term "cp"}-value, the procedure described above can stop. \begin{enumerate} \item Lemma @{text "eq_up_self"} shows if the re-computation of @{term "th"}'s @{term "cp"} gives the same result, the procedure can stop: @{thm [display] eq_up_self} \item Lemma @{text "eq_up"}) shows if the re-computation at intermediate threads gives unchanged result, the procedure can stop: @{thm [display] eq_up} \end{enumerate} \end{enumerate} *}(*<*)end(*>*)subsection {* Event @{text "V th cs"} *}(*<*)context step_v_cps_ntbegin(*>*)text {* The context under which event @{text "V th cs"} happens is formalized as follows: \begin{enumerate} \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}. \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies event @{text "V th cs"} is eligible to happen under state @{term "s'"} and state @{term "s'"} is a valid state. \end{enumerate} *}text {* \noindent Under such a context, we investigated how the current precedence @{term "cp"} of threads change from state @{term "s'"} to @{term "s"}. Two subcases are considerted, where the first is that there exits @{term "th'"} such that @{thm [display] nt} holds, which means there exists a thread @{term "th'"} to take over the resource release by thread @{term "th"}. In this sub-case, the following results are obtained: \begin{enumerate} \item The change of RAG is given by lemma @{text "depend_s"}: @{thm [display] "depend_s"} which shows two edges are removed while one is added. These changes imply how the current precedences should be re-computed. \item First all threads different from @{term "th"} and @{term "th'"} have their @{term "cp"}-value kept, therefore do not need a re-computation (@{text "cp_kept"}): @{thm [display] cp_kept} This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"} need to be recomputed. \end{enumerate} *}(*<*)endcontext step_v_cps_nntbegin(*>*)text {* The other sub-case is when for all @{text "th'"} @{thm [display] nnt} holds, no such thread exists. The following results can be obtained for this sub-case: \begin{enumerate} \item The change of RAG is given by lemma @{text "depend_s"}: @{thm [display] depend_s} which means only one edge is removed. \item In this case, no re-computation is needed (@{text "eq_cp"}): @{thm [display] eq_cp} \end{enumerate} *}(*<*)end(*>*)subsection {* Event @{text "P th cs"} *}(*<*)context step_P_cps_ebegin(*>*)text {* The context under which event @{text "P th cs"} happens is formalized as follows: \begin{enumerate} \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}. \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies event @{text "P th cs"} is eligible to happen under state @{term "s'"} and state @{term "s'"} is a valid state. \end{enumerate} This case is further divided into two sub-cases. The first is when @{thm ee} holds. The following results can be obtained: \begin{enumerate} \item One edge is added to the RAG (@{text "depend_s"}): @{thm [display] depend_s} \item No re-computation is needed (@{text "eq_cp"}): @{thm [display] eq_cp} \end{enumerate}*}(*<*)endcontext step_P_cps_nebegin(*>*)text {* The second is when @{thm ne} holds. The following results can be obtained: \begin{enumerate} \item One edge is added to the RAG (@{text "depend_s"}): @{thm [display] depend_s} \item Threads with no dependence relation with @{term "th"} do not need a re-computation of their @{term "cp"}-values (@{text "eq_cp"}): @{thm [display] eq_cp} This lemma implies all threads with a dependence relation with @{term "th"} may need re-computation. \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier (@{text "eq_up"}): @{thm [display] eq_up} \end{enumerate} *}(*<*)end(*>*)subsection {* Event @{text "Create th prio"} *}(*<*)context step_create_cpsbegin(*>*)text {* The context under which event @{text "Create th prio"} happens is formalized as follows: \begin{enumerate} \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}. \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies event @{text "Create th prio"} is eligible to happen under state @{term "s'"} and state @{term "s'"} is a valid state. \end{enumerate} The following results can be obtained under this context: \begin{enumerate} \item The RAG does not change (@{text "eq_dep"}): @{thm [display] eq_dep} \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}): @{thm [display] eq_cp} \item The @{term "cp"}-value of @{term "th"} equals its precedence (@{text "eq_cp_th"}): @{thm [display] eq_cp_th} \end{enumerate}*}(*<*)end(*>*)subsection {* Event @{text "Exit th"} *}(*<*)context step_exit_cpsbegin(*>*)text {* The context under which event @{text "Exit th"} happens is formalized as follows: \begin{enumerate} \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}. \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies event @{text "Exit th"} is eligible to happen under state @{term "s'"} and state @{term "s'"} is a valid state. \end{enumerate} The following results can be obtained under this context: \begin{enumerate} \item The RAG does not change (@{text "eq_dep"}): @{thm [display] eq_dep} \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}): @{thm [display] eq_cp} \end{enumerate} Since @{term th} does not live in state @{term "s"}, there is no need to compute its @{term cp}-value.*}(*<*)end(*>*)section {* Related works \label{related} *}text {* \begin{enumerate} \item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java} \cite{Wellings07} models and verifies the combination of Priority Inheritance (PI) and Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed formal model of combined PI and PCE is given, the number of properties is quite small and the focus is put on the harmonious working of PI and PCE. Most key features of PI (as well as PCE) are not shown. Because of the limitation of the model checking technique used there, properties are shown only for a small number of scenarios. Therefore, the verification does not show the correctness of the formal model itself in a convincing way. \item {\em Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC} \cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown for PI using model checking. The limitation of model checking is intrinsic to the work. \item {\em Synchronous modeling and validation of priority inheritance schedulers} \cite{Jahier09}. Gives a formal model of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked several properties using model checking. The number of properties shown there is less than here and the scale is also limited by the model checking technique. \item {\em The Priority Ceiling Protocol: Formalization and Analysis Using PVS} \cite{dutertre99b}. Formalized another protocol for Priority Inversion in the interactive theorem proving system PVS.\end{enumerate} There are several works on inversion avoidance: \begin{enumerate} \item {\em Solving the group priority inversion problem in a timed asynchronous system} \cite{Wang:2002:SGP}. The notion of Group Priority Inversion is introduced. The main strategy is still inversion avoidance. The method is by reordering requests in the setting of Client-Server. \item {\em A Formalization of Priority Inversion} \cite{journals/rts/BabaogluMS93}. Formalized the notion of Priority Inversion and proposes methods to avoid it. \end{enumerate} {\em Examples of inaccurate specification of the protocol ???}.*}section {* Conclusions \label{conclusion} *}text {* The work in this paper only deals with single CPU configurations. The "one CPU" assumption is essential for our formalisation, because the main lemma fails in multi-CPU configuration. The lemma says that any runing thead must be the one with the highest prioirty or already held some resource when the highest priority thread was initiated. When there are multiple CPUs, it may well be the case that a threads did not hold any resource when the highest priority thread was initiated, but that thread still runs after that moment on a separate CPU. In this way, the main lemma does not hold anymore. There are some works deals with priority inversion in multi-CPU configurations[???], but none of them have given a formal correctness proof. The extension of our formal proof to deal with multi-CPU configurations is not obvious. One possibility, as suggested in paper [???], is change our formal model (the defiintion of "schs") to give the released resource to the thread with the highest prioirty. In this way, indefinite prioirty inversion can be avoided, but for a quite different reason from the one formalized in this paper (because the "mail lemma" will be different). This means a formal correctness proof for milt-CPU configuration would be quite different from the one given in this paper. The solution of prioirty inversion problem in mult-CPU configurations is a different problem which needs different solutions which is outside the scope of this paper.*}(*<*)end(*>*)