
diff -r e6b13c7b9494 -r ee58e3d99f8a prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Apr 30 15:32:34 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed May 02 13:13:47 2012 +0000
@@ -82,7 +82,7 @@
   rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
   \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
   Inheritance Protocol} \cite{Sha90} and others sometimes also call it
-  \emph{Priority Boosting}.} in the scheduling software.
+  \emph{Priority Boosting} or \emph{Priority Donation}.} in the scheduling software.
 
   The idea behind PIP is to let the thread $L$ temporarily inherit
   the high priority from $H$ until $L$ leaves the critical section
@@ -167,16 +167,18 @@
   into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
   checking techniques. This paper presents a formalised and
   mechanically checked proof for the correctness of PIP (to our
-  knowledge the first one). 
-  In contrast to model checking, our
+  knowledge the first one).  In contrast to model checking, our
   formalisation provides insight into why PIP is correct and allows us
-  to prove stronger properties that, as we will show, can inform an
-  efficient implementation.  For example, we found by ``playing'' with the formalisation
-  that the choice of the next thread to take over a lock when a
-  resource is released is irrelevant for PIP being correct---a fact
-  that has not been mentioned in the literature. This is important
-  for an efficient implementation, because we can give the lock to the
-  thread with the highest priority so that it terminates more quickly.
+  to prove stronger properties that, as we will show, can help with an
+  efficient implementation of PIP in the educational PINTOS operating
+  system \cite{PINTOS}.  For example, we found by ``playing'' with the
+  formalisation that the choice of the next thread to take over a lock
+  when a resource is released is irrelevant for PIP being correct---a
+  fact that has not been mentioned in the literature and not been used
+  in the reference implementation of PIP in PINTOS.  This is important
+  for an efficient implementation of PIP, because we can give the lock
+  to the thread with the highest priority so that it terminates more
+  quickly.
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}
@@ -1212,20 +1214,34 @@
   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}. 
-  Our events translate in PINTOS to the following function interface:
+  We confirmed that our observations translate into practice by implementing
+  our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 
+  Stanford University \cite{PINTOS}. To implement PIP, we only need to modify the kernel 
+  functions corresponding to the events in our formal model. The events translate to the following 
+  function interface in PINTOS:
 
   \begin{center}
-  \begin{tabular}{|l|l|}
+  \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
   \hline
   {\bf Event} & {\bf PINTOS function} \\
   \hline
-  @{text Create} & \\
-  @{text Exit}   & \\
+  @{text Create} & @{text "thread_create"}\\
+  @{text Exit}   & @{text "thread_exit"}\\
+  @{text Set}    & @{text "thread_set_priority"}\\
+  @{text P}      & @{text "lock_acquire"}\\
+  @{text V}      & @{text "lock_release"}\\ 
+  \hline
   \end{tabular}
   \end{center}
 
+  \noindent
+  Our assumption that every event is an atomic operation is ensured by the architecture of 
+  PINTOS. The case where an unlocked resource is given next to the waiting thread with the
+  highest precedence is realised in our implementation by priority queues. We implemented
+  them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
+  for accessing and restructuring. Apart from having to implement complex datastructures in C
+  using pointers, our experience with the implementation has been very positive: our specification 
+  and formalisation of PIP translates smoothly to an efficent implementation. 
 *}
 
 section {* Conclusion *}
@@ -1265,29 +1281,19 @@
   the next thread which takes over a lock is irrelevant for the correctness
   of PIP. 
 
-  {\bf ??? rewrite the following slightly}
-
   PIP is a scheduling algorithm for single-processor systems. We are
   now living in a multi-processor world. So the question naturally
   arises whether PIP has any relevance in such a world beyond
   teaching. Priority Inversion certainly occurs also in
-  multi-processor systems.  However, the surprising answer, according
-  to \cite{Steinberg10}, is that except for one unsatisfactory
-  proposal nobody has a good idea for how PIP should be modified to
-  work correctly on multi-processor systems. The difficulties become
-  clear when considering the fact that releasing and re-locking a resource always
-  requires a small amount of time. If processes work independently,
-  then a low priority process can ``steal'' in such an unguarded
-  moment a lock for a resource that was supposed to allow a high-priority
-  process to run next. Thus the problem of Priority Inversion is not
-  really prevented by the classic PIP. It seems difficult to design a PIP-algorithm with
-  a meaningful correctness property on a multi-processor systems where
-  processes work independently.  We can imagine PIP to be of use in
-  situations where processes are \emph{not} independent, but
-  coordinated via a master process that distributes work over some
-  slave processes. However, a formal investigation of this idea is beyond
-  the scope of this paper.  We are not aware of any proofs in this
-  area, not even informal or flawed ones.
+  multi-processor systems.  However, the answer is that
+  there is very little work about PIP and multi-processors in the literature. 
+  We are not aware of any proofs in this area, not even informal ones. There
+  is an implementation of PIP on multi-processors in Linux as part of the ``real-time'' effort,
+  with an informal description given in \cite{LINUX}.
+  We estimate that the formal verification of this algorithm, involving more
+  fine-grained events, is a magnitude harder than the one we presented here, but 
+  still within reach of current theorem proving technology. We leave this for future 
+  work. 
 
   The most closely related work to ours is the formal verification in
   PVS of the Priority Ceiling Protocol done by Dutertre




