# HG changeset patch
# User urbanc
# Date 1327706350 0
# Node ID 993068ce745f67be3c83c82c0ff6f3d994ddac21
# Parent  24199eb2c4230d0622f4d9cbc5641c17c48890ea
changed abstract, intro and IsaMakefile

diff -r 24199eb2c423 -r 993068ce745f prio/IsaMakefile
--- a/prio/IsaMakefile	Fri Jan 27 13:50:02 2012 +0000
+++ b/prio/IsaMakefile	Fri Jan 27 23:19:10 2012 +0000
@@ -1,7 +1,7 @@
 
 ## targets
 
-default: paper
+default: itp
 all: session paper
 
 ## global settings
@@ -18,9 +18,8 @@
 
 session: ./ROOT.ML ./*.thy
 	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
-	
-paper: Paper/ROOT.ML \
-       Paper/*.thy 
+
+itp: Paper/*.thy Paper/*.ML 
 	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
 	rm -f Paper/generated/*.aux # otherwise latex will fall over  
 	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
diff -r 24199eb2c423 -r 993068ce745f prio/Paper/Paper.thy
--- 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;*)
 *}
 (*>*)
 
diff -r 24199eb2c423 -r 993068ce745f prio/Paper/document/root.tex
--- a/prio/Paper/document/root.tex	Fri Jan 27 13:50:02 2012 +0000
+++ b/prio/Paper/document/root.tex	Fri Jan 27 23:19:10 2012 +0000
@@ -41,28 +41,34 @@
        for Correct and Efficient Implementation}
 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
 \institute{PLA University of Science and Technology, China \and 
-           King's College London, U.K.}
+           King's College London, United Kingdom}
 \maketitle
 
-%\mbox{}\\[-10mm]
 \begin{abstract}
-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. 
+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
+
+{\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
+realtime systems
 \end{abstract}
 
-
 \input{session}
 
-%%\mbox{}\\[-10mm]
 \bibliographystyle{plain}
 \bibliography{root}
 
diff -r 24199eb2c423 -r 993068ce745f prio/paper.pdf
Binary file prio/paper.pdf has changed