diff -r 83fb18cadd2b -r 1baf8d0c7093 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Jan 30 06:46:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Jan 30 08:45:56 2012 +0000
@@ -14,8 +14,8 @@
   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
+  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,
@@ -23,29 +23,37 @@
   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.
+  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. It was first described in
+  \cite{Lampson:Redell:cacm:1980} in the context of the Mesa
+  programming language designed to support concurrent programming.
 
   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.
+  controlled the Mars Pathfinder mission in 1997
+  \cite{Reeves-Glenn-1998}.  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 reason for the shutdowns was that
+  the schedulling software fell victim of Priority Inversion: a low
+  priority task locking a resource prevented a high priority process
+  from running leading to a system reset. Once the problem was found,
+  it was 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.
+  let the process $L$ temporarily inherit the high priority from $H$ 
+  until $L$ releases the locked resource. This solves the problem of
+  $H$ having to wait indefinitely, because $L$ cannot be blocked by 
+  processes having priority $M$. This solution to the Priority
+  Inversion problem has been known since \cite{Lampson:Redell:cacm:1980}
+  but Lui et al give the first thourough analysis and present a correctness
+  proof for an algorithm \cite{journals/tc/ShaRL90}.
 
   However, there are further subtleties: just lowering the priority 
   of the process $L$ to its low priority, as proposed in ???, is