# HG changeset patch
# User urbanc
# Date 1334677023 0
# Node ID 27270b4bffba9ea923ea052a9773fd684c1fa845
# Parent  1687f868dd5e50592234141850107d13d6f51737
some small improvements

diff -r 1687f868dd5e -r 27270b4bffba prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Apr 16 15:16:02 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Apr 17 15:37:03 2012 +0000
@@ -54,10 +54,9 @@
   \emph{Priority Inversion}. Suppose three threads having priorities
   $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
   $H$ blocks any other thread with lower priority and the thread itself cannot
-  be blocked indefinitely by any thread with lower priority. Alas, in a naive
+  be blocked indefinitely by threads with lower priority. Alas, in a naive
   implementation of resource locking and priorities this property can
-  be violated. Even worse, $H$ can be delayed indefinitely by
-  threads with lower priorities. For this let $L$ be in the
+  be violated. For this let $L$ be in the
   possession of a lock for a resource that $H$ also needs. $H$ must
   therefore wait for $L$ to exit the critical section and release this
   lock. The problem is that $L$ might in turn be blocked by any
@@ -93,7 +92,7 @@
   implemented. This includes VxWorks (a proprietary real-time OS used
   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
   ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
-  example in libraries for FreeBSD, Solaris and Linux. ({\bf ??? Is this True?})
+  example in libraries for FreeBSD, Solaris and Linux. 
 
   One advantage of PIP is that increasing the priority of a thread
   can be dynamically calculated by the scheduler. This is in contrast
@@ -124,7 +123,7 @@
   and also a few high-level descriptions of implementations (e.g.~in
   the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
   with actual implementations. That this is a problem in practice is
-  proved by an email from Baker, who wrote on 13 July 2009 on the Linux
+  proved by an email by Baker, who wrote on 13 July 2009 on the Linux
   Kernel mailing list:
 
   \begin{quote}
@@ -1082,8 +1081,8 @@
   The first property is again telling us we do not need to change the @{text RAG}. 
   The second shows that the @{term cp}-values of all threads other than @{text th} 
   are unchanged. The reason is that @{text th} is running; therefore it is not in 
-  the @{term dependants} relation of any thread. This in turn means that the 
-  change of its priority cannot affect the threads.
+  the @{term dependants} relation of any other thread. This in turn means that the 
+  change of its priority cannot affect other threads.
 
   %The second
   %however states that only threads that are \emph{not} dependants of @{text th} have their
@@ -1205,6 +1204,8 @@
   this section closely inform an implementation of PIP, namely whether the
   @{text RAG} needs to be reconfigured or current precedences need to
   be recalculated for an event. This information is provided by the lemmas we proved.
+  We confirmened that our observations translate into practice by implementing
+  a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}. 
 *}
 
 section {* Conclusion *}
@@ -1237,8 +1238,8 @@
   email from Baker we cited in the Introduction. We achieved also this
   goal: The formalisation gives the first author enough data to enable
   his undergraduate students to implement PIP (as part of their OS course)
-  on top of PINTOS, a small operating system for teaching
-  purposes. A byproduct of our formalisation effort is that nearly all
+  on top of PINTOS, a simple instructional operating system for the x86 
+  architecture \cite{PINTOS}. A byproduct of our formalisation effort is that nearly all
   design choices for the PIP scheduler are backed up with a proved
   lemma. We were also able to establish the property that the choice of
   the next thread which takes over a lock is irrelevant for the correctness
@@ -1275,7 +1276,12 @@
   PVS of the Priority Ceiling Protocol done by Dutertre
   \cite{dutertre99b}---another solution to the Priority Inversion
   problem, which however needs static analysis of programs in order to
-  avoid it. {\bf ??? mention model-checking approaches}
+  avoid it. There have been earlier formal investigations
+  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
+  checking techniques. In this way they are limited to validating
+  one particular implementation. In contrast, our paper is a good 
+  witness for one of the major reasons to be interested in machine checked 
+  reasoning: gaining deeper understanding of the subject matter.
 
   Our formalisation
   consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
@@ -1286,13 +1292,6 @@
   can be downloaded from
   \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
 
-  {\bf ??? say:
-  So this paper is a good witness for one
-of the major reasons to be interested in machine checked reasoning:
-gaining deeper understanding of the subject matter.
-  }
-
-
   \bibliographystyle{plain}
   \bibliography{root}
 *}
diff -r 1687f868dd5e -r 27270b4bffba prio/Paper/document/root.bib
--- a/prio/Paper/document/root.bib	Mon Apr 16 15:16:02 2012 +0000
+++ b/prio/Paper/document/root.bib	Tue Apr 17 15:37:03 2012 +0000
@@ -1,3 +1,9 @@
+
+@Misc{PINTOS,
+  title = {\url{http://www.stanford.edu/class/cs140/projects/}},
+}
+
+
 @inproceedings{Haftmann08,
   author    = {F.~Haftmann and M.~Wenzel},
   title     = {{L}ocal {T}heory {S}pecifications in {I}sabelle/{I}sar},
diff -r 1687f868dd5e -r 27270b4bffba prio/paper.pdf
Binary file prio/paper.pdf has changed