--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Paper/Paper.thy Tue Jan 24 00:20:09 2012 +0000
@@ -0,0 +1,168 @@
+(*<*)
+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
+(*>*)
\ No newline at end of file