--- a/Paper/tt.thy	Tue Mar 04 15:30:24 2014 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-
-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. 
-*}
-
-*)