--- 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

Binary file prio/paper.pdf has changed