# HG changeset patch # User urbanc # Date 1335964427 0 # Node ID ee58e3d99f8ae6a9c81be7ca57c377f062531dca # Parent e6b13c7b94946f38f310c2ff9361546652ea6961 added section about PINTOS and rewritten multi-processor section 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 diff -r e6b13c7b9494 -r ee58e3d99f8a prio/Paper/document/root.bib --- a/prio/Paper/document/root.bib Mon Apr 30 15:32:34 2012 +0000 +++ b/prio/Paper/document/root.bib Wed May 02 13:13:47 2012 +0000 @@ -1,6 +1,22 @@ + +@Book{Paulson96, + author = {L.~C.~Paulson}, + title = {{ML} for the {W}orking {P}rogrammer}, + publisher = {Cambridge University Press}, + year = {1996} +} + + +@Manual{LINUX, + author = {S.~Rostedt}, + title = {{R}eal-{T}ime {G}roup {S}cheduling}, + note = {Linux Kernel Distribution at kernel.org, Documentation/scheduler/sched-rt-group.txt} +} @Misc{PINTOS, - title = {\url{http://www.stanford.edu/class/cs140/projects/}}, + author = {B.~Pfaff}, + title = {{PINTOS}}, + note = {\url{http://www.stanford.edu/class/cs140/projects/}}, } diff -r e6b13c7b9494 -r ee58e3d99f8a prio/paper.pdf Binary file prio/paper.pdf has changed