# HG changeset patch # User urbanc # Date 1329168859 0 # Node ID 0423e4d7c77b430e7f7b3051b1e364677dca7d02 # Parent f05f6aeb32f4e59471c3c6a041d3355d50259e6f more conclusion diff -r f05f6aeb32f4 -r 0423e4d7c77b prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Mon Feb 13 20:57:02 2012 +0000 +++ b/prio/Paper/Paper.thy Mon Feb 13 21:34:19 2012 +0000 @@ -1160,100 +1160,33 @@ design choices for the PIP scheduler are backed up with a proved lemma. We were also able to prove the property that the choice of the next thread taking over a lock is irrelevant for the correctness - of PIP. Earlier model checking techniques - \cite{Faria08,Jahier09,Wellings07} were not able to provided this - kind of ``deep understanding'' into PIP. + of PIP. Earlier model checking approaches to verifying the + correctness of PIP \cite{Faria08,Jahier09,Wellings07} were not able + to provide this kind of ``deep understanding'' about PIP. 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 nowadays any relevance beyond teaching. - - The work in this paper only deals with single CPU configurations. The - "one CPU" assumption is essential for our formalisation, because the - main lemma fails in multi-CPU configuration. The lemma says that any - runing thead must be the one with the highest prioirty or already held - some resource when the highest priority thread was initiated. When - there are multiple CPUs, it may well be the case that a threads did - not hold any resource when the highest priority thread was initiated, - but that thread still runs after that moment on a separate CPU. In - this way, the main lemma does not hold anymore. - - - There are some works deals with priority inversion in multi-CPU - configurations[???], but none of them have given a formal correctness - proof. The extension of our formal proof to deal with multi-CPU - configurations is not obvious. One possibility, as suggested in paper - [???], is change our formal model (the defiintion of "schs") to give - the released resource to the thread with the highest prioirty. In this - way, indefinite prioirty inversion can be avoided, but for a quite - different reason from the one formalized in this paper (because the - "mail lemma" will be different). This means a formal correctness proof - for milt-CPU configuration would be quite different from the one given - in this paper. The solution of prioirty inversion problem in mult-CPU - configurations is a different problem which needs different solutions - which is outside the scope of this paper. - - no clue about multi-processor case according to \cite{Steinberg10} + now living in a multi-processor world. So the question naturally + arises whether PIP has any relevance nowadays beyond + teaching. Priority inversion certainly occurs also in + multi-processor systems. The surprising answer, according to + \cite{Steinberg10}, is that except for one unsatisfactory proposal + nobody seems to have any good idea how PIP shoud be modified to work + correctly on multi-processor systems. The obstacles become clear + when considering that locking and releasing a resource always + requires some small time span. If processes are independent, then a + low priority process can always ``steal'' a the lock for such a + resource from a high-priority process that should have run next. In + effect, we have again the problem of Priority Inversions. It seems + difficult to design an algorithm with a meaningful property from + PIP. We can imagine PIP can be of use in a situation where + processes are not independent, but coordinated such that a master + process distributes the work over some slave processes. However a + formal investigation of this is beyond the scope of this paper. *} -section {* An overview of priority inversion and priority inheritance \label{overview} *} - -text {* - - Priority inversion refers to the phenomenon when a thread with high priority is blocked - by a thread with low priority. Priority happens when the high priority thread requests - for some critical resource already taken by the low priority thread. Since the high - priority thread has to wait for the low priority thread to complete, it is said to be - blocked by the low priority thread. Priority inversion might prevent high priority - thread from fulfill its task in time if the duration of priority inversion is indefinite - and unpredictable. Indefinite priority inversion happens when indefinite number - of threads with medium priorities is activated during the period when the high - priority thread is blocked by the low priority thread. Although these medium - priority threads can not preempt the high priority thread directly, they are able - to preempt the low priority threads and cause it to stay in critical section for - an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. - - Priority inheritance is one protocol proposed to avoid indefinite priority inversion. - The basic idea is to let the high priority thread donate its priority to the low priority - thread holding the critical resource, so that it will not be preempted by medium priority - threads. The thread with highest priority will not be blocked unless it is requesting - some critical resource already taken by other threads. Viewed from a different angle, - any thread which is able to block the highest priority threads must already hold some - critical resource. Further more, it must have hold some critical resource at the - moment the highest priority is created, otherwise, it may never get change to run and - get hold. Since the number of such resource holding lower priority threads is finite, - if every one of them finishes with its own critical section in a definite duration, - the duration the highest priority thread is blocked is definite as well. The key to - guarantee lower priority threads to finish in definite is to donate them the highest - priority. In such cases, the lower priority threads is said to have inherited the - highest priority. And this explains the name of the protocol: - {\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay. - - The objectives of this paper are: - \begin{enumerate} - \item Build the above mentioned idea into formal model and prove a series of properties - until we are convinced that the formal model does fulfill the original idea. - \item Show how formally derived properties can be used as guidelines for correct - and efficient implementation. - \end{enumerate} - The proof is totally formal in the sense that every detail is reduced to the - very first principles of Higher Order Logic. The nature of interactive theorem - proving is for the human user to persuade computer program to accept its arguments. - A clear and simple understanding of the problem at hand is both a prerequisite and a - byproduct of such an effort, because everything has finally be reduced to the very - first principle to be checked mechanically. The former intuitive explanation of - Priority Inheritance is just such a byproduct. - *} - -section {* General properties of Priority Inheritance \label{general} *} - -text {* - - *} - section {* Key properties \label{extension} *} (*<*) @@ -1416,12 +1349,6 @@ *} -section {* Conclusions \label{conclusion} *} - -text {* - - -*} (*<*) end diff -r f05f6aeb32f4 -r 0423e4d7c77b prio/paper.pdf Binary file prio/paper.pdf has changed