# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1355960796 0
# Node ID 5ba3d79622dae010147dc36234174cd2eb7a50b0
# Parent  0514be2ad83e5cc05d2489ad5549c9688b783e0c
added a paragraph about RAGS

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''.  
 
 *}
 
diff -r 0514be2ad83e -r 5ba3d79622da Journal/document/root.tex
--- a/Journal/document/root.tex	Wed Dec 19 12:51:06 2012 +0000
+++ b/Journal/document/root.tex	Wed Dec 19 23:46:36 2012 +0000
@@ -68,12 +68,14 @@
 the Property Inheritance Protocol presents a correctness ``proof'' for
 an \emph{incorrect} algorithm. In this paper we fix the problem of
 this proof by making all notions precise and implementing a variant of
-a solution proposed earlier. Our formalisation in Isabelle/HOL
+a solution proposed earlier. We also generalise the result to the
+practically relevant case where critical sections can
+overlap. Our formalisation in Isabelle/HOL not just
 uncovers facts not mentioned in the literature, but also shows how to
 efficiently implement this protocol. Earlier correct implementations
 were criticised as too inefficient. Our formalisation is based on
 Paulson's inductive approach to verifying protocols; our implementation
-is on top of the small PINTOS operating system.\medskip
+builds on top of the small PINTOS operating system.\medskip
 
 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
 %real-time systems, Isabelle/HOL
diff -r 0514be2ad83e -r 5ba3d79622da journal.pdf
Binary file journal.pdf has changed