pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:1bf194825a4e
+:9e664c268e25
 \end{tabular}
 \end{center}
 \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
+locking of a resource by the current running thread. The convention in the PINTOS
-code is use the terminology \emph{locks} rather than resources.
+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
+a \emph{kernel panic}.
-@{ML_text "lock_acquire"} in PINTOS.
+\begin{figure}[t]
-\begin{figure}
 \begin{lstlisting}
 void lock_acquire (struct lock *lock)
 { ASSERT (lock != NULL);
 ASSERT (!intr_context());
 ASSERT (!lock_held_by_current_thread (lock));
 queue_insert(lock_prec, &thread_current()->held, &lock->helem);
 };
 intr_set_level(old_level);
 }
 \end{lstlisting}
-\caption{Our version of the {\tt lock\_release} function in
+\caption{Our version of the {\tt lock\_release} function for the small operating
-PINTOS.  It implements the operation corresponding to a @{text P}-event.\label{code}}
+system PINTOS.  It implements the operation corresponding to a @{text P}-event.\label{code}}
 \end{figure}
 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 with respect to scheduling starts: we
 first check 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 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.
 To initialise the loop, we
 assign in Lines 11 and 12 the variable @{ML_text pt} to the owner
 Inside the loop, we first update the precedence of the lock held by @{ML_text pt} (Line 14).
 Next, we check whether 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 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
 (Lines 22 and 23). After all current precedences have been updated, we finally need
 to block the current thread, because the lock it asked for was taken (Line 25).
 If the lock the current thread asked for is \emph{not} taken, we proceed with the else-branch
 (Lines 26 to 30). We first decrease the value of the lock to 0, meaning
 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
+we however do not show. The reader should note though that we did \emph{not} verify our C-code.
-verification of the specification however provided us with the justification for designing
+This is in contrast, for example, to the work on seL4, which actually verified in Isabelle/HOL
-the C-code in this way. It gave us confidence for leaving the ``chase'' early whenever
+that their C-code satisfies its specification \cite{sel4}.
-there is no change in the calculated current precedence.
+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 *}
 text {*

changeset 15	9e664c268e25
parent 14	1bf194825a4e
child 16	9764023f719e