diff -r 85116bc854c0 -r 735e36c64a71 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Dec 21 00:24:30 2012 +0000
+++ b/Journal/Paper.thy	Fri Dec 21 13:30:14 2012 +0000
@@ -178,8 +178,8 @@
   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.  We were also bale to generalise the scheduler of Sha
-  et al \cite{Sha90} to the practically relevant case where critical 
+  quickly.  We were also able to generalise the scheduler of Sha
+  et al.~\cite{Sha90} to the practically relevant case where critical 
   sections can overlap.
 *}
 
@@ -368,7 +368,7 @@
   \draw [<-,line width=0.6mm] (U2) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (R);
   \end{tikzpicture}
   \end{center}
-  \caption{An Instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}
+  \caption{An instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}
   \end{figure}
 
   \noindent
@@ -376,9 +376,10 @@
   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 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.
+  already, then the process is blocked 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.
+  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
@@ -547,8 +548,9 @@
   \noindent
   With these abbreviations in place we can introduce 
   the notion of a thread being @{term ready} in a state (i.e.~threads
-  that do not wait for any resource, i.e.~the roots of the trees in the RAG, see 
-  Figure~\ref{RAGgraph}) and the running thread.
+  that do not wait for any resource, which are the roots of the trees 
+  in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread
+  is then the thread with the highest current precedence of all ready threads.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -566,7 +568,8 @@
   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 and also when a thread is detached in a state (meaning the thread neither 
-  holds nor waits for a resource):
+  holds nor waits for a resource---in the RAG this would correspond to an
+  isolated node without any incoming and outgoing edges, see Figure~\ref{RAGgraph}):
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -766,7 +769,7 @@
   one resource---that means the thread was not \emph{detached} in @{text s}. 
   As we shall see shortly, that means there are only finitely 
   many threads that can block @{text th} in this way and then they 
-  need to run with the same current precedence as @{text th}.
+  need to run with the same precedence as @{text th}.
 
   Like in the argument by Sha et al.~our
   finite bound does not guarantee absence of indefinite Priority
@@ -1228,7 +1231,7 @@
 
   \noindent
   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}
+  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"}. To do this we can start from @{term "th"} 
   and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem} 
@@ -1289,15 +1292,15 @@
   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\_aquire}, 
+  Let us illustrate this with the C-code of the function {\tt lock\_acquire}, 
   shown in Figure~\ref{code}.  This function implements the operation that
   the currently running thread asks for the lock of a resource. 
   In C such a lock is represented as a pointer to the structure {\tt lock} (Line 1). 
 
-  Lines 2 to 4 of {\tt lock\_aquire} contain diagnostic code: first, we check that 
+  Lines 2 to 4 of {\tt lock\_acquire} contain diagnostic code: first, we check that 
   the lock is a ``valid'' lock 
   by testing it is not {\tt NULL}; second, we check that the code is not called
-  as part of an interrupt---aquiring a lock should only be initiated by a 
+  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 
   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.
@@ -1315,27 +1318,27 @@
   enum intr_level old_level;
   old_level = intr_disable();
   if (lock->value == 0) {
-    heap_insert(thread_cprec, &lock->wq, &thread_current()->helem); 
+    queue_insert(thread_cprec, &lock->wq, &thread_current()->helem); 
     thread_current()->waiting = lock;
     struct thread *pt;
     pt = lock->holder;
     while (pt) {
-      heap_update(lock_cprec, &pt->held, &lock->helem);
+      queue_update(lock_cprec, &pt->held, &lock->helem);
       if (!(update_cprec(pt)))
         break;
       lock = pt->waiting;
       if (!lock) {
-        heap_update(higher_cprec, &ready_heap, &pt->helem);
+        queue_update(higher_cprec, &ready_queue, &pt->helem);
         break;
       };
-      heap_update(thread_cprec, &lock->wq, &pt->helem);
+      queue_update(thread_cprec, &lock->wq, &pt->helem);
       pt = lock->holder;
     };
     thread_block();
   } else {
     lock->value--;
     lock->holder = thread_current();
-    heap_insert(lock_prec, &thread_current()->held, &lock->helem); 
+    queue_insert(lock_prec, &thread_current()->held, &lock->helem); 
   };
   intr_set_level(old_level);
 }
@@ -1345,20 +1348,38 @@
   \end{figure}
 
  
-  Line 6 and 7 of {\tt lock\_aquire} make the operation of aquiring a lock atomic by disabling all 
+  Line 6 and 7 of {\tt lock\_acquire} make the operation of acquiring a lock atomic by disabling all 
   interrupts, but saving them for resumption at the end of the function (Line 31).
-  In Line 8, the interesting code starts: we 
+  In Line 8, the interesting code with respect to scheduling starts: we 
   test whether the lock is already taken (its value is then 0 indicating ``already 
   taken'', or 1 for being ``free''). In case the lock is taken, we enter the
-  if-branch by first inserting the current thread into the waiting queue of this lock (Line 9,
-  the waiting queue is referenced as @{ML_text "&lock-wq"}). 
+  if-branch by first 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).
   According to our specification, we need to next ``chase'' the dependants 
-  in the RAG (Resource Allocation Graph), but we can stop whenever there
-  is no change in the @{text cprec}. Befre we start the loop, we 
-  assign in Lines 11 and 12 assign the variable @{ML_text pt} to the owner 
-  of the lock, and enter the while-loop in Lines 13 to 24. \ldots
+  in the RAG (Resource Allocation Graph), but we can stop the ``chase'' whenever 
+  there is no change in the @{text cprec}. To start the loop, we 
+  assign in Lines 11 and 12 the variable @{ML_text pt} to the owner 
+  of the lock, and then enter the while-loop in Lines 13 to 24. 
+  
+  Inside the loop, we first update the precedence of the lock held by @{ML_text pt} (Line 14).
+  Next, we test if there is a change in the current precedence of @{ML_text pt}. If not,
+  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 the lock
+  @{ML_text pt} is waiting for (Lines 17 and 18). If there isn't one, the thread @{ML_text pt}
+  is ready (the ``chase'' finished with finding a root) and 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 
+  (Lines 22 and 23). Finally we need to block the current thread, since the lock 
+  it asked for was taken (Line 25). 
 
+  If the lock was not taken, we take the else-branch (Lines 26 to 30). We first 
+  decrease the value of the lock to 0, meaning it is taken now (Line 27).
+  We update the reference of holder of the lock (Line 28) and finally update
+  the queue of locks the current thread already possesses (Line 29).
+  Finally, we enable interrupts again, leaving the protected section of PINTOS.
+  Similar operations need to be implementated for the @{ML_text lock_release} function, which
+  we omit.
 *}
 
 section {* Conclusion *}