1 (*<*)

     2 theory Paper

     3 imports CpsG ExtGG

     4 begin

     5 (*>*)

     6 

     7 section {* Introduction *}

     8 

     9 text {*

    10 

    11   Priority inversion referrers to the phenomena where tasks with higher 

    12   priority are blocked by ones with lower priority. If priority inversion 

    13   is not controlled, there will be no guarantee the urgent tasks will be 

    14   processed in time. As reported in \cite{Reeves-Glenn-1998}, 

    15   priority inversion used to cause software system resets and data lose in 

    16   JPL's Mars pathfinder project. Therefore, the avoiding, detecting and controlling 

    17   of priority inversion is a key issue to attain predictability in priority 

    18   based real-time systems. 

    19 

    20   The priority inversion phenomenon was first published in \cite{Lampson:Redell:cacm:1980}. 

    21   The two protocols widely used to eliminate priority inversion, namely 

    22   PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed 

    23   in \cite{journals/tc/ShaRL90}. PCE is less convenient to use because it requires 

    24   static analysis of programs. Therefore, PI is more commonly used in 

    25   practice\cite{locke-july02}. However, as pointed out in the literature, 

    26   the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}. 

    27   A formal analysis will certainly be helpful for us to understand and correctly 

    28   implement PI. All existing formal analysis of PI

    29   \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the model checking 

    30   technology. Because of the state explosion problem, model check 

    31   is much like an exhaustive testing of finite models with limited size. 

    32   The results obtained can not be safely generalized to models with arbitrarily 

    33   large size. Worse still, since model checking is fully automatic, it give little 

    34   insight on why the formal model is correct. It is therefore 

    35   definitely desirable to analyze PI using theorem proving, which gives 

    36   more general results as well as deeper insight. And this is the purpose 

    37   of this paper which gives a formal analysis of PI in the interactive 

    38   theorem prover Isabelle using Higher Order Logic (HOL). The formalization 

    39   focuses on on two issues:

    40 

    41   \begin{enumerate}

    42   \item The correctness of the protocol model itself. A series of desirable properties is 

    43     derived until we are fully convinced that the formal model of PI does 

    44     eliminate priority inversion. And a better understanding of PI is so obtained 

    45     in due course. For example, we find through formalization that the choice of 

    46     next thread to take hold when a 

    47     resource is released is irrelevant for the very basic property of PI to hold. 

    48     A point never mentioned in literature. 

    49   \item The correctness of the implementation. A series of properties is derived the meaning 

    50     of which can be used as guidelines on how PI can be implemented efficiently and correctly. 

    51   \end{enumerate} 

    52 

    53   The rest of the paper is organized as follows: Section \ref{overview} gives an overview 

    54   of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} 

    55   discusses a series of basic properties of PI. Section \ref{extension} shows formally 

    56   how priority inversion is controlled by PI. Section \ref{implement} gives properties 

    57   which can be used for guidelines of implementation. Section \ref{related} discusses 

    58   related works. Section \ref{conclusion} concludes the whole paper.

    59 *}

    60 

    61 section {* An overview of priority inversion and priority inheritance \label{overview} *}

    62 

    63 text {*

    64 

    65   Priority inversion refers to the phenomenon when a thread with high priority is blocked 

    66   by a thread with low priority. Priority happens when the high priority thread requests 

    67   for some critical resource already taken by the low priority thread. Since the high 

    68   priority thread has to wait for the low priority thread to complete, it is said to be 

    69   blocked by the low priority thread. Priority inversion might prevent high priority 

    70   thread from fulfill its task in time if the duration of priority inversion is indefinite 

    71   and unpredictable. Indefinite priority inversion happens when indefinite number 

    72   of threads with medium priorities is activated during the period when the high 

    73   priority thread is blocked by the low priority thread. Although these medium 

    74   priority threads can not preempt the high priority thread directly, they are able 

    75   to preempt the low priority threads and cause it to stay in critical section for 

    76   an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. 

    77   

    78   Priority inheritance is one protocol proposed to avoid indefinite priority inversion. 

    79   The basic idea is to let the high priority thread donate its priority to the low priority 

    80   thread holding the critical resource, so that it will not be preempted by medium priority 

    81   threads. The thread with highest priority will not be blocked unless it is requesting 

    82   some critical resource already taken by other threads. Viewed from a different angle, 

    83   any thread which is able to block the highest priority threads must already hold some 

    84   critical resource. Further more, it must have hold some critical resource at the 

    85   moment the highest priority is created, otherwise, it may never get change to run and 

    86   get hold. Since the number of such resource holding lower priority threads is finite, 

    87   if every one of them finishes with its own critical section in a definite duration, 

    88   the duration the highest priority thread is blocked is definite as well. The key to 

    89   guarantee lower priority threads to finish in definite is to donate them the highest 

    90   priority. In such cases, the lower priority threads is said to have inherited the 

    91   highest priority. And this explains the name of the protocol: 

    92   {\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.

    93 

    94   The objectives of this paper are:

    95   \begin{enumerate}

    96   \item Build the above mentioned idea into formal model and prove a series of properties 

    97     until we are convinced that the formal model does fulfill the original idea. 

    98   \item Show how formally derived properties can be used as guidelines for correct 

    99     and efficient implementation.

   100   \end{enumerate}

   101   The proof is totally formal in the sense that every detail is reduced to the 

   102   very first principles of Higher Order Logic. The nature of interactive theorem 

   103   proving is for the human user to persuade computer program to accept its arguments. 

   104   A clear and simple understanding of the problem at hand is both a prerequisite and a 

   105   byproduct of such an effort, because everything has finally be reduced to the very 

   106   first principle to be checked mechanically. The former intuitive explanation of 

   107   Priority Inheritance is just such a byproduct. 

   108   *}

   109 

   110 section {* Formal model of Priority Inheritance \label{model} *}

   111 text {*

   112   \input{../../generated/PrioGDef}

   113 *}

   114 

   115 section {* General properties of Priority Inheritance \label{general} *}

   116 

   117 section {* Key properties \label{extension} *}

   118 

   119 section {* Properties to guide implementation \label{implement} *}

   120 

   121 section {* Related works \label{related} *}

   122 

   123 text {*

   124   \begin{enumerate}

   125   \item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}

   126     \cite{WellingsBSB07} models and verifies the combination of Priority Inheritance (PI) and 

   127     Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine 

   128     using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed 

   129     formal model of combined PI and PCE is given, the number of properties is quite 

   130     small and the focus is put on the harmonious working of PI and PCE. Most key features of PI 

   131     (as well as PCE) are not shown. Because of the limitation of the model checking technique

   132     used there, properties are shown only for a small number of scenarios. Therefore, 

   133     the verification does not show the correctness of the formal model itself in a 

   134     convincing way.  

   135   \item {\em Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC}

   136     \cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown 

   137     for PI using model checking. The limitation of model checking is intrinsic to the work.

   138   \item {\em Synchronous modeling and validation of priority inheritance schedulers}

   139     \cite{conf/fase/JahierHR09}. Gives a formal model

   140     of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked 

   141     several properties using model checking. The number of properties shown there is 

   142     less than here and the scale is also limited by the model checking technique. 

   143   \item {\em The Priority Ceiling Protocol: Formalization and Analysis Using PVS}

   144     \cite{dutertre99b}. Formalized another protocol for Priority Inversion in the 

   145     interactive theorem proving system PVS.

   146 \end{enumerate}

   147 

   148 

   149   There are several works on inversion avoidance:

   150   \begin{enumerate}

   151   \item {\em Solving the group priority inversion problem in a timed asynchronous system}

   152     \cite{Wang:2002:SGP}. The notion of Group Priority Inversion is introduced. The main 

   153     strategy is still inversion avoidance. The method is by reordering requests 

   154     in the setting of Client-Server.

   155   \item {\em A Formalization of Priority Inversion} \cite{journals/rts/BabaogluMS93}. 

   156     Formalized the notion of Priority 

   157     Inversion and proposes methods to avoid it. 

   158   \end{enumerate}

   159 

   160   {\em Examples of inaccurate specification of the protocol ???}.

   161 

   162 *}

   163 

   164 section {* Conclusions \label{conclusion} *}

   165 

   166 (*<*)

   167 end

   168 (*>*)