--- 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;*)
 *}
 (*>*)