--- a/Journal/document/root.tex	Thu Jan 14 00:55:54 2016 +0800
+++ b/Journal/document/root.tex	Thu Jan 14 03:29:22 2016 +0000
@@ -53,7 +53,9 @@
 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
 Compared with that paper we give an actual implementation of our formalised scheduling 
 algorithm in C and the operating system PINTOS. Our implementation follows closely all results
-we proved about optimisations of the Priority Inheritance Protocol.}
+we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper
+more details about the proof and also surveying 
+the existing literature in more depth.}
 \renewcommand{\thefootnote}{\arabic{footnote}}
 
 \title{Priority Inheritance Protocol Proved Correct}
@@ -63,28 +65,28 @@
 \maketitle
 
 \begin{abstract}
-In real-time systems with threads, resource locking and 
-priority sched\-uling, one faces the problem of Priority
-Inversion. This problem can make the behaviour of threads
-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 informal investigation of
-the Property Inheritance Protocol presents a correctness ``proof'' for
-an \emph{incorrect} algorithm. In this paper we fix the problem of
-this proof by making all notions precise and implementing a variant of
-a solution proposed earlier. We also generalise the original informal proof to the
-practically relevant case where critical sections can
-overlap. Our formalisation in Isabelle/HOL not just
-uncovers facts not mentioned in the literature, but also helps with
-implementing efficiently this protocol. Earlier correct implementations
-were criticised as too inefficient. Our formalisation is based on
-Paulson's inductive approach to verifying protocols; our implementation
-builds on top of the small PINTOS operating system used for teaching.\medskip
+In real-time systems with threads, resource locking and priority
+sched\-uling, one faces the problem of Priority Inversion. This
+problem can make the behaviour of threads 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 informal investigation of the Property Inheritance Protocol
+presents a correctness ``proof'' for an \emph{incorrect} algorithm. In
+this paper we fix the problem of this proof by making all notions
+precise and implementing a variant of a solution proposed earlier. We
+also generalise the scheduling problem to the practically relevant case where
+critical sections can overlap. Our formalisation in Isabelle/HOL not
+just uncovers facts not mentioned in the literature, but also helps
+with implementing efficiently this protocol. Earlier correct
+implementations were criticised as too inefficient. Our formalisation
+is based on Paulson's inductive approach to verifying protocols; our
+implementation builds on top of the small PINTOS operating system used
+for teaching.\medskip
 
-%{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
-%real-time systems, Isabelle/HOL
+{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
+real-time systems, Isabelle/HOL
 \end{abstract}
 
 \input{session}