
diff -r 1bf194825a4e -r 9e664c268e25 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Dec 21 18:06:00 2012 +0000
+++ b/Journal/Paper.thy	Fri Dec 21 23:32:58 2012 +0000
@@ -1285,33 +1285,34 @@
 
   \noindent
   Our implicit assumption that every event is an atomic operation is ensured by the architecture of 
-  PINTOS (which allows to disable interrupts when some operations are performed). The case where 
+  PINTOS (which allows disabling of interrupts when some operations are performed). The case where 
   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
   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 of the function {\tt lock\_acquire}, 
+  Let us illustrate this with the C-code for the function @{ML_text "lock_acquire"}, 
   shown in Figure~\ref{code}.  This function implements the operation of requesting and, if free, 
-  locking of a resource by the currently running thread. The convention in the PINTOS
-  code is use the terminology \emph{locks} rather than resources. 
+  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 of the function @{ML_text "lock_acquire"} contain diagnostic code: first, we check that 
+  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 
   the lock is a ``valid'' lock 
-  by testing whether it is not {\tt NULL}; second, we check that the code is not called
+  by testing whether it is not {\tt NULL}; second, a check that the code is not called
   as part of an interrupt---acquiring a lock should only be initiated by a 
-  request from a (user) thread, not an interrupt; third, we make sure the 
+  request from a (user) thread, not from an interrupt; third, it is ensured that the 
   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}. We took these three lines from the original code of 
-  @{ML_text "lock_acquire"} in PINTOS.
+  a \emph{kernel panic}. 
 
 
 
-  \begin{figure}
+  \begin{figure}[t]
   \begin{lstlisting}
 void lock_acquire (struct lock *lock)
 { ASSERT (lock != NULL);
@@ -1346,8 +1347,8 @@
   intr_set_level(old_level);
 }
   \end{lstlisting}
-  \caption{Our version of the {\tt lock\_release} function in 
-  PINTOS.  It implements the operation corresponding to a @{text P}-event.\label{code}}
+  \caption{Our version of the {\tt lock\_release} function for the small operating 
+  system PINTOS.  It implements the operation corresponding to a @{text P}-event.\label{code}}
   \end{figure}
 
  
@@ -1358,13 +1359,13 @@
   taken'', or 1 for being ``free''). In case the lock is taken, we enter the
   if-branch inserting the current thread into the waiting queue of this lock (Line 9).
   The waiting queue is referenced in the usual C-way as @{ML_text "&lock->wq"}. 
-  Next we record that the current thread is waiting for the lock (Line 10).
+  Next, we record that the current thread is waiting for the lock (Line 10).
   Thus we established two pointers: one in the waiting queue of the lock pointing to the 
   current thread, and the other from the currend thread pointing to the lock.
   According to our specification in Section~\ref{model} and the properties we were able 
   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; however we only have to do this as long as there is change in the 
   current precedence from one thread at hand to another. 
 
   The ``chase'' is implemented in the while-loop in Lines 13 to 24. 
@@ -1376,7 +1377,7 @@
   then we leave the loop, since nothing else needs to be updated (Lines 15 and 16).
   If there is a change, then we have to continue our ``chase''. We check what lock the 
   thread @{ML_text pt} is waiting for (Lines 17 and 18). If there is none, then 
-  the thread @{ML_text pt} is ready (the ``chase'' is finished with finding a root). In this 
+  the thread @{ML_text pt} is ready (the ``chase'' is finished with finding a root in the RAG). In this 
   case we update the ready-queue accordingly (Lines 19 and 20). If there is a lock  @{ML_text pt} is 
   waiting for, we update the waiting queue for this lock and we continue the loop with 
   the holder of that lock 
@@ -1388,14 +1389,17 @@
   it is taken now (Line 27). Second, we update the reference of the holder of 
   the lock (Line 28), and finally update the queue of locks the current 
   thread already possesses (Line 29).
-  The very last is to enable interrupts again thus leaving the protected section.
+  The very last step is to enable interrupts again thus leaving the protected section.
   
 
   Similar operations need to be implementated for the @{ML_text lock_release} function, which
-  we however do not show. The reader should note that we did not verify our C-code. The
-  verification of the specification however provided us with the justification for designing 
-  the C-code in this way. It gave us confidence for leaving the ``chase'' early whenever
-  there is no change in the calculated current precedence.
+  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 
+  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.
 *}
 
 section {* Conclusion *}




