|
262
|
1 |
(*<*)
|
|
|
2 |
theory Paper
|
|
264
|
3 |
imports CpsG ExtGG LaTeXsugar
|
|
262
|
4 |
begin
|
|
|
5 |
(*>*)
|
|
|
6 |
|
|
|
7 |
section {* Introduction *}
|
|
|
8 |
|
|
|
9 |
text {*
|
|
|
10 |
|
|
|
11 |
Priority inversion referrers to the phenomena where tasks with higher
|
|
|
12 |
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
|
|
|
14 |
processed in time. As reported in \cite{Reeves-Glenn-1998},
|
|
|
15 |
priority inversion used to cause software system resets and data lose in
|
|
|
16 |
JPL's Mars pathfinder project. Therefore, the avoiding, detecting and controlling
|
|
|
17 |
of priority inversion is a key issue to attain predictability in priority
|
|
|
18 |
based real-time systems.
|
|
|
19 |
|
|
|
20 |
The priority inversion phenomenon was first published in \cite{Lampson:Redell:cacm:1980}.
|
|
|
21 |
The two protocols widely used to eliminate priority inversion, namely
|
|
|
22 |
PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed
|
|
|
23 |
in \cite{journals/tc/ShaRL90}. PCE is less convenient to use because it requires
|
|
|
24 |
static analysis of programs. Therefore, PI is more commonly used in
|
|
|
25 |
practice\cite{locke-july02}. However, as pointed out in the literature,
|
|
|
26 |
the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}.
|
|
|
27 |
A formal analysis will certainly be helpful for us to understand and correctly
|
|
|
28 |
implement PI. All existing formal analysis of PI
|
|
|
29 |
\cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the model checking
|
|
|
30 |
technology. Because of the state explosion problem, model check
|
|
|
31 |
is much like an exhaustive testing of finite models with limited size.
|
|
|
32 |
The results obtained can not be safely generalized to models with arbitrarily
|
|
|
33 |
large size. Worse still, since model checking is fully automatic, it give little
|
|
|
34 |
insight on why the formal model is correct. It is therefore
|
|
|
35 |
definitely desirable to analyze PI using theorem proving, which gives
|
|
|
36 |
more general results as well as deeper insight. And this is the purpose
|
|
|
37 |
of this paper which gives a formal analysis of PI in the interactive
|
|
|
38 |
theorem prover Isabelle using Higher Order Logic (HOL). The formalization
|
|
|
39 |
focuses on on two issues:
|
|
|
40 |
|
|
|
41 |
\begin{enumerate}
|
|
|
42 |
\item The correctness of the protocol model itself. A series of desirable properties is
|
|
|
43 |
derived until we are fully convinced that the formal model of PI does
|
|
|
44 |
eliminate priority inversion. And a better understanding of PI is so obtained
|
|
|
45 |
in due course. For example, we find through formalization that the choice of
|
|
|
46 |
next thread to take hold when a
|
|
|
47 |
resource is released is irrelevant for the very basic property of PI to hold.
|
|
|
48 |
A point never mentioned in literature.
|
|
|
49 |
\item The correctness of the implementation. A series of properties is derived the meaning
|
|
|
50 |
of which can be used as guidelines on how PI can be implemented efficiently and correctly.
|
|
|
51 |
\end{enumerate}
|
|
|
52 |
|
|
|
53 |
The rest of the paper is organized as follows: Section \ref{overview} gives an overview
|
|
|
54 |
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
|
|
|
56 |
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
|
|
|
58 |
related works. Section \ref{conclusion} concludes the whole paper.
|
|
|
59 |
*}
|
|
|
60 |
|
|
|
61 |
section {* An overview of priority inversion and priority inheritance \label{overview} *}
|
|
|
62 |
|
|
|
63 |
text {*
|
|
|
64 |
|
|
|
65 |
Priority inversion refers to the phenomenon when a thread with high priority is blocked
|
|
|
66 |
by a thread with low priority. Priority happens when the high priority thread requests
|
|
|
67 |
for some critical resource already taken by the low priority thread. Since the high
|
|
|
68 |
priority thread has to wait for the low priority thread to complete, it is said to be
|
|
|
69 |
blocked by the low priority thread. Priority inversion might prevent high priority
|
|
|
70 |
thread from fulfill its task in time if the duration of priority inversion is indefinite
|
|
|
71 |
and unpredictable. Indefinite priority inversion happens when indefinite number
|
|
|
72 |
of threads with medium priorities is activated during the period when the high
|
|
|
73 |
priority thread is blocked by the low priority thread. Although these medium
|
|
|
74 |
priority threads can not preempt the high priority thread directly, they are able
|
|
|
75 |
to preempt the low priority threads and cause it to stay in critical section for
|
|
|
76 |
an indefinite long duration. In this way, the high priority thread may be blocked indefinitely.
|
|
|
77 |
|
|
|
78 |
Priority inheritance is one protocol proposed to avoid indefinite priority inversion.
|
|
|
79 |
The basic idea is to let the high priority thread donate its priority to the low priority
|
|
|
80 |
thread holding the critical resource, so that it will not be preempted by medium priority
|
|
|
81 |
threads. The thread with highest priority will not be blocked unless it is requesting
|
|
|
82 |
some critical resource already taken by other threads. Viewed from a different angle,
|
|
|
83 |
any thread which is able to block the highest priority threads must already hold some
|
|
|
84 |
critical resource. Further more, it must have hold some critical resource at the
|
|
|
85 |
moment the highest priority is created, otherwise, it may never get change to run and
|
|
|
86 |
get hold. Since the number of such resource holding lower priority threads is finite,
|
|
|
87 |
if every one of them finishes with its own critical section in a definite duration,
|
|
|
88 |
the duration the highest priority thread is blocked is definite as well. The key to
|
|
|
89 |
guarantee lower priority threads to finish in definite is to donate them the highest
|
|
|
90 |
priority. In such cases, the lower priority threads is said to have inherited the
|
|
|
91 |
highest priority. And this explains the name of the protocol:
|
|
|
92 |
{\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.
|
|
|
93 |
|
|
|
94 |
The objectives of this paper are:
|
|
|
95 |
\begin{enumerate}
|
|
|
96 |
\item Build the above mentioned idea into formal model and prove a series of properties
|
|
|
97 |
until we are convinced that the formal model does fulfill the original idea.
|
|
|
98 |
\item Show how formally derived properties can be used as guidelines for correct
|
|
|
99 |
and efficient implementation.
|
|
|
100 |
\end{enumerate}
|
|
|
101 |
The proof is totally formal in the sense that every detail is reduced to the
|
|
|
102 |
very first principles of Higher Order Logic. The nature of interactive theorem
|
|
|
103 |
proving is for the human user to persuade computer program to accept its arguments.
|
|
|
104 |
A clear and simple understanding of the problem at hand is both a prerequisite and a
|
|
|
105 |
byproduct of such an effort, because everything has finally be reduced to the very
|
|
|
106 |
first principle to be checked mechanically. The former intuitive explanation of
|
|
|
107 |
Priority Inheritance is just such a byproduct.
|
|
|
108 |
*}
|
|
|
109 |
|
|
|
110 |
section {* Formal model of Priority Inheritance \label{model} *}
|
|
|
111 |
text {*
|
|
|
112 |
\input{../../generated/PrioGDef}
|
|
|
113 |
*}
|
|
|
114 |
|
|
|
115 |
section {* General properties of Priority Inheritance \label{general} *}
|
|
264
|
116 |
(*<*)
|
|
|
117 |
ML {*
|
|
|
118 |
val () = show_question_marks_default := false;
|
|
|
119 |
*}
|
|
|
120 |
(*>*)
|
|
|
121 |
|
|
|
122 |
text {*
|
|
|
123 |
The following are several very basic prioprites:
|
|
|
124 |
\begin{enumerate}
|
|
|
125 |
\item All runing threads must be ready (@{text "runing_ready"}):
|
|
|
126 |
@{thm[display] "runing_ready"}
|
|
|
127 |
\item All ready threads must be living (@{text "readys_threads"}):
|
|
|
128 |
@{thm[display] "readys_threads"}
|
|
|
129 |
\item There are finite many living threads at any moment (@{text "finite_threads"}):
|
|
|
130 |
@{thm[display] "finite_threads"}
|
|
|
131 |
\item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}):
|
|
|
132 |
@{thm[display] "wq_distinct"}
|
|
|
133 |
\item All threads in waiting queues are living threads (@{text "wq_threads"}):
|
|
|
134 |
@{thm[display] "wq_threads"}
|
|
|
135 |
\item The event which can get a thread into waiting queue must be @{term "P"}-events
|
|
|
136 |
(@{text "block_pre"}):
|
|
|
137 |
@{thm[display] "block_pre"}
|
|
|
138 |
\item A thread may never wait for two different critical resources
|
|
|
139 |
(@{text "waiting_unique"}):
|
|
|
140 |
@{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
|
|
|
141 |
\item Every resource can only be held by one thread
|
|
|
142 |
(@{text "held_unique"}):
|
|
|
143 |
@{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
|
|
|
144 |
\item Every living thread has an unique precedence
|
|
|
145 |
(@{text "preced_unique"}):
|
|
|
146 |
@{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
|
|
|
147 |
\end{enumerate}
|
|
|
148 |
*}
|
|
|
149 |
|
|
|
150 |
text {* \noindent
|
|
|
151 |
The following lemmas show how RAG is changed with the execution of events:
|
|
|
152 |
\begin{enumerate}
|
|
|
153 |
\item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
|
|
|
154 |
@{thm[display] depend_set_unchanged}
|
|
|
155 |
\item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
|
|
|
156 |
@{thm[display] depend_create_unchanged}
|
|
|
157 |
\item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
|
|
|
158 |
@{thm[display] depend_exit_unchanged}
|
|
|
159 |
\item Execution of @{term "P"} (@{text "step_depend_p"}):
|
|
|
160 |
@{thm[display] step_depend_p}
|
|
|
161 |
\item Execution of @{term "V"} (@{text "step_depend_v"}):
|
|
|
162 |
@{thm[display] step_depend_v}
|
|
|
163 |
\end{enumerate}
|
|
|
164 |
*}
|
|
|
165 |
|
|
|
166 |
text {* \noindent
|
|
|
167 |
These properties are used to derive the following important results about RAG:
|
|
|
168 |
\begin{enumerate}
|
|
|
169 |
\item RAG is loop free (@{text "acyclic_depend"}):
|
|
|
170 |
@{thm [display] acyclic_depend}
|
|
|
171 |
\item RAGs are finite (@{text "finite_depend"}):
|
|
|
172 |
@{thm [display] finite_depend}
|
|
|
173 |
\item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
|
|
|
174 |
@{thm [display] wf_dep_converse}
|
|
|
175 |
\item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
|
|
|
176 |
@{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
|
|
|
177 |
\item All threads in RAG are living threads
|
|
|
178 |
(@{text "dm_depend_threads"} and @{text "range_in"}):
|
|
|
179 |
@{thm [display] dm_depend_threads range_in}
|
|
|
180 |
\end{enumerate}
|
|
|
181 |
*}
|
|
|
182 |
|
|
|
183 |
text {* \noindent
|
|
|
184 |
The following lemmas show how every node in RAG can be chased to ready threads:
|
|
|
185 |
\begin{enumerate}
|
|
|
186 |
\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
|
|
|
187 |
@{thm [display] chain_building[rule_format]}
|
|
|
188 |
\item The ready thread chased to is unique (@{text "dchain_unique"}):
|
|
|
189 |
@{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
|
|
|
190 |
\end{enumerate}
|
|
|
191 |
*}
|
|
|
192 |
|
|
|
193 |
text {* \noindent
|
|
|
194 |
Properties about @{term "next_th"}:
|
|
|
195 |
\begin{enumerate}
|
|
|
196 |
\item The thread taking over is different from the thread which is releasing
|
|
|
197 |
(@{text "next_th_neq"}):
|
|
|
198 |
@{thm [display] next_th_neq}
|
|
|
199 |
\item The thread taking over is unique
|
|
|
200 |
(@{text "next_th_unique"}):
|
|
|
201 |
@{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}
|
|
|
202 |
\end{enumerate}
|
|
|
203 |
*}
|
|
|
204 |
|
|
|
205 |
text {* \noindent
|
|
|
206 |
Some deeper results about the system:
|
|
|
207 |
\begin{enumerate}
|
|
|
208 |
\item There can only be one running thread (@{text "runing_unique"}):
|
|
|
209 |
@{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
|
|
|
210 |
\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
|
|
|
211 |
@{thm [display] max_cp_eq}
|
|
|
212 |
\item There must be one ready thread having the max @{term "cp"}-value
|
|
|
213 |
(@{text "max_cp_readys_threads"}):
|
|
|
214 |
@{thm [display] max_cp_readys_threads}
|
|
|
215 |
\end{enumerate}
|
|
|
216 |
*}
|
|
|
217 |
|
|
|
218 |
text {* \noindent
|
|
|
219 |
The relationship between the count of @{text "P"} and @{text "V"} and the number of
|
|
|
220 |
critical resources held by a thread is given as follows:
|
|
|
221 |
\begin{enumerate}
|
|
|
222 |
\item The @{term "V"}-operation decreases the number of critical resources
|
|
|
223 |
one thread holds (@{text "cntCS_v_dec"})
|
|
|
224 |
@{thm [display] cntCS_v_dec}
|
|
|
225 |
\item The number of @{text "V"} never exceeds the number of @{text "P"}
|
|
|
226 |
(@{text "cnp_cnv_cncs"}):
|
|
|
227 |
@{thm [display] cnp_cnv_cncs}
|
|
|
228 |
\item The number of @{text "V"} equals the number of @{text "P"} when
|
|
|
229 |
the relevant thread is not living:
|
|
|
230 |
(@{text "cnp_cnv_eq"}):
|
|
|
231 |
@{thm [display] cnp_cnv_eq}
|
|
|
232 |
\item When a thread is not living, it does not hold any critical resource
|
|
|
233 |
(@{text "not_thread_holdents"}):
|
|
|
234 |
@{thm [display] not_thread_holdents}
|
|
|
235 |
\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant
|
|
|
236 |
thread does not hold any critical resource, therefore no thread can depend on it
|
|
|
237 |
(@{text "count_eq_dependents"}):
|
|
|
238 |
@{thm [display] count_eq_dependents}
|
|
|
239 |
\end{enumerate}
|
|
|
240 |
*}
|
|
262
|
241 |
|
|
|
242 |
section {* Key properties \label{extension} *}
|
|
|
243 |
|
|
264
|
244 |
(*<*)
|
|
|
245 |
context extend_highest_gen
|
|
|
246 |
begin
|
|
|
247 |
(*>*)
|
|
|
248 |
|
|
|
249 |
text {*
|
|
|
250 |
The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this
|
|
|
251 |
purpose, we need to investigate what happens after one thread takes the highest precedence.
|
|
|
252 |
A locale is used to describe such a situation, which assumes:
|
|
|
253 |
\begin{enumerate}
|
|
|
254 |
\item @{term "s"} is a valid state (@{text "vt_s"}):
|
|
|
255 |
@{thm vt_s}.
|
|
|
256 |
\item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
|
|
|
257 |
@{thm threads_s}.
|
|
|
258 |
\item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
|
|
|
259 |
@{thm highest}.
|
|
|
260 |
\item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
|
|
|
261 |
@{thm preced_th}.
|
|
|
262 |
\end{enumerate}
|
|
|
263 |
*}
|
|
|
264 |
|
|
|
265 |
text {* \noindent
|
|
|
266 |
Under these assumptions, some basic priority can be derived for @{term "th"}:
|
|
|
267 |
\begin{enumerate}
|
|
|
268 |
\item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):
|
|
|
269 |
@{thm [display] eq_cp_s_th}
|
|
|
270 |
\item The current precedence of @{term "th"} is the highest precedence in
|
|
|
271 |
the system (@{text "highest_cp_preced"}):
|
|
|
272 |
@{thm [display] highest_cp_preced}
|
|
|
273 |
\item The precedence of @{term "th"} is the highest precedence
|
|
|
274 |
in the system (@{text "highest_preced_thread"}):
|
|
|
275 |
@{thm [display] highest_preced_thread}
|
|
|
276 |
\item The current precedence of @{term "th"} is the highest current precedence
|
|
|
277 |
in the system (@{text "highest'"}):
|
|
|
278 |
@{thm [display] highest'}
|
|
|
279 |
\end{enumerate}
|
|
|
280 |
*}
|
|
|
281 |
|
|
|
282 |
text {* \noindent
|
|
|
283 |
To analysis what happens after state @{term "s"} a sub-locale is defined, which
|
|
|
284 |
assumes:
|
|
|
285 |
\begin{enumerate}
|
|
|
286 |
\item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
|
|
|
287 |
\item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
|
|
|
288 |
its precedence can not be higher than @{term "th"}, therefore
|
|
|
289 |
@{term "th"} remain to be the one with the highest precedence
|
|
|
290 |
(@{text "create_low"}):
|
|
|
291 |
@{thm [display] create_low}
|
|
|
292 |
\item Any adjustment of priority in
|
|
|
293 |
@{term "t"} does not happen to @{term "th"} and
|
|
|
294 |
the priority set is no higher than @{term "prio"}, therefore
|
|
|
295 |
@{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
|
|
|
296 |
@{thm [display] set_diff_low}
|
|
|
297 |
\item Since we are investigating what happens to @{term "th"}, it is assumed
|
|
|
298 |
@{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
|
|
|
299 |
@{thm [display] exit_diff}
|
|
|
300 |
\end{enumerate}
|
|
|
301 |
*}
|
|
|
302 |
|
|
|
303 |
text {* \noindent
|
|
|
304 |
All these assumptions are put into a predicate @{term "extend_highest_gen"}.
|
|
|
305 |
It can be proved that @{term "extend_highest_gen"} holds
|
|
|
306 |
for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
|
|
|
307 |
@{thm [display] red_moment}
|
|
|
308 |
|
|
|
309 |
From this, an induction principle can be derived for @{text "t"}, so that
|
|
|
310 |
properties already derived for @{term "t"} can be applied to any prefix
|
|
|
311 |
of @{text "t"} in the proof of new properties
|
|
|
312 |
about @{term "t"} (@{text "ind"}):
|
|
|
313 |
\begin{center}
|
|
|
314 |
@{thm[display] ind}
|
|
|
315 |
\end{center}
|
|
|
316 |
|
|
|
317 |
The following properties can be proved about @{term "th"} in @{term "t"}:
|
|
|
318 |
\begin{enumerate}
|
|
|
319 |
\item In @{term "t"}, thread @{term "th"} is kept live and its
|
|
|
320 |
precedence is preserved as well
|
|
|
321 |
(@{text "th_kept"}):
|
|
|
322 |
@{thm [display] th_kept}
|
|
|
323 |
\item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among
|
|
|
324 |
all living threads
|
|
|
325 |
(@{text "max_preced"}):
|
|
|
326 |
@{thm [display] max_preced}
|
|
|
327 |
\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
|
|
|
328 |
among all living threads
|
|
|
329 |
(@{text "th_cp_max_preced"}):
|
|
|
330 |
@{thm [display] th_cp_max_preced}
|
|
|
331 |
\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current
|
|
|
332 |
precedence among all living threads
|
|
|
333 |
(@{text "th_cp_max"}):
|
|
|
334 |
@{thm [display] th_cp_max}
|
|
|
335 |
\item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment
|
|
|
336 |
@{term "s"}
|
|
|
337 |
(@{text "th_cp_preced"}):
|
|
|
338 |
@{thm [display] th_cp_preced}
|
|
|
339 |
\end{enumerate}
|
|
|
340 |
*}
|
|
|
341 |
|
|
|
342 |
text {* \noindent
|
|
|
343 |
The main theorem is to characterizing the running thread during @{term "t"}
|
|
|
344 |
(@{text "runing_inversion_2"}):
|
|
|
345 |
@{thm [display] runing_inversion_2}
|
|
|
346 |
According to this, if a thread is running, it is either @{term "th"} or was
|
|
|
347 |
already live and held some resource
|
|
|
348 |
at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
|
|
|
349 |
|
|
|
350 |
Since there are only finite many threads live and holding some resource at any moment,
|
|
|
351 |
if every such thread can release all its resources in finite duration, then after finite
|
|
|
352 |
duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
|
|
|
353 |
then.
|
|
|
354 |
*}
|
|
|
355 |
|
|
|
356 |
(*<*)
|
|
|
357 |
end
|
|
|
358 |
(*>*)
|
|
|
359 |
|
|
262
|
360 |
section {* Properties to guide implementation \label{implement} *}
|
|
|
361 |
|
|
264
|
362 |
text {*
|
|
|
363 |
The properties (especially @{text "runing_inversion_2"}) convinced us that model defined
|
|
|
364 |
in section \ref{model} does prevent indefinite priority inversion and therefore fulfills
|
|
|
365 |
the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper
|
|
|
366 |
is to show how this model can be used to guide a concrete implementation.
|
|
|
367 |
*}
|
|
|
368 |
|
|
|
369 |
|
|
262
|
370 |
section {* Related works \label{related} *}
|
|
|
371 |
|
|
|
372 |
text {*
|
|
|
373 |
\begin{enumerate}
|
|
|
374 |
\item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}
|
|
|
375 |
\cite{WellingsBSB07} models and verifies the combination of Priority Inheritance (PI) and
|
|
|
376 |
Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine
|
|
|
377 |
using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed
|
|
|
378 |
formal model of combined PI and PCE is given, the number of properties is quite
|
|
|
379 |
small and the focus is put on the harmonious working of PI and PCE. Most key features of PI
|
|
|
380 |
(as well as PCE) are not shown. Because of the limitation of the model checking technique
|
|
|
381 |
used there, properties are shown only for a small number of scenarios. Therefore,
|
|
|
382 |
the verification does not show the correctness of the formal model itself in a
|
|
|
383 |
convincing way.
|
|
|
384 |
\item {\em Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC}
|
|
|
385 |
\cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown
|
|
|
386 |
for PI using model checking. The limitation of model checking is intrinsic to the work.
|
|
|
387 |
\item {\em Synchronous modeling and validation of priority inheritance schedulers}
|
|
|
388 |
\cite{conf/fase/JahierHR09}. Gives a formal model
|
|
|
389 |
of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked
|
|
|
390 |
several properties using model checking. The number of properties shown there is
|
|
|
391 |
less than here and the scale is also limited by the model checking technique.
|
|
|
392 |
\item {\em The Priority Ceiling Protocol: Formalization and Analysis Using PVS}
|
|
|
393 |
\cite{dutertre99b}. Formalized another protocol for Priority Inversion in the
|
|
|
394 |
interactive theorem proving system PVS.
|
|
|
395 |
\end{enumerate}
|
|
|
396 |
|
|
|
397 |
|
|
|
398 |
There are several works on inversion avoidance:
|
|
|
399 |
\begin{enumerate}
|
|
|
400 |
\item {\em Solving the group priority inversion problem in a timed asynchronous system}
|
|
|
401 |
\cite{Wang:2002:SGP}. The notion of Group Priority Inversion is introduced. The main
|
|
|
402 |
strategy is still inversion avoidance. The method is by reordering requests
|
|
|
403 |
in the setting of Client-Server.
|
|
|
404 |
\item {\em A Formalization of Priority Inversion} \cite{journals/rts/BabaogluMS93}.
|
|
|
405 |
Formalized the notion of Priority
|
|
|
406 |
Inversion and proposes methods to avoid it.
|
|
|
407 |
\end{enumerate}
|
|
|
408 |
|
|
|
409 |
{\em Examples of inaccurate specification of the protocol ???}.
|
|
|
410 |
|
|
|
411 |
*}
|
|
|
412 |
|
|
|
413 |
section {* Conclusions \label{conclusion} *}
|
|
|
414 |
|
|
|
415 |
(*<*)
|
|
|
416 |
end
|
|
|
417 |
(*>*) |