diff -r c4783e4ef43f -r a04084de4946 Paper/tt.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/tt.thy	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,94 @@
+
+There are several works on inversion avoidance:
+\begin{enumerate}
+\item {\em Solving the group priority inversion problem in a timed asynchronous system}. 
+The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. 
+The method is by reordering requests in the setting of Client-Server.
+\item {\em Examples of inaccurate specification of the protocol}.
+\end{enumerate}
+
+
+
+
+
+
+section{* Related works *}
+
+text {*
+1.	<<Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java>> 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.  
+2.	<< Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC>>. 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.
+3.	<<Synchronous modeling and validation of priority inheritance schedulers>>. 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. 
+
+
+There are several works on inversion avoidance:
+1.	<<Solving the group priority inversion problem in a timed asynchronous system>>. 
+The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. 
+The method is by reordering requests in the setting of Client-Server.
+
+
+<<Examples of inaccurate specification of the protocol>>.
+
+*}
+
+text {*
+
+\section{An overview of priority inversion and priority inheritance}
+
+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. 
+*}
+
+*)