--- a/prio/Paper/Paper.thy	Sun Jan 29 09:31:03 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Jan 30 06:46:47 2012 +0000
@@ -3,7 +3,7 @@
 imports CpsG ExtGG LaTeXsugar
 begin
 ML {*
-  show_question_marks_default := false;
+  Printer.show_question_marks_default := false;
   *}
 (*>*)
 
@@ -11,30 +11,47 @@
 
 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.
+  locking of resources. Locking of resources ensures mutual exclusion
+  when accessing shared data or devices. Priorities allow schedulling
+  of processes that need to finish their work within hard deadlines.
+  Unfortunately, both features can interact in subtle ways leading to a
+  problem, called \emph{Priority Inversion}. Suppose three processes
+  having priorities $H$(igh), $M$(edium) and $L$(ow). We would expect
+  that the process $H$ blocks any other process with lower priority
+  and itself cannot be blocked by a process with lower priority. Alas,
+  in a naive implementation of resource looking and priorities this
+  property can be violated. Even worse, $H$ can be delayed
+  indefinitely by processes with lower priorities. For this let $L$ be
+  in the possession of a lock for a resource that also $H$ needs. $H$
+  must therefore wait for $L$ to release this lock. The problem is that 
+  $L$ might be in turn blocked by any process with priority $M$, and so
+  $H$ sits there potentially waiting indefinitely. Since $H$ is blocked
+  by processes with lower priorities, the problem
+  is called Priority Inversion.
 
-  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.
- 
+  If the problem of Priority Inversion is ignored, realtime systems
+  can become unpredictable and resulting bugs can be hard to diagnose.
+  The classic example where this happened is the software that
+  controlled the Mars Pathfinder mission in 1997.  Once the spacecraft
+  landed, the software shut down at irregular intervals leading to
+  loss of project time, as normal operation of the craft could only
+  resume the next day (the mission and data already collected was
+  fortunately not lost, because of a clever system design).  The
+  problem was that the schedulling software fell victim of Priority
+  Inversion: a low priority task locking a resource prevented a high
+  priority process from running.  Once found, the problem could be
+  rectified by enabling the Priority Inheritance Protocol in the
+  schedulling software.
 
+  The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
+  temporarily inherit the low priority process the higher priority
+  until it released the locked resource.
+
+  However, there are further subtleties: just lowering the priority 
+  of the process $L$ to its low priority, as proposed in ???, is 
+  incorrect.\bigskip
+  
+  \noindent
   Priority inversion referrers to the phenomena where tasks with higher 
   priority are blocked by ones with lower priority. If priority inversion 
   is not controlled, there will be no guarantee the urgent tasks will be 
@@ -156,11 +173,6 @@
 *}
 
 section {* General properties of Priority Inheritance \label{general} *}
-(*<*)
-ML {*
-  (*val () = show_question_marks_default := false;*)
-*}
-(*>*)
 
 text {*
   The following are several very basic prioprites: