--- a/prio/Paper/Paper.thy Fri Jan 27 13:50:02 2012 +0000
+++ b/prio/Paper/Paper.thy Fri Jan 27 23:19:10 2012 +0000
@@ -7,6 +7,30 @@
section {* Introduction *}
text {*
+ Many realtime systems need to support processes with priorities and
+ locking of resources. Locking of resources ensures... Priorities
+ are needed so that some processes can finish their work within ``hard''
+ deadlines. Unfortunately both features interact in subtle ways
+ leading to the problem, called Priority Inversion. Suppose three
+ processes with priorities $H$(igh), $M$(edium) and $L$(ow). We would
+ assume that process $H$ cannot be blocked by any process with lower
+ priority. Unfortunately in a naive implementation, this can happen
+ and $H$ even can be delayed indefinitely by processes with lower
+ priorities. For this let $L$ be in the posession of lock for a
+ research which also $H$ needs. $H$ must therefore wait for $L$ to
+ release this lock. Unfortunately, $L$ can in turn be blocked by any
+ process with priority $M$, and so $H$ sits there potentially waiting
+ indefinitely.
+
+ If this problem of inversion of priorities is left untreated,
+ systems can become unpredictable and have dire consequences. The
+ classic example where this happened in practice is the software on
+ the Mars pathfinder project. This software shut down at irregulare
+ intervals leading to loss of project time (the mission and data was
+ fortunately not lost, because of clever system design). The problem
+ was that a high priority process and could only be restarted the
+ next day.
+
Priority inversion referrers to the phenomena where tasks with higher
priority are blocked by ones with lower priority. If priority inversion
@@ -56,6 +80,22 @@
how priority inversion is controlled by PI. Section \ref{implement} gives properties
which can be used for guidelines of implementation. Section \ref{related} discusses
related works. Section \ref{conclusion} concludes the whole paper.
+
+
+ Contributions
+
+ Despite the wide use of Priority Inheritance Protocol in real time operating
+ system, it's correctness has never been formally proved and mechanically checked.
+ All existing verification are based on model checking technology. Full automatic
+ verification gives little help to understand why the protocol is correct.
+ And results such obtained only apply to models of limited size.
+ This paper presents a formal verification based on theorem proving.
+ Machine checked formal proof does help to get deeper understanding. We found
+ the fact which is not mentioned in the literature, that the choice of next
+ thread to take over when an critical resource is release does not affect the correctness
+ of the protocol. The paper also shows how formal proof can help to construct
+ correct and efficient implementation.\bigskip
+
*}
section {* An overview of priority inversion and priority inheritance \label{overview} *}
@@ -115,7 +155,7 @@
section {* General properties of Priority Inheritance \label{general} *}
(*<*)
ML {*
- val () = show_question_marks_default := false;
+ (*val () = show_question_marks_default := false;*)
*}
(*>*)