regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:e6b13c7b9494
+:ee58e3d99f8a
 locking a resource prevented a high priority thread from running in
 time, leading to a system reset. Once the problem was found, it was
 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
 unlocking the resource. This solves the problem of $H$ having to
 wait indefinitely, because $L$ cannot be blocked by threads having
 \noindent
 {\bf Contributions:} There have been earlier formal investigations
 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).
+knowledge the first one).  In contrast to model checking, our
-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
+to prove stronger properties that, as we will show, can help with an
-efficient implementation.  For example, we found by ``playing'' with the formalisation
+efficient implementation of PIP in the educational PINTOS operating
-that the choice of the next thread to take over a lock when a
+system \cite{PINTOS}.  For example, we found by ``playing'' with the
-resource is released is irrelevant for PIP being correct---a fact
+formalisation that the choice of the next thread to take over a lock
-that has not been mentioned in the literature. This is important
+when a resource is released is irrelevant for PIP being correct---a
-for an efficient implementation, because we can give the lock to the
+fact that has not been mentioned in the literature and not been used
-thread with the highest priority so that it terminates more quickly.
+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 *}
 text {*
 \noindent
 As can be seen, a pleasing byproduct of our formalisation is that the properties in
 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
+We confirmed 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 version of PIP on top of PINTOS, a small operating system written in C and used for teaching at
-Our events translate in PINTOS to the following function interface:
+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 Create} & @{text "thread_create"}\\
-@{text Exit}   & \\
+@{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 *}
 text {*
 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
 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
+multi-processor systems.  However, the answer is that
-to \cite{Steinberg10}, is that except for one unsatisfactory
+there is very little work about PIP and multi-processors in the literature.
-proposal nobody has a good idea for how PIP should be modified to
+We are not aware of any proofs in this area, not even informal ones. There
-work correctly on multi-processor systems. The difficulties become
+is an implementation of PIP on multi-processors in Linux as part of the ``real-time'' effort,
-clear when considering the fact that releasing and re-locking a resource always
+with an informal description given in \cite{LINUX}.
-requires a small amount of time. If processes work independently,
+We estimate that the formal verification of this algorithm, involving more
-then a low priority process can ``steal'' in such an unguarded
+fine-grained events, is a magnitude harder than the one we presented here, but
-moment a lock for a resource that was supposed to allow a high-priority
+still within reach of current theorem proving technology. We leave this for future
-process to run next. Thus the problem of Priority Inversion is not
+work.
-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.
 The most closely related work to ours is the formal verification in
 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

changeset 352	ee58e3d99f8a
parent 351	e6b13c7b9494
child 353	32186d6a1951