# HG changeset patch
# User urbanc
# Date 1328314481 0
# Node ID 7911439863b00babe9c7ab8d8e028d87382ec837
# Parent  3e2c006e7d6c8f4e58017259cdc0051b2086768a
slight polishing

diff -r 3e2c006e7d6c -r 7911439863b0 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Fri Feb 03 11:26:11 2012 +0000
+++ b/prio/Paper/Paper.thy	Sat Feb 04 00:14:41 2012 +0000
@@ -63,7 +63,7 @@
   can be dynamically calculated by the scheduler. This is in contrast
   to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
   solution to the Priority Inversion problem, which requires static
-  analysis of the program in order to be helpful. However, there has
+  analysis of the program in order to prevent Priority Inversion. However, there has
   also been strong criticism against PIP. For instance, PIP cannot
   prevent deadlocks when lock dependencies are circular, and also
   blocking times can be substantial (more than just the duration of a
@@ -81,7 +81,7 @@
   sections to be preempted. While this might have been a reasonable
   solution in 2002, in our modern multiprocessor world, this seems out
   of date. The reason is that this precludes other high-priority 
-  processes from running that do not make any use of the locked
+  processes from running even when they do not make any use of the locked
   resource.
 
   However, there is clearly a need for investigating correct
@@ -115,16 +115,16 @@
   straightforward'' \cite{Sha90}.  Unfortunately, as Yodaiken pointed
   out, this behaviour is too simplistic.  Consider the case where the
   low priority process $L$ locks \emph{two} resources, and two
-  high-priority processes $H$ and $H'$, respectively, wait for one of
-  them.  If $L$ releases only one of them so that $H$, say, can
-  proceed, then we still have Priority Inversion with $H'$: according
-  to Sha et al., $L$ already dropped back to its low priority, but has not yet
-  released the lock $H'$ is waiting for. Therefore the correct behaviour for $L$
+  high-priority processes $H$ and $H'$ each wait for one of
+  them.  If $L$ then releases one resource so that $H$, say, can
+  proceed, then we still have Priority Inversion with $H'$. The correct 
+  behaviour for $L$
   is to revert to the highest remaining priority of processes which it
   blocks. The advantage of a formalisation of PIP in a theorem prover 
-  is that such issues clearly show up and cannot be dodged. 
+  is that such issues clearly show up and cannot be overlooked as in
+  informal reasoning.
 
-  There have been earlier formal investigations into PIP, but ...
+  There have been earlier formal investigations into PIP, but ...\cite{Faria08}
 
   \bigskip
   Priority Inversion problem has been known since 1980
diff -r 3e2c006e7d6c -r 7911439863b0 prio/Paper/document/root.bib
--- a/prio/Paper/document/root.bib	Fri Feb 03 11:26:11 2012 +0000
+++ b/prio/Paper/document/root.bib	Sat Feb 04 00:14:41 2012 +0000
@@ -43,7 +43,12 @@
   year = 	"1980"
 }
 
-
+@MISC{Faria08,
+  author = {J.~M.~S.~Faria},
+  title = {{F}ormal {D}evelopment of {S}olutions for {R}eal-{T}ime {O}perating {S}ystems with {TLA+/TLC}},
+  year = {2008},
+  howpublished={\url{http://repositorio-aberto.up.pt/bitstream/10216/11466/2/Texto%20integral.pdf}},
+}
 
 
 
@@ -56,12 +61,7 @@
 howpublished={\url{http://www.math.unipd.it/~tullio/SCD/2007/Materiale/Locke.pdf}},
 }
 
-@MISC{Faria08,
-author = {J. M. S. Faria},
-title = {Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC},
-year = {2008},
-howpublished={\url{http://repositorio-aberto.up.pt/bitstream/10216/11466/2/Texto%20integral.pdf}},
-}
+
 
 
 
diff -r 3e2c006e7d6c -r 7911439863b0 prio/paper.pdf
Binary file prio/paper.pdf has changed