|
1 |
|
2 There are several works on inversion avoidance: |
|
3 \begin{enumerate} |
|
4 \item {\em Solving the group priority inversion problem in a timed asynchronous system}. |
|
5 The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. |
|
6 The method is by reordering requests in the setting of Client-Server. |
|
7 \item {\em Examples of inaccurate specification of the protocol}. |
|
8 \end{enumerate} |
|
9 |
|
10 |
|
11 |
|
12 |
|
13 |
|
14 |
|
15 section{* Related works *} |
|
16 |
|
17 text {* |
|
18 1. <<Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java>> models and |
|
19 verifies the combination of Priority Inheritance (PI) and Priority Ceiling Emulation (PCE) protocols in |
|
20 the setting of Java virtual machine using extended Timed Automata(TA) formalism of the UPPAAL tool. |
|
21 Although a detailed formal model of combined PI and PCE is given, the number of properties is quite |
|
22 small and the focus is put on the harmonious working of PI and PCE. Most key features of PI |
|
23 (as well as PCE) are not shown. Because of the limitation of the model checking technique |
|
24 used there, properties are shown only for a small number of scenarios. Therefore, the verification |
|
25 does not show the correctness of the formal model itself in a convincing way. |
|
26 2. << Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC>>. A formal model |
|
27 of PI is given in TLA+. Only 3 properties are shown for PI using model checking. The limitation of |
|
28 model checking is intrinsic to the work. |
|
29 3. <<Synchronous modeling and validation of priority inheritance schedulers>>. Gives a formal model |
|
30 of PI and PCE in AADL (Architecture Analysis & Design Language) and checked several properties |
|
31 using model checking. The number of properties shown there is less than here and the scale |
|
32 is also limited by the model checking technique. |
|
33 |
|
34 |
|
35 There are several works on inversion avoidance: |
|
36 1. <<Solving the group priority inversion problem in a timed asynchronous system>>. |
|
37 The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. |
|
38 The method is by reordering requests in the setting of Client-Server. |
|
39 |
|
40 |
|
41 <<Examples of inaccurate specification of the protocol>>. |
|
42 |
|
43 *} |
|
44 |
|
45 text {* |
|
46 |
|
47 \section{An overview of priority inversion and priority inheritance} |
|
48 |
|
49 Priority inversion refers to the phenomenon when a thread with high priority is blocked |
|
50 by a thread with low priority. Priority happens when the high priority thread requests |
|
51 for some critical resource already taken by the low priority thread. Since the high |
|
52 priority thread has to wait for the low priority thread to complete, it is said to be |
|
53 blocked by the low priority thread. Priority inversion might prevent high priority |
|
54 thread from fulfill its task in time if the duration of priority inversion is indefinite |
|
55 and unpredictable. Indefinite priority inversion happens when indefinite number |
|
56 of threads with medium priorities is activated during the period when the high |
|
57 priority thread is blocked by the low priority thread. Although these medium |
|
58 priority threads can not preempt the high priority thread directly, they are able |
|
59 to preempt the low priority threads and cause it to stay in critical section for |
|
60 an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. |
|
61 |
|
62 Priority inheritance is one protocol proposed to avoid indefinite priority inversion. |
|
63 The basic idea is to let the high priority thread donate its priority to the low priority |
|
64 thread holding the critical resource, so that it will not be preempted by medium priority |
|
65 threads. The thread with highest priority will not be blocked unless it is requesting |
|
66 some critical resource already taken by other threads. Viewed from a different angle, |
|
67 any thread which is able to block the highest priority threads must already hold some |
|
68 critical resource. Further more, it must have hold some critical resource at the |
|
69 moment the highest priority is created, otherwise, it may never get change to run and |
|
70 get hold. Since the number of such resource holding lower priority threads is finite, |
|
71 if every one of them finishes with its own critical section in a definite duration, |
|
72 the duration the highest priority thread is blocked is definite as well. The key to |
|
73 guarantee lower priority threads to finish in definite is to donate them the highest |
|
74 priority. In such cases, the lower priority threads is said to have inherited the |
|
75 highest priority. And this explains the name of the protocol: |
|
76 {\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay. |
|
77 |
|
78 The objectives of this paper are: |
|
79 \begin{enumerate} |
|
80 \item Build the above mentioned idea into formal model and prove a series of properties |
|
81 until we are convinced that the formal model does fulfill the original idea. |
|
82 \item Show how formally derived properties can be used as guidelines for correct |
|
83 and efficient implementation. |
|
84 \end{enumerate}. |
|
85 The proof is totally formal in the sense that every detail is reduced to the |
|
86 very first principles of Higher Order Logic. The nature of interactive theorem |
|
87 proving is for the human user to persuade computer program to accept its arguments. |
|
88 A clear and simple understanding of the problem at hand is both a prerequisite and a |
|
89 byproduct of such an effort, because everything has finally be reduced to the very |
|
90 first principle to be checked mechanically. The former intuitive explanation of |
|
91 Priority Inheritance is just such a byproduct. |
|
92 *} |
|
93 |
|
94 *) |