diff -r 0514be2ad83e -r 5ba3d79622da Journal/Paper.thy
--- a/Journal/Paper.thy	Wed Dec 19 12:51:06 2012 +0000
+++ b/Journal/Paper.thy	Wed Dec 19 23:46:36 2012 +0000
@@ -165,8 +165,8 @@
   {\bf Contributions:} There have been earlier formal investigations
   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
+  mechanically checked proof for the correctness of PIP. For this we 
+  needed to design a new correctness criterion. 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 help with an
   efficient implementation of PIP in the educational PINTOS operating
@@ -354,6 +354,15 @@
   \end{center}
 
   \noindent
+  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 only one outgoing  
+  waiting edge. The reason is that when a thread asks for resource that is locked
+  already, then the process is stopped and cannot ask for another resource.
+  Clearly, also every resource can only have at most one outgoing holding edge---indicating
+  that the resource is locked.
+
+
   The use of relations for representing RAGs allows us to conveniently define
   the notion of the \emph{dependants} of a thread using the transitive closure
   operation for relations. This gives
@@ -1317,6 +1326,10 @@
   implemented as Braun Trees providing an heap interface, therefore
   the function is called @{ML_text "heap_insert"}. Next we
   record that the current thread is waiting for the lock (Line 10).
+  According to our specification, we need to ``chase'' the holders of locks
+  in the @{text RAG} (Resource Allocation Graph). In Lines 11 and 12 we
+  assign to the variable @{ML_text pt} the owner of the lock, and enter
+  a while-loop in Lines 13 to 24, which implements the ``chase''.  
 
 *}