regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:1687f868dd5e
+:27270b4bffba
 finish their work within deadlines.  Unfortunately, both features
 can interact in subtle ways leading to a problem, called
 \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
+be violated. For this let $L$ be in the
-threads with lower priorities. 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
 thread with priority $M$, and so $H$ sits there potentially waiting
 indefinitely. Since $H$ is blocked by threads with lower
 priority $M$. While a few other solutions exist for the Priority
 Inversion problem, PIP is one that is widely deployed and
 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
 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
 solution to the Priority Inversion problem, which requires static
 In our opinion, there is clearly a need for investigating correct
 algorithms for PIP. A few specifications for PIP exist (in English)
 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}
 \it{}``I observed in the kernel code (to my disgust), the Linux PIP
 implementation is a nightmare: extremely heavy weight, involving
 \noindent
 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
+the @{term dependants} relation of any other thread. This in turn means that the
-change of its priority cannot affect the threads.
+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
 %current precedence unchanged. For the others we have to recalculate the current
 %precedence. To do this we can start from @{term "th"}
 \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
+a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}.
 *}
 section {* Conclusion *}
 text {*
 programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).
 That this is an issue in practice is illustrated by the
 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
+on top of PINTOS, a simple instructional operating system for the x86
-purposes. A byproduct of our formalisation effort is that nearly all
+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
 of PIP. Earlier model checking approaches which verified particular implementations
 of PIP \cite{Faria08,Jahier09,Wellings07} cannot
 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
-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
 code with a few apply-scripts interspersed. The formal model of PIP
 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
 definitions and proofs span over 770 lines of code. The properties relevant
 for an implementation require 2000 lines. The code of our formalisation
 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}
 *}

changeset 344	27270b4bffba
parent 343	1687f868dd5e
child 345	73a415af3bcd