+
−
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. +
−
*}+
−
+
−
*)+
−