# HG changeset patch # User Christian Urban # Date 1393863768 0 # Node ID 9f0b78fcc89411fb096d3a178bca77522c080f59 # Parent 55d1591b17f06d2075d173bdbaae8ad4d2d1c073 updated diff -r 55d1591b17f0 -r 9f0b78fcc894 Journal/Paper.thy --- a/Journal/Paper.thy Fri Feb 28 12:49:58 2014 +0000 +++ b/Journal/Paper.thy Mon Mar 03 16:22:48 2014 +0000 @@ -54,7 +54,7 @@ priorities, the problem is called Priority Inversion. It was first described in \cite{Lampson80} in the context of the Mesa programming language designed for concurrent programming. - + If the problem of Priority Inversion is ignored, real-time systems can become unpredictable and resulting bugs can be hard to diagnose. The classic example where this happened is the software that @@ -81,17 +81,19 @@ 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 + ASIMO robot, etc.) and ThreadX (another proprietary real-time OS + used in HP inkjet printers \cite{ThreadX}), but also + the POSIX 1003.1c Standard realised for example in libraries for FreeBSD, Solaris and Linux. - Two advantages of PIP are that increasing the priority of a thread - can be performed dynamically by the scheduler and is deterministic. + Two advantages of PIP are that it is deterministic and that increasing the priority of a thread + can be performed dynamically by the scheduler. This is in contrast to \emph{Priority Ceiling} \cite{Sha90}, another solution to the Priority Inversion problem, which requires static analysis of the program in order to prevent - Priority Inversion, and also to the Windows NT scheduler, which avoids - this problem by randomly boosting the priority of ready (low priority) threads - (e.g.~\cite{WINDOWSNT}). + Priority Inversion, and also in contrast to the Windows NT scheduler, which avoids + this problem by randomly boosting the priority of ready low-priority threads + (see for instance~\cite{WINDOWSNT}). However, there has also been strong criticism against PIP. For instance, PIP cannot prevent deadlocks when lock dependencies are circular, and also blocking times can be @@ -147,14 +149,17 @@ so that $H$, say, can proceed, then we still have Priority Inversion with $H'$ (which waits for the other resource). The correct behaviour for $L$ is to switch to the highest remaining priority of - the threads that it blocks. The advantage of formalising the + the threads that it blocks. While + \cite{Sha90} is the only formal publication we have + found that describes the incorrect behaviour, not all, but many + informal\footnote{informal as in ``found on the Web''} + descriptions of PIP overlook the possibility that another + high-priority might wait for a low-priority process to finish. + The advantage of formalising the correctness of a high-level specification of PIP in a theorem prover is that such issues clearly show up and cannot be overlooked as in informal reasoning (since we have to analyse all possible behaviours - of threads, i.e.~\emph{traces}, that could possibly happen).\footnote{While - \cite{Sha90} is the only formal publication we have - found that describes the incorrect behaviour, not all, but many - informal descriptions of PIP overlook the case...}\medskip + of threads, i.e.~\emph{traces}, that could possibly happen).\medskip\smallskip \noindent {\bf Contributions:} There have been earlier formal investigations @@ -326,10 +331,8 @@ @{thm cs_depend_def} \end{isabelle} - \noindent - If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows: - \begin{figure}[ph] + \begin{figure}[t] \begin{center} \newcommand{\fnt}{\fontsize{7}{8}\selectfont} \begin{tikzpicture}[scale=1] @@ -368,6 +371,9 @@ \end{figure} \noindent + If there is no cycle, then every RAG can be pictured as a forrest of trees, as + for example in Figure~\ref{RAGgraph}. + We will design our scheduler so that every thread can be in the possession of several resources, that is it has potentially several incoming holding edges in the RAG, but has at most one outgoing @@ -1008,7 +1014,6 @@ text {* While our formalised proof gives us confidence about the correctness of our model of PIP, we found that the formalisation can even help us with efficiently implementing it. - For example Baker complained that calculating the current precedence in PIP is quite ``heavy weight'' in Linux (see the Introduction). In our model of PIP the current precedence of a thread in a state @{text s} @@ -1250,12 +1255,7 @@ This lemma states that if an intermediate @{term cp}-value does not change, then the procedure can also stop, because none of its dependent threads will have their current precedence changed. - *} -(*<*) -end -(*>*) -text {* - \noindent + *}(*<*)end(*>*)text {* 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 RAG needs to be reconfigured or current precedences need to @@ -1288,7 +1288,7 @@ them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations for accessing and updating. In the code we shall describe below, we use the function @{ML_text "queue_insert"}, for inserting a new element into a priority queue, and - @{ML_text "queue_update"}, for updating the position of an element that is already + the function @{ML_text "queue_update"}, for updating the position of an element that is already in a queue. Both functions take an extra argument that specifies the comparison function used for organising the priority queue. @@ -1314,7 +1314,7 @@ - \begin{figure}[t] + \begin{figure}[tph] \begin{lstlisting} void lock_acquire (struct lock *lock) { ASSERT (lock != NULL); @@ -1459,6 +1459,12 @@ within reach of current theorem proving technology. We leave this for future work. + To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult + if done informally by ``pencil-and-paper''. This is proved by the flawed proof + in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who + pointed out an error in a paper about Preemption + Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was + invaluable to us in order to feel confident about the correctness of our results. 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 @@ -1478,9 +1484,9 @@ 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}. + The code of our formalisation + can be downloaded from the Mercurial repository at + \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. %\medskip diff -r 55d1591b17f0 -r 9f0b78fcc894 Journal/document/root.bib --- a/Journal/document/root.bib Fri Feb 28 12:49:58 2014 +0000 +++ b/Journal/document/root.bib Mon Mar 03 16:22:48 2014 +0000 @@ -1,3 +1,21 @@ +@inproceedings{ThreadX, + author = {Y.~Wang and M.~Saksena}, + title = {{S}cheduling {F}ixed-{P}riority {T}asks with {P}reemption {T}hreshold}, + booktitle = {Proc.~of the 6th Workshop on Real-Time Computing Systems and Applications (RTCSA)}, + year = {1999}, + pages = {328--337} +} + +@inproceedings{Regehr, + author = {J.~Regehr}, + title = {{S}cheduling {T}asks with {M}ixed {P}reemption {R}elations for {R}obustness + to {T}iming {F}aults}, + booktitle = {Proc.~of the 23rd IEEE Real-Time Systems Symposium (RTSS)}, + year = {2002}, + pages = {315--326} +} + + @INPROCEEDINGS{WINDOWSNT, author={L.~Budin and L.~Jelenkovic}, booktitle={Proc.~of the IEEE International Symposium on diff -r 55d1591b17f0 -r 9f0b78fcc894 journal.pdf Binary file journal.pdf has changed