--- 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