--- a/Journal/Paper.thy	Sat Dec 22 01:58:45 2012 +0000
+++ b/Journal/Paper.thy	Sat Dec 22 14:50:29 2012 +0000
@@ -302,6 +302,8 @@
 
   \noindent
   In this definition we assume @{text "set"} converts a list into a set.
+  Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow
+  from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL. 
   At the beginning, that is in the state where no thread is created yet, 
   the waiting queue function will be the function that returns the
   empty list for every resource.
@@ -380,6 +382,7 @@
   Clearly, also every resource can only have at most one outgoing holding edge---indicating
   that the resource is locked. In this way we can always start at a thread waiting for a 
   resource and ``chase'' outgoing arrows leading to a single root of a tree. 
+  
 
 
   The use of relations for representing RAGs allows us to conveniently define
@@ -527,7 +530,7 @@
   \begin{tabular}{@ {}l}
   @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
   \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
-  \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\
   \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
   \end{tabular}
   \end{isabelle}
@@ -1289,7 +1292,13 @@
   an unlocked resource is given next to the waiting thread with the
   highest precedence is realised in our implementation by priority queues. We implemented
   them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
-  for accessing and updating. Apart from having to implement relatively complex data\-structures in C
+  for accessing and updating. In the code we shall describe below, we use the function
+  @{ML_text "queue_insert"}, for inserting a new element into a priority queue, and 
+  @{ML_text "queue_update"}, for updating the position of an element that is already
+  in a queue. Both functions take an extra argument that specifies the
+  comparison function used for organising the priority queue.
+  
+  Apart from having to implement relatively complex data\-structures in C
   using pointers, our experience with the implementation has been very positive: our specification 
   and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. 
   Let us illustrate this with the C-code for the function @{ML_text "lock_acquire"}, 
@@ -1297,7 +1306,6 @@
   locking of a resource by the current running thread. The convention in the PINTOS
   code is to use the terminology \emph{locks} rather than resources. 
   A lock is represented as a pointer to the structure {\tt lock} (Line 1). 
-
   Lines 2 to 4 are taken from the original 
   code of @{ML_text "lock_acquire"} in PINTOS. They contain diagnostic code: first, 
   there is a check that 
@@ -1308,7 +1316,7 @@
   current thread does not ask twice for a lock. These assertions are supposed
   to be satisfied because of the assumptions in PINTOS about how this code is called.
   If not, then the assertions indicate a bug in PINTOS and the result will be
-  a \emph{kernel panic}. 
+  a ``kernel panic''. 
 
 
 
@@ -1347,7 +1355,7 @@
   intr_set_level(old_level);
 }
   \end{lstlisting}
-  \caption{Our version of the {\tt lock\_release} function for the small operating 
+  \caption{Our version of the {\tt lock\_acquire} function for the small operating 
   system PINTOS.  It implements the operation corresponding to a @{text P}-event.\label{code}}
   \end{figure}
 
@@ -1366,7 +1374,7 @@
   to prove for @{text P}, we need to ``chase'' all the dependants 
   in the RAG (Resource Allocation Graph) and update their
   current precedence; however we only have to do this as long as there is change in the 
-  current precedence from one thread at hand to another. 
+  current precedence.
 
   The ``chase'' is implemented in the while-loop in Lines 13 to 24. 
   To initialise the loop, we 
@@ -1395,8 +1403,9 @@
   Similar operations need to be implementated for the @{ML_text lock_release} function, which
   we however do not show. The reader should note though that we did \emph{not} verify our C-code. 
   This is in contrast, for example, to the work on seL4, which actually verified in Isabelle/HOL
-  that their C-code satisfies its specification \cite{sel4}.
-  Our verification however provided us with the justification for designing 
+  that their C-code satisfies its specification, thought this specification does not contain 
+  anything about PIP \cite{sel4}.
+  Our verification of PIP however provided us with the justification for designing 
   the C-code. It gave us confidence that leaving the ``chase'' early, whenever
   there is no change in the calculated current precedence, does not break the
   correctness of the algorithm.
@@ -1444,7 +1453,7 @@
 
   PIP is a scheduling algorithm for single-processor systems. We are
   now living in a multi-processor world. Priority Inversion certainly
-  occurs also there, see for example \cite{Brandenburg11, Davis11}  
+  occurs also there, see for example \cite{Brandenburg11, Davis11}.  
   However, there is very little ``foundational''
   work about PIP-algorithms on multi-processor systems.  We are not
   aware of any correctness proofs, not even informal ones. There is an