diff -r da7a6ccfa7a9 -r 6b1141c5e24c Paper/tt.thy --- 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 \\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 Examples of inaccurate specification of the protocol}. -\end{enumerate} - - - - - - -section{* Related works *} - -text {* -1. <> 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. <>. 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. <>. -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. - - -<>. - -*} - -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. -*} - -*)