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. 

*}

*)