(*<*)+ −
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+ −
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, can 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 the union of the sets of waiting and holding edges, namely+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
@{thm cs_depend_def}+ −
\end{isabelle}+ −
+ −
\noindent+ −
Given three threads and three resources, an instance of a RAG can be pictured + −
as follows:+ −
+ −
\begin{center}+ −
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}+ −
\begin{tikzpicture}[scale=1]+ −
%%\draw[step=2mm] (-3,2) grid (1,-1);+ −
+ −
\node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};+ −
\node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};+ −
\node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};+ −
\node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};+ −
\node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};+ −
\node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};+ −
\node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};+ −
+ −
\draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);+ −
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);+ −
\draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);+ −
\draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E);+ −
\draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1);+ −
\draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\noindent+ −
The use of relations for representing RAGs allows us to conveniently define+ −
the notion of the \emph{dependants} of a thread using the transitive closure+ −
operation for relations. This gives+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
@{thm cs_dependents_def}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This definition needs to account for all threads that wait for a thread to+ −
release a resource. This means we need to include threads that transitively+ −
wait for a resource being released (in the picture above this means the dependants+ −
of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"}, + −
but also @{text "th\<^isub>3"}, + −
which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which+ −
in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle 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+ −
where the dependants of @{text th} are given by the waiting queue function.+ −
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 the scheduler increase this+ −
precedence, if needed according to PIP. Therefore the current precedence of @{text th} is+ −
given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all + −
threads that are dependants of @{text th}. Since the notion @{term "dependants"} is+ −
defined as the transitive closure of all dependent threads, we deal correctly with the + −
problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is+ −
lowered prematurely.+ −
+ −
The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined+ −
by recursion on the state (a list of events); this function returns a \emph{schedule state}, which + −
we represent as a record consisting of two+ −
functions:+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
@{text "\<lparr>wq_fun, cprec_fun\<rparr>"}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The first function is a waiting queue function (that is, it takes a resource @{text "cs"} and returns the+ −
corresponding list of threads that 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 (the corresponding + −
function is defined in \eqref{allunlocked}) and the+ −
current precedence of every thread is initialised with @{term "Prc 0 0"}; that means + −
\mbox{@{abbrev initial_cprec}}. Therefore+ −
we have for the initial state+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ + −
\hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:+ −
we calculate the waiting queue function of the (previous) state @{text s}; + −
this waiting queue function @{text wq} is unchanged in the next schedule state---because+ −
none of these events lock or release any resource; + −
for calculating the next @{term "cprec_fun"}, we use @{text wq} and + −
@{term cpreced}. This gives the following three clauses for @{term schs}:+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ + −
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+ −
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\+ −
@{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\+ −
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+ −
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\+ −
@{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ + −
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+ −
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent + −
More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases+ −
we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update+ −
the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} + −
appended to the end of that list (remember the head of this list is seen to be in the possession of this+ −
resource). This gives the clause+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ + −
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+ −
\hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\+ −
\hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function+ −
so that the thread that possessed the lock is deleted from the corresponding thread list. For this + −
list transformation, we use+ −
the auxiliary function @{term release}. A simple version of @{term release} would+ −
just delete this thread and return the remaining threads, namely+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lcl}+ −
@{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\+ −
@{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
In practice, however, often the thread with the highest precedence in the list will get the+ −
lock next. We have implemented this choice, but later found out that the choice + −
of which thread is chosen next is actually irrelevant for the correctness of PIP.+ −
Therefore we prove the stronger result where @{term release} is defined as+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}lcl}+ −
@{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\+ −
@{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary+ −
choice for the next waiting list. It just has to be a list of distinctive threads and+ −
contain the same elements as @{text "qs"}. This gives for @{term V} the clause:+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\+ −
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\+ −
\hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\+ −
\hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
Having the scheduler function @{term schs} at our disposal, we can ``lift'', or+ −
overload, the notions+ −
@{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}rcl}+ −
@{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\+ −
@{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\+ −
@{thm (lhs) s_depend_abv} & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\+ −
@{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
With these abbreviations 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 "DUMMY ` DUMMY"} stands for the image of a set under a function.+ −
Note that in the initial state, that is where the list of events is empty, the set + −
@{term threads} is empty and therefore there is neither a thread ready nor running.+ −
If there is one or more threads ready, then there can only be \emph{one} thread+ −
running, namely the one whose current precedence is equal to the maximum of all ready + −
threads. We use the set-comprehension to capture both possibilities.+ −
We can now also conveniently define the set of resources that are locked by a thread in a+ −
given state.+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
@{thm holdents_def}+ −
\end{isabelle}+ −
+ −
Finally we can define what a \emph{valid state} is in our model of PIP. For+ −
example we cannot expect to be able to exit a thread, if it was not+ −
created yet. These validity constraints on states are characterised by the+ −
inductive predicate @{term "step"} and @{term vt}. We first give five inference rules+ −
for @{term step} relating a state and an event that can happen next.+ −
+ −
\begin{center}+ −
\begin{tabular}{c}+ −
@{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}+ −
@{thm[mode=Rule] thread_exit[where thread=th]}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
The first rule states that a thread can only be created, if it 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 (this simplifies slightly our model;+ −
in practice we would expect the operating system releases all held lock of a+ −
thread that is about to exit). The event @{text Set} can happen+ −
if the corresponding thread is running. + −
+ −
\begin{center}+ −
@{thm[mode=Rule] thread_set[where thread=th]}+ −
\end{center}+ −
+ −
\noindent+ −
If a thread wants to lock a resource, then the thread needs to be+ −
running and also we have to make sure that the resource lock does+ −
not lead to a cycle in the RAG. In practice, ensuring the latter is+ −
of course the responsibility of the programmer. In our formal+ −
model we just exclude such problematic cases in order to be able 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, one needs to perform an occurs+ −
check. But in practice the occurs check is ommited and the+ −
responsibility for avoiding problems rests with the programmer.}+ −
+ −
\begin{center}+ −
@{thm[mode=Rule] thread_P[where thread=th]}+ −
\end{center}+ −
+ −
\noindent+ −
Similarly, if a thread wants to release a lock on a resource, then+ −
it must be running and in the possession of that lock. This is+ −
formally given by the last inference rule of @{term step}.+ −
+ −
\begin{center}+ −
@{thm[mode=Rule] thread_V[where thread=th]}+ −
\end{center}+ −
+ −
\noindent+ −
A valid state of PIP can then be conveniently be defined as follows:+ −
+ −
\begin{center}+ −
\begin{tabular}{c}+ −
@{thm[mode=Axiom] vt_nil}\hspace{1cm}+ −
@{thm[mode=Rule] vt_cons}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
This completes our formal model of PIP. In the next section we present+ −
properties that show our model of PIP is correct.+ −
*}+ −
+ −
section {* The Correctness Proof *}+ −
+ −
(*<*)+ −
context extend_highest_gen+ −
begin+ −
print_locale extend_highest_gen+ −
thm extend_highest_gen_def+ −
thm extend_highest_gen_axioms_def+ −
thm highest_gen_def+ −
(*>*)+ −
text {* + −
Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion for PIP in terms+ −
of the number of critical resources: if there are @{text m} critical+ −
resources, then a blocked job can only be blocked @{text m} times---that is+ −
a bounded number of times.+ −
For their version of PIP, this property is \emph{not} true (as pointed out by + −
Yodaiken \cite{Yodaiken02}) as a high-priority thread can be+ −
blocked an unbounded number of times by creating medium-priority+ −
threads that block a thread, which in turn locks a critical resource and has+ −
too low priority to make progress. In the way we have set up our formal model of PIP, + −
their proof idea, even when fixed, does not seem to go through.+ −
+ −
The idea behind our correctness criterion of PIP is as follows: for all states+ −
@{text s}, we know the corresponding thread @{text th} with the highest precedence;+ −
we show that in every future state (denoted by @{text "s' @ s"}) in which+ −
@{text th} is still alive, either @{text th} is running or it is blocked by a + −
thread that was alive in the state @{text s}. Since in @{text s}, as in every + −
state, the set of alive threads is finite, @{text th} can only be blocked a+ −
finite number of times. We will actually prove a stricter bound below. However,+ −
this correctness criterion hinges upon a number of assumptions about the states+ −
@{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening+ −
in @{text s'}. We list them next:+ −
+ −
\begin{quote}+ −
{\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make + −
any meaningful statement, we need to require that @{text "s"} and + −
@{text "s' @ s"} are valid states, namely+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{l}+ −
@{term "vt s"}\\+ −
@{term "vt (s' @ s)"} + −
\end{tabular}+ −
\end{isabelle}+ −
\end{quote}+ −
+ −
\begin{quote}+ −
{\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and + −
has the highest precedence of all alive threads in @{text s}. Furthermore the+ −
priority of @{text th} is @{text prio} (we need this in the next assumptions).+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{l}+ −
@{term "th \<in> threads s"}\\+ −
@{term "prec th s = Max (cprec s ` threads s)"}\\+ −
@{term "prec th s = (prio, DUMMY)"}+ −
\end{tabular}+ −
\end{isabelle}+ −
\end{quote}+ −
+ −
\begin{quote}+ −
{\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot+ −
be blocked indefinitely. Of course this can happen if threads with higher priority+ −
than @{text th} are continously created in @{text s'}. Therefore we have to assume that + −
events in @{text s'} can only create (respectively set) threads with equal or lower + −
priority than @{text prio} of @{text th}. We also need to assume that the+ −
priority of @{text "th"} does not get reset and also that @{text th} does+ −
not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. + −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{l}+ −
{If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\+ −
{If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\+ −
{If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\+ −
\end{tabular}+ −
\end{isabelle}+ −
\end{quote}+ −
+ −
\noindent+ −
Under these assumptions we will prove the following correctness property:+ −
+ −
\begin{theorem}\label{mainthm}+ −
Given the assumptions about states @{text "s"} and @{text "s' @ s"},+ −
the thread @{text th} and the events in @{text "s'"},+ −
if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then+ −
@{text "th' \<in> threads s"}.+ −
\end{theorem}+ −
+ −
\noindent+ −
This theorem ensures that the thread @{text th}, which has the highest + −
precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} + −
by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,+ −
that means by only finitely many threads. Consequently, indefinite wait of+ −
@{text th}---which would be Priority Inversion---cannot occur.+ −
+ −
In what follows we will describe properties of PIP that allow us to prove + −
Theorem~\ref{mainthm}. It is relatively easily to see that+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text "running s \<subseteq> ready s \<subseteq> threads s"}\\+ −
@{thm[mode=IfThen] finite_threads}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where the second property is by induction of @{term vt}. The next three+ −
properties are + −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\+ −
@{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\+ −
@{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The first one states that every waiting thread can only wait for a single+ −
resource (because it gets suspended after requesting that resource and having+ −
to wait for it); the second that every resource can only be held by a single thread; + −
the third property establishes that in every given valid state, there is+ −
at most one running thread. We can also show the following properties + −
about the RAG in @{text "s"}.+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\+ −
\hspace{5mm}@{thm (concl) acyclic_depend},+ −
@{thm (concl) finite_depend} and+ −
@{thm (concl) wf_dep_converse},\\+ −
\hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}\\+ −
\hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
TODO+ −
+ −
\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 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}+ −
*}+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −
+ −
section {* Properties for an Implementation\label{implement}*}+ −
+ −
text {*+ −
While a formal correctness proof for our model of PIP is certainly+ −
attractive (especially in light of the flawed proof by Sha et+ −
al.~\cite{Sha90}), we found that the formalisation can even help us+ −
with efficiently implementing PIP.+ −
+ −
For example Baker complained that calculating the current precedence+ −
in PIP is quite ``heavy weight'' in Linux (see our Introduction).+ −
In our model of PIP the current precedence of a thread in a state s+ −
depends on all its dependants---a ``global'' transitive notion,+ −
which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).+ −
We can however prove how to improve upon this. For this let us+ −
define the notion of @{term children} of a thread as+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm children_def2}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
where a child is a thread that is one ``hop'' away in the @{term RAG} from the + −
tread @{text th} (and waiting for @{text th} to release a resource). We can prove that+ −
+ −
\begin{lemma}\label{childrenlem}+ −
@{text "If"} @{thm (prem 1) cp_rec} @{text "then"}+ −
\begin{center}+ −
@{thm (concl) cp_rec}.+ −
\end{center}+ −
\end{lemma}+ −
+ −
\noindent+ −
That means the current precedence of a thread @{text th} can be+ −
computed locally by considering only the children of @{text th}. In+ −
effect, it only needs to be recomputed for @{text th} when one of+ −
its children change their current precedence. Once the current + −
precedence is computed in this more efficient manner, the selection+ −
of the thread with highest precedence from a set of ready threads is+ −
a standard scheduling operation implemented in most operating+ −
systems.+ −
+ −
Of course the main implementation work for PIP involves the scheduler+ −
and coding how it should react to the events, for example which + −
datastructures need to be modified (mainly @{text RAG} and @{text cprec}).+ −
Below we outline how our formalisation guides this implementation for each + −
event.\smallskip+ −
*}+ −
+ −
(*<*)+ −
context step_create_cps+ −
begin+ −
(*>*)+ −
text {*+ −
\noindent+ −
@{term "Create th prio"}: We assume that the current state @{text s'} and + −
the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event+ −
is allowed to occur). In this situation we can show that+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm eq_dep}\\+ −
@{thm eq_cp_th}\\+ −
@{thm[mode=IfThen] eq_cp}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This means we do not have recalculate the @{text RAG} and also none of the+ −
current precedences of the other threads. The current precedence of the created+ −
thread is just its precedence, that is the pair @{term "(prio, length (s::event list))"}.+ −
\smallskip+ −
*}+ −
(*<*)+ −
end+ −
context step_exit_cps+ −
begin+ −
(*>*)+ −
text {*+ −
\noindent+ −
@{term "Exit th"}: We again assume that the current state @{text s'} and + −
the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm eq_dep}\\+ −
@{thm[mode=IfThen] eq_cp}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This means also we do not have to recalculate the @{text RAG} and+ −
not the current precedences for the other threads. Since @{term th} is not+ −
alive anymore in state @{term "s"}, there is no need to calculate its+ −
current precedence.+ −
\smallskip+ −
*}+ −
(*<*)+ −
end+ −
context step_set_cps+ −
begin+ −
(*>*)+ −
text {*+ −
\noindent+ −
@{term "Set th prio"}: We assume that @{text s'} and + −
@{term "s \<equiv> Set th prio#s'"} are both valid. We can show that+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm[mode=IfThen] eq_dep}\\+ −
@{thm[mode=IfThen] eq_cp}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The first is again telling us we do not need to change the @{text RAG}. The second+ −
however states that only threads that are \emph{not} dependent on @{text th} have their+ −
current precedence unchanged. For the others we have to recalculate the current+ −
precedence. To do this we can start from @{term "th"} + −
and follow the @{term "depend"}-chains to recompute the @{term "cp"} of every + −
thread encountered on the way using Lemma~\ref{childrenlem}. Since the @{term "depend"}+ −
is loop free, this procedure always stop. The the following two lemmas show this + −
procedure can actually stop often earlier.+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm[mode=IfThen] eq_up_self}\\+ −
@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\+ −
@{text "then"} @{thm (concl) eq_up}.+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
The first states that if the current precedence of @{text th} is unchanged,+ −
then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).+ −
The second states that if an intermediate @{term cp}-value does not change, then+ −
the procedure can also stop, because none of its dependent threads will+ −
have their current precedence changed.+ −
\smallskip+ −
*}+ −
+ −
(*<*)+ −
end+ −
context step_v_cps_nt+ −
begin+ −
(*>*)+ −
text {*+ −
\noindent+ −
@{term "V th cs"}: We assume that @{text s'} and + −
@{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two+ −
subcases: one where there is a thread to ``take over'' the released+ −
resource @{text cs}, and where there is not. Let us consider them+ −
in turn. Suppose in state @{text s}, the thread @{text th'} takes over+ −
resource @{text cs} from thread @{text th}. We can show+ −
+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
@{thm depend_s}+ −
\end{isabelle}+ −
+ −
\noindent+ −
which shows how the @{text RAG} needs to be changed. This also suggests+ −
how the current precedences need to be recalculated. For threads that are+ −
not @{text "th"} and @{text "th'"} nothing needs to be changed, since we+ −
can show+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
@{thm[mode=IfThen] cp_kept}+ −
\end{isabelle}+ −
+ −
\noindent+ −
For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to+ −
recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*+ −
\noindent+ −
In the other case where there is no thread that takes over @{text cs}, we can show how+ −
to recalculate the @{text RAG} and also show that no current precedence needs+ −
to be recalculated, except for @{text th} (like in the case above).+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm depend_s}\\+ −
@{thm eq_cp}+ −
\end{tabular}+ −
\end{isabelle}+ −
*}+ −
(*<*)+ −
end+ −
context step_P_cps_e+ −
begin+ −
(*>*)+ −
+ −
text {*+ −
\noindent+ −
@{term "P th cs"}: We assume that @{text s'} and + −
@{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely+ −
the one where @{text cs} is locked, and where it is not. We treat the second case+ −
first by showing that+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm depend_s}\\+ −
@{thm eq_cp}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
This means we do not need to add a holding edge to the @{text RAG} and no+ −
current precedence must be recalculated (including that for @{text th}).*}(*<*)end context step_P_cps_ne begin(*>*) text {*+ −
\noindent+ −
In the second case we know that resouce @{text cs} is locked. We can show that+ −
+ −
\begin{isabelle}\ \ \ \ \ %%%+ −
\begin{tabular}{@ {}l}+ −
@{thm depend_s}\\+ −
@{thm[mode=IfThen] eq_cp}+ −
\end{tabular}+ −
\end{isabelle}+ −
+ −
\noindent+ −
That means we have to add a waiting edge to the @{text RAG}. Furthermore+ −
the current precedence for all threads that are not dependent on @{text th}+ −
are unchanged. For the others we need to follow the @{term "depend"}-chains + −
in the @{text RAG} and recompute the @{term "cp"}. However, like in the + −
@{text Set}-event, this operation can stop often earlier, namely when intermediate+ −
values do not change.+ −
*}+ −
(*<*)+ −
end+ −
(*>*)+ −
+ −
text {*+ −
\noindent+ −
TO DO a few sentences summarising what has been achieved.+ −
*}+ −
+ −
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 {*+ −
+ −
*}+ −
+ −
section {* Key properties \label{extension} *}+ −
+ −
(*<*)+ −
context extend_highest_gen+ −
begin+ −
(*>*)+ −
+ −
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 {* 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+ −
(*>*)+ −