(*<*)
theory Paper
imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar
begin
ML {*
open Printer;
show_question_marks_default := false;
*}
notation (latex output)
Cons ("_::_" [78,77] 73) and
vt ("valid'_state") and
runing ("running") and
birthtime ("inception") and
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
section {* Introduction *}
text {*
Many real-time systems need to support threads involving priorities and
locking of resources. Locking of resources ensures mutual exclusion
when accessing shared data or devices that cannot be
preempted. Priorities allow scheduling of threads that need to
finish their work within deadlines. Unfortunately, both features
can interact in subtle ways leading to a problem, called
\emph{Priority Inversion}. Suppose three threads having priorities
$H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
$H$ blocks any other thread with lower priority and itself cannot
be blocked by any thread with lower priority. Alas, in a naive
implementation of resource looking and priorities this property can
be violated. Even worse, $H$ can be delayed indefinitely by
threads with lower priorities. For this let $L$ be in the
possession of a lock for a resource that also $H$ needs. $H$ must
therefore wait for $L$ to exit the critical section and release this
lock. The problem is that $L$ might in turn be blocked by any
thread with priority $M$, and so $H$ sits there potentially waiting
indefinitely. Since $H$ is blocked by threads with lower
priorities, the problem is called Priority Inversion. It was first
described in \cite{Lampson80} in the context of the
Mesa programming language designed for concurrent programming.
If the problem of Priority Inversion is ignored, real-time systems
can become unpredictable and resulting bugs can be hard to diagnose.
The classic example where this happened is the software that
controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
Once the spacecraft landed, the software shut down at irregular
intervals leading to loss of project time as normal operation of the
craft could only resume the next day (the mission and data already
collected were fortunately not lost, because of a clever system
design). The reason for the shutdowns was that the scheduling
software fell victim of Priority Inversion: a low priority thread
locking a resource prevented a high priority thread from running in
time leading to a system reset. Once the problem was found, it was
rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
\cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
Inheritance Protocol} \cite{Sha90} and others sometimes call it
also \emph{Priority Boosting}.} in the scheduling software.
The idea behind PIP is to let the thread $L$ temporarily inherit
the high priority from $H$ until $L$ leaves the critical section by
unlocking the resource. This solves the problem of $H$ having to
wait indefinitely, because $L$ cannot be blocked by threads having
priority $M$. While a few other solutions exist for the Priority
Inversion problem, PIP is one that is widely deployed and
implemented. This includes VxWorks (a proprietary real-time OS used
in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
example in libraries for FreeBSD, Solaris and Linux.
One advantage of PIP is that increasing the priority of a thread
can be dynamically calculated by the scheduler. This is in contrast
to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
solution to the Priority Inversion problem, which requires static
analysis of the program in order to prevent Priority
Inversion. However, there has also been strong criticism against
PIP. For instance, PIP cannot prevent deadlocks when lock
dependencies are circular, and also blocking times can be
substantial (more than just the duration of a critical section).
Though, most criticism against PIP centres around unreliable
implementations and PIP being too complicated and too inefficient.
For example, Yodaiken writes in \cite{Yodaiken02}:
\begin{quote}
\it{}``Priority inheritance is neither efficient nor reliable. Implementations
are either incomplete (and unreliable) or surprisingly complex and intrusive.''
\end{quote}
\noindent
He suggests to avoid PIP altogether by not allowing critical
sections to be preempted. While this might have been a reasonable
solution in 2002, in our modern multiprocessor world, this seems out
of date. The reason is that this precludes other high-priority
threads from running even when they do not make any use of the locked
resource.
However, there is clearly a need for investigating correct
algorithms for PIP. A few specifications for PIP exist (in English)
and also a few high-level descriptions of implementations (e.g.~in
the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
with actual implementations. That this is a problem in practise is
proved by an email from Baker, who wrote on 13 July 2009 on the Linux
Kernel mailing list:
\begin{quote}
\it{}``I observed in the kernel code (to my disgust), the Linux PIP
implementation is a nightmare: extremely heavy weight, involving
maintenance of a full wait-for graph, and requiring updates for a
range of events, including priority changes and interruptions of
wait operations.''
\end{quote}
\noindent
The criticism by Yodaiken, Baker and others suggests to us to look
again at PIP from a more abstract level (but still concrete enough
to inform an implementation) and makes PIP an ideal candidate for a
formal verification. One reason, of course, is that the original
presentation of PIP~\cite{Sha90}, despite being informally
``proved'' correct, is actually \emph{flawed}.
Yodaiken \cite{Yodaiken02} points to a subtlety that had been
overlooked in the informal proof by Sha et al. They specify in
\cite{Sha90} that after the thread (whose priority has been raised)
completes its critical section and releases the lock, it ``returns
to its original priority level.'' This leads them to believe that an
implementation of PIP is ``rather straightforward''~\cite{Sha90}.
Unfortunately, as Yodaiken points out, this behaviour is too
simplistic. Consider the case where the low priority thread $L$
locks \emph{two} resources, and two high-priority threads $H$ and
$H'$ each wait for one of them. If $L$ then releases one resource
so that $H$, say, can proceed, then we still have Priority Inversion
with $H'$ (which waits for the other resource). The correct
behaviour for $L$ is to revert to the highest remaining priority of
the threads that it blocks. The advantage of formalising the
correctness of a high-level specification of PIP in a theorem prover
is that such issues clearly show up and cannot be overlooked as in
informal reasoning (since we have to analyse all possible behaviours
of threads, i.e.~\emph{traces}, that could possibly happen).
There have been earlier formal investigations into PIP, but ...\cite{Faria08}
vt (valid trace) was introduced earlier, cite
distributed PIP
*}
section {* Formal Model of the Priority Inheritance Protocol *}
text {*
We follow the original work by Sha et al.~\cite{Sha90} by modelling
first a classical single CPU system where only one \emph{thread} is
active at any given moment. We shall discuss later how to lift this
restriction. Our model of PIP is based on Paulson's inductive
approach to protocol verification \cite{Paulson98}, where the
\emph{state} of a system is given by a list of events that
happened so far. \emph{Events} fall into four categories defined as
the datatype
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
\isacommand{datatype} event
& @{text "="} & @{term "Create thread priority"}\\
& @{text "|"} & @{term "Exit thread"} \\
& @{text "|"} & @{term "Set thread priority"} & {\rm reset of the proprity for} @{text thread}\\
& @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
& @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
\end{tabular}}
\end{isabelle}
\noindent
whereby threads, priorities and (critical) resources are represented
as natural numbers. As in Paulson's work, we need to define
functions that allow one to make some observations about states.
One is the ``live'' threads we have seen so far in a state:
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
@{thm (rhs) threads.simps(1)}\\
@{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} &
@{thm (rhs) threads.simps(2)[where thread="th"]}\\
@{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
@{thm (rhs) threads.simps(3)[where thread="th"]}\\
@{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
\end{tabular}}
\end{isabelle}
\noindent
Another is that given a thread @{text "th"}, what is the original priority was at
its inception.
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
@{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
@{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
@{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
@{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
@{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
@{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
\end{tabular}}
\end{isabelle}
\noindent
In this definition we set @{text 0} as the default priority for
threads that have not (yet) been created. The last function we need
calculates the ``time'', or index, at which a process was created.
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
@{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
@{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
@{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
@{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
@{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
@{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
\end{tabular}}
\end{isabelle}
\begin{center}
threads, original-priority, birth time, precedence.
\end{center}
resources
step relation:
\begin{center}
\begin{tabular}{c}
@{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
@{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\
@{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
@{thm[mode=Rule] thread_V[where thread=th]}\\
\end{tabular}
\end{center}
valid state:
\begin{center}
\begin{tabular}{c}
@{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm}
@{thm[mode=Rule] vt_cons[where cs=step]}
\end{tabular}
\end{center}
To define events, the identifiers of {\em threads},
{\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
need to be represented. All three are represetned using standard
Isabelle/HOL type @{typ "nat"}:
*}
text {*
\bigskip
The priority inversion phenomenon was first published in
\cite{Lampson80}. The two protocols widely used to eliminate
priority inversion, namely PI (Priority Inheritance) and PCE
(Priority Ceiling Emulation), were proposed in \cite{Sha90}. PCE is
less convenient to use because it requires static analysis of
programs. Therefore, PI is more commonly used in
practice\cite{locke-july02}. However, as pointed out in the
literature, the analysis of priority inheritance protocol is quite
subtle\cite{yodaiken-july02}. A formal analysis will certainly be
helpful for us to understand and correctly implement PI. All
existing formal analysis of PI
\cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the
model checking technology. Because of the state explosion problem,
model check is much like an exhaustive testing of finite models with
limited size. The results obtained can not be safely generalized to
models with arbitrarily large size. Worse still, since model
checking is fully automatic, it give little insight on why the
formal model is correct. It is therefore definitely desirable to
analyze PI using theorem proving, which gives more general results
as well as deeper insight. And this is the purpose of this paper
which gives a formal analysis of PI in the interactive theorem
prover Isabelle using Higher Order Logic (HOL). The formalization
focuses on on two issues:
\begin{enumerate}
\item The correctness of the protocol model itself. A series of desirable properties is
derived until we are fully convinced that the formal model of PI does
eliminate priority inversion. And a better understanding of PI is so obtained
in due course. For example, we find through formalization that the choice of
next thread to take hold when a
resource is released is irrelevant for the very basic property of PI to hold.
A point never mentioned in literature.
\item The correctness of the implementation. A series of properties is derived the meaning
of which can be used as guidelines on how PI can be implemented efficiently and correctly.
\end{enumerate}
The rest of the paper is organized as follows: Section \ref{overview} gives an overview
of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general}
discusses a series of basic properties of PI. Section \ref{extension} shows formally
how priority inversion is controlled by PI. Section \ref{implement} gives properties
which can be used for guidelines of implementation. Section \ref{related} discusses
related works. Section \ref{conclusion} concludes the whole paper.
The basic priority inheritance protocol has two problems:
It does not prevent a deadlock from happening in a program with circular lock dependencies.
A chain of blocking may be formed; blocking duration can be substantial, though bounded.
Contributions
Despite the wide use of Priority Inheritance Protocol in real time operating
system, it's correctness has never been formally proved and mechanically checked.
All existing verification are based on model checking technology. Full automatic
verification gives little help to understand why the protocol is correct.
And results such obtained only apply to models of limited size.
This paper presents a formal verification based on theorem proving.
Machine checked formal proof does help to get deeper understanding. We found
the fact which is not mentioned in the literature, that the choice of next
thread to take over when an critical resource is release does not affect the correctness
of the protocol. The paper also shows how formal proof can help to construct
correct and efficient implementation.\bigskip
*}
section {* An overview of priority inversion and priority inheritance \label{overview} *}
text {*
Priority inversion refers to the phenomenon when a thread with high priority is blocked
by a thread with low priority. Priority happens when the high priority thread requests
for some critical resource already taken by the low priority thread. Since the high
priority thread has to wait for the low priority thread to complete, it is said to be
blocked by the low priority thread. Priority inversion might prevent high priority
thread from fulfill its task in time if the duration of priority inversion is indefinite
and unpredictable. Indefinite priority inversion happens when indefinite number
of threads with medium priorities is activated during the period when the high
priority thread is blocked by the low priority thread. Although these medium
priority threads can not preempt the high priority thread directly, they are able
to preempt the low priority threads and cause it to stay in critical section for
an indefinite long duration. In this way, the high priority thread may be blocked indefinitely.
Priority inheritance is one protocol proposed to avoid indefinite priority inversion.
The basic idea is to let the high priority thread donate its priority to the low priority
thread holding the critical resource, so that it will not be preempted by medium priority
threads. The thread with highest priority will not be blocked unless it is requesting
some critical resource already taken by other threads. Viewed from a different angle,
any thread which is able to block the highest priority threads must already hold some
critical resource. Further more, it must have hold some critical resource at the
moment the highest priority is created, otherwise, it may never get change to run and
get hold. Since the number of such resource holding lower priority threads is finite,
if every one of them finishes with its own critical section in a definite duration,
the duration the highest priority thread is blocked is definite as well. The key to
guarantee lower priority threads to finish in definite is to donate them the highest
priority. In such cases, the lower priority threads is said to have inherited the
highest priority. And this explains the name of the protocol:
{\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.
The objectives of this paper are:
\begin{enumerate}
\item Build the above mentioned idea into formal model and prove a series of properties
until we are convinced that the formal model does fulfill the original idea.
\item Show how formally derived properties can be used as guidelines for correct
and efficient implementation.
\end{enumerate}
The proof is totally formal in the sense that every detail is reduced to the
very first principles of Higher Order Logic. The nature of interactive theorem
proving is for the human user to persuade computer program to accept its arguments.
A clear and simple understanding of the problem at hand is both a prerequisite and a
byproduct of such an effort, because everything has finally be reduced to the very
first principle to be checked mechanically. The former intuitive explanation of
Priority Inheritance is just such a byproduct.
*}
section {* Formal model of Priority Inheritance \label{model} *}
text {*
\input{../../generated/PrioGDef}
*}
section {* General properties of Priority Inheritance \label{general} *}
text {*
The following are several very basic prioprites:
\begin{enumerate}
\item All runing threads must be ready (@{text "runing_ready"}):
@{thm[display] "runing_ready"}
\item All ready threads must be living (@{text "readys_threads"}):
@{thm[display] "readys_threads"}
\item There are finite many living threads at any moment (@{text "finite_threads"}):
@{thm[display] "finite_threads"}
\item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}):
@{thm[display] "wq_distinct"}
\item All threads in waiting queues are living threads (@{text "wq_threads"}):
@{thm[display] "wq_threads"}
\item The event which can get a thread into waiting queue must be @{term "P"}-events
(@{text "block_pre"}):
@{thm[display] "block_pre"}
\item A thread may never wait for two different critical resources
(@{text "waiting_unique"}):
@{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
\item Every resource can only be held by one thread
(@{text "held_unique"}):
@{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
\item Every living thread has an unique precedence
(@{text "preced_unique"}):
@{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
\end{enumerate}
*}
text {* \noindent
The following lemmas show how RAG is changed with the execution of events:
\begin{enumerate}
\item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
@{thm[display] depend_set_unchanged}
\item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
@{thm[display] depend_create_unchanged}
\item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
@{thm[display] depend_exit_unchanged}
\item Execution of @{term "P"} (@{text "step_depend_p"}):
@{thm[display] step_depend_p}
\item Execution of @{term "V"} (@{text "step_depend_v"}):
@{thm[display] step_depend_v}
\end{enumerate}
*}
text {* \noindent
These properties are used to derive the following important results about RAG:
\begin{enumerate}
\item RAG is loop free (@{text "acyclic_depend"}):
@{thm [display] acyclic_depend}
\item RAGs are finite (@{text "finite_depend"}):
@{thm [display] finite_depend}
\item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
@{thm [display] wf_dep_converse}
\item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
@{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
\item All threads in RAG are living threads
(@{text "dm_depend_threads"} and @{text "range_in"}):
@{thm [display] dm_depend_threads range_in}
\end{enumerate}
*}
text {* \noindent
The following lemmas show how every node in RAG can be chased to ready threads:
\begin{enumerate}
\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
@{thm [display] chain_building[rule_format]}
\item The ready thread chased to is unique (@{text "dchain_unique"}):
@{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
\end{enumerate}
*}
text {* \noindent
Properties about @{term "next_th"}:
\begin{enumerate}
\item The thread taking over is different from the thread which is releasing
(@{text "next_th_neq"}):
@{thm [display] next_th_neq}
\item The thread taking over is unique
(@{text "next_th_unique"}):
@{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}
\end{enumerate}
*}
text {* \noindent
Some deeper results about the system:
\begin{enumerate}
\item There can only be one running thread (@{text "runing_unique"}):
@{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
@{thm [display] max_cp_eq}
\item There must be one ready thread having the max @{term "cp"}-value
(@{text "max_cp_readys_threads"}):
@{thm [display] max_cp_readys_threads}
\end{enumerate}
*}
text {* \noindent
The relationship between the count of @{text "P"} and @{text "V"} and the number of
critical resources held by a thread is given as follows:
\begin{enumerate}
\item The @{term "V"}-operation decreases the number of critical resources
one thread holds (@{text "cntCS_v_dec"})
@{thm [display] cntCS_v_dec}
\item The number of @{text "V"} never exceeds the number of @{text "P"}
(@{text "cnp_cnv_cncs"}):
@{thm [display] cnp_cnv_cncs}
\item The number of @{text "V"} equals the number of @{text "P"} when
the relevant thread is not living:
(@{text "cnp_cnv_eq"}):
@{thm [display] cnp_cnv_eq}
\item When a thread is not living, it does not hold any critical resource
(@{text "not_thread_holdents"}):
@{thm [display] not_thread_holdents}
\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant
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_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 {* 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,conf/fase/JahierHR09,WellingsBSB07} 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_cps
begin
(*>*)
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_nt
begin
(*>*)
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}
*}
(*<*)
end
context step_v_cps_nnt
begin
(*>*)
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_e
begin
(*>*)
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}
*}
(*<*)
end
context step_P_cps_ne
begin
(*>*)
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_cps
begin
(*>*)
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_cps
begin
(*>*)
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{WellingsBSB07} 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{conf/fase/JahierHR09}. 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} *}
(*<*)
end
(*>*)