diff -r 800b0e3b4204 -r 83fb18cadd2b prio/Paper/document/root.tex
--- a/prio/Paper/document/root.tex	Sun Jan 29 09:31:03 2012 +0000
+++ b/prio/Paper/document/root.tex	Mon Jan 30 06:46:47 2012 +0000
@@ -45,23 +45,23 @@
 \maketitle
 
 \begin{abstract}
-In realtime systems with support for resource locking and
-processes involving priorities, one faces the problem of
-priority inversion. This problem can make the behaviour of processes unpredictable
-and the resulting bugs can be hard to find.  The Priority Inheritance
-Protocol is one solution implemented in many systems for
-solving the priority inversion problem, but the correctness of this solution has never
-been formally verified in a theorem prover. The original description
-of the Property Inheritance Protocol presents a ``correctness proof''
-done with pencil-and-paper for an \emph{incorrect} algorithm. This has
-already been pointed out in the literature. In this paper we fix the
-problem of the original proof by making all notions precise and implement a
-variant of a solution proposed earlier. Our formalisation in
-Isabelle/HOL uncovered facts not mentioned in the literature, but also
-shows how to efficiently implement this protocol. Earlier correct
-implementations were criticised as too inefficient. Our formalisation  
-is based on Paulson's inductive approach to verifying 
-protocols.\medskip
+In realtime systems with support for resource locking and processes
+involving priorities, one faces the problem of priority
+inversion. This problem can make the behaviour of processes
+unpredictable and the resulting bugs can be hard to find.  The
+Priority Inheritance Protocol is one solution implemented in many
+systems for solving this problem, but the correctness of this solution
+has never been formally verified in a theorem prover. As already
+pointed out in the literature, the original description of the
+Property Inheritance Protocol presents an informal correctness
+``proof'' for an \emph{incorrect} algorithm. In this paper we fix the
+problem of the original proof by making all notions precise and
+implementing a variant of a solution proposed earlier. Our
+formalisation in Isabelle/HOL uncovered facts not mentioned in the
+literature, but also shows how to efficiently implement this
+protocol. Earlier correct implementations were criticised as too
+inefficient. Our formalisation is based on Paulson's inductive
+approach to verifying protocols.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
 realtime systems