5 (*>*) |
5 (*>*) |
6 |
6 |
7 section {* Introduction *} |
7 section {* Introduction *} |
8 |
8 |
9 text {* |
9 text {* |
|
10 Many realtime systems need to support processes with priorities and |
|
11 locking of resources. Locking of resources ensures... Priorities |
|
12 are needed so that some processes can finish their work within ``hard'' |
|
13 deadlines. Unfortunately both features interact in subtle ways |
|
14 leading to the problem, called Priority Inversion. Suppose three |
|
15 processes with priorities $H$(igh), $M$(edium) and $L$(ow). We would |
|
16 assume that process $H$ cannot be blocked by any process with lower |
|
17 priority. Unfortunately in a naive implementation, this can happen |
|
18 and $H$ even can be delayed indefinitely by processes with lower |
|
19 priorities. For this let $L$ be in the posession of lock for a |
|
20 research which also $H$ needs. $H$ must therefore wait for $L$ to |
|
21 release this lock. Unfortunately, $L$ can in turn be blocked by any |
|
22 process with priority $M$, and so $H$ sits there potentially waiting |
|
23 indefinitely. |
|
24 |
|
25 If this problem of inversion of priorities is left untreated, |
|
26 systems can become unpredictable and have dire consequences. The |
|
27 classic example where this happened in practice is the software on |
|
28 the Mars pathfinder project. This software shut down at irregulare |
|
29 intervals leading to loss of project time (the mission and data was |
|
30 fortunately not lost, because of clever system design). The problem |
|
31 was that a high priority process and could only be restarted the |
|
32 next day. |
|
33 |
10 |
34 |
11 Priority inversion referrers to the phenomena where tasks with higher |
35 Priority inversion referrers to the phenomena where tasks with higher |
12 priority are blocked by ones with lower priority. If priority inversion |
36 priority are blocked by ones with lower priority. If priority inversion |
13 is not controlled, there will be no guarantee the urgent tasks will be |
37 is not controlled, there will be no guarantee the urgent tasks will be |
14 processed in time. As reported in \cite{Reeves-Glenn-1998}, |
38 processed in time. As reported in \cite{Reeves-Glenn-1998}, |
54 of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} |
78 of PI. Section \ref{model} introduces the formal model of PI. Section \ref{general} |
55 discusses a series of basic properties of PI. Section \ref{extension} shows formally |
79 discusses a series of basic properties of PI. Section \ref{extension} shows formally |
56 how priority inversion is controlled by PI. Section \ref{implement} gives properties |
80 how priority inversion is controlled by PI. Section \ref{implement} gives properties |
57 which can be used for guidelines of implementation. Section \ref{related} discusses |
81 which can be used for guidelines of implementation. Section \ref{related} discusses |
58 related works. Section \ref{conclusion} concludes the whole paper. |
82 related works. Section \ref{conclusion} concludes the whole paper. |
|
83 |
|
84 |
|
85 Contributions |
|
86 |
|
87 Despite the wide use of Priority Inheritance Protocol in real time operating |
|
88 system, it's correctness has never been formally proved and mechanically checked. |
|
89 All existing verification are based on model checking technology. Full automatic |
|
90 verification gives little help to understand why the protocol is correct. |
|
91 And results such obtained only apply to models of limited size. |
|
92 This paper presents a formal verification based on theorem proving. |
|
93 Machine checked formal proof does help to get deeper understanding. We found |
|
94 the fact which is not mentioned in the literature, that the choice of next |
|
95 thread to take over when an critical resource is release does not affect the correctness |
|
96 of the protocol. The paper also shows how formal proof can help to construct |
|
97 correct and efficient implementation.\bigskip |
|
98 |
59 *} |
99 *} |
60 |
100 |
61 section {* An overview of priority inversion and priority inheritance \label{overview} *} |
101 section {* An overview of priority inversion and priority inheritance \label{overview} *} |
62 |
102 |
63 text {* |
103 text {* |