(*<*)
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
(*>*)