
diff -r 677364c67cc8 -r e9bafb20004d prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Thu May 03 08:52:03 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed May 09 13:41:35 2012 +0000
@@ -114,10 +114,9 @@
   \end{quote}
 
   \noindent
-  He suggests avoiding PIP altogether by not allowing critical
-  sections to be preempted. Unfortunately, this solution does not
-  help in real-time systems with hard deadlines for high-priority 
-  threads.
+  He suggests avoiding PIP altogether by designing the system so that no 
+  priority inversion may happen in the first place. However, such ideal designs may 
+  not always be achievable in practice.
 
   In our opinion, there is clearly a need for investigating correct
   algorithms for PIP. A few specifications for PIP exist (in English)
@@ -175,7 +174,7 @@
   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
+  in the reference implementation of PIP in PINTOS.  This fact, however, 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.
@@ -526,7 +525,7 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm readys_def}\\
-  @{thm runing_def}\\
+  @{thm runing_def}
   \end{tabular}
   \end{isabelle}
 
@@ -538,21 +537,18 @@
   running, namely the one whose current precedence is equal to the maximum of all ready 
   threads. We use sets to capture both possibilities.
   We can now also conveniently define the set of resources that are locked by a thread in a
-  given state
+  given state and also when a thread is detached that state (meaning the thread neither 
+  holds nor waits for a resource):
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm holdents_def}
+  \begin{tabular}{@ {}l}
+  @{thm holdents_def}\\
+  @{thm detached_def}
+  \end{tabular}
   \end{isabelle}
 
   \noindent
-  and also when a thread is detached
-
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{thm detached_def}
-  \end{isabelle}
-
-  \noindent
-  which means that @{text th} neither holds nor waits for a resource in @{text s}.
+  The second definition states that @{text th}  in @{text s}.
   
   Finally we can define what a \emph{valid state} is in our model of PIP. For
   example we cannot expect to be able to exit a thread, if it was not
@@ -680,8 +676,7 @@
   @{text "s' @ s"} are valid states:
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
-  @{term "vt s"}\\
-  @{term "vt (s' @ s)"} 
+  @{term "vt s"}, @{term "vt (s' @ s)"} 
   \end{tabular}
   \end{isabelle}
   \end{quote}
@@ -1019,7 +1014,7 @@
   Of course the main work for implementing PIP involves the
   scheduler and coding how it should react to events.  Below we
   outline how our formalisation guides this implementation for each
-  kind of event.\smallskip
+  kind of events.\smallskip
 *}
 
 (*<*)
@@ -1201,9 +1196,26 @@
   That means we have to add a waiting edge to the @{text RAG}. Furthermore
   the current precedence for all threads that are not dependants of @{text th}
   are unchanged. For the others we need to follow the edges 
-  in the @{text RAG} and recompute the @{term "cp"}. However, like in the 
-  case of @{text Set}, this operation can stop often earlier, namely when intermediate
-  values do not change.
+  in the @{text RAG} and recompute the @{term "cp"}. To do this we can start from @{term "th"} 
+  and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
+  the @{term "cp"} of every 
+  thread encountered on the way. Since the @{term "depend"}
+  is loop free, this procedure will always stop. The following lemma shows, however, 
+  that this procedure can actually stop often earlier without having to consider all
+  dependants.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  %%@ {t hm[mode=IfThen] eq_up_self}\\
+  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+  @{text "then"} @{thm (concl) eq_up}.
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  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
@@ -1301,8 +1313,10 @@
   problem, which however needs static analysis of programs in order to
   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 
+  checking techniques. The results obtained by them apply,
+  however, only to systems with a fixed size, such as a fixed number of 
+  events and threads. In contrast, our result applies to systems of arbitrary
+  size. Moreover, our result is a good 
   witness for one of the major reasons to be interested in machine checked 
   reasoning: gaining deeper understanding of the subject matter.
 
@@ -1311,9 +1325,10 @@
   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}.\medskip
+  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}.\medskip
 
   \noindent
   {\bf Acknowledgements:}




