(*<*)+
−
theory Paper+
−
imports CpsG ExtGG+
−
begin+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
+
−
  Priority inversion referrers to the phenomena where tasks with higher +
−
  priority are blocked by ones with lower priority. If priority inversion +
−
  is not controlled, there will be no guarantee the urgent tasks will be +
−
  processed in time. As reported in \cite{Reeves-Glenn-1998}, +
−
  priority inversion used to cause software system resets and data lose in +
−
  JPL's Mars pathfinder project. Therefore, the avoiding, detecting and controlling +
−
  of priority inversion is a key issue to attain predictability in priority +
−
  based real-time systems. +
−
+
−
  The priority inversion phenomenon was first published in \cite{Lampson:Redell:cacm:1980}. +
−
  The two protocols widely used to eliminate priority inversion, namely +
−
  PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed +
−
  in \cite{journals/tc/ShaRL90}. 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.+
−
*}+
−
+
−
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} *}+
−
+
−
section {* Key properties \label{extension} *}+
−
+
−
section {* Properties to guide implementation \label{implement} *}+
−
+
−
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+
−
(*>*)+
−