--- 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 *}
--- a/Journal/document/root.bib Fri Dec 21 18:06:00 2012 +0000
+++ b/Journal/document/root.bib Fri Dec 21 23:32:58 2012 +0000
@@ -1,3 +1,27 @@
+@article{seL4,
+ author = {G.~Klein and
+ J.~Andronick and
+ K.~Elphinstone and
+ G.~Heiser and
+ D.~Cock and
+ P.~Derrin and
+ D.~Elkaduwe and
+ K.~Engelhardt and
+ R.~Kolanski and
+ M.~Norrish and
+ T.~Sewell and
+ H.~Tuch and
+ S.~Winwood},
+ title = {{seL4}: {F}ormal {V}erification of an {OS} {K}ernel},
+ journal = {Communications of the ACM},
+ publisher = {ACM},
+ year = {2010},
+ pages = {107--115},
+ volume = 53,
+ number = 6
+}
+
+
@phdthesis{Brandenburg11,
Author = {Bj\"{o}rn B. Brandenburg},
School = {The University of North Carolina at Chapel Hill},
Binary file journal.pdf has changed