--- a/Journal/Paper.thy Thu Dec 20 14:54:06 2012 +0000
+++ b/Journal/Paper.thy Fri Dec 21 00:24:30 2012 +0000
@@ -167,7 +167,7 @@
into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
checking techniques. This paper presents a formalised and
mechanically checked proof for the correctness of PIP. For this we
- needed to design a new correctness criterion. In contrast to model checking, our
+ needed to design a new correctness criterion for PIP. In contrast to model checking, our
formalisation provides insight into why PIP is correct and allows us
to prove stronger properties that, as we will show, can help with an
efficient implementation of PIP in the educational PINTOS operating
@@ -331,9 +331,9 @@
\end{isabelle}
\noindent
- Given four threads and three resources, an instance of a RAG can be pictured
- as follows:
+ If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:
+ \begin{figure}[h]
\begin{center}
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
\begin{tikzpicture}[scale=1]
@@ -347,19 +347,34 @@
\node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
\node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+ \node (X) at (0,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>4"}};
+ \node (Y) at (2,-2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>4"}};
+ \node (Z) at (2,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>5"}};
+ \node (U1) at (4,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>5"}};
+ \node (U2) at (4,-2.9) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>6"}};
+ \node (R) at (6,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>6"}};
+
\draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
\draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);
\draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E);
\draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1);
\draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);
+
+ \draw [->,line width=0.6mm] (U1) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (Y);
+ \draw [->,line width=0.6mm] (U2) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (Z);
+ \draw [<-,line width=0.6mm] (X) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (Z);
+ \draw [<-,line width=0.6mm] (X) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (Y);
+ \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}}
+ \end{figure}
\noindent
We will design our scheduler
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 only one outgoing
+ 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.
Clearly, also every resource can only have at most one outgoing holding edge---indicating
@@ -532,7 +547,8 @@
\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) and the running thread.
+ 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.
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -759,7 +775,7 @@
this assumption is awkward to formalise in our model. Therefore we
leave it out and let the programmer assume the responsibility to
program threads in such a benign manner (in addition to causing no
- circularity in the @{text RAG}). In this detail, we do not
+ circularity in the RAG). In this detail, we do not
make any progress in comparison with the work by Sha et al.
However, we are able to combine their two separate bounds into a
single theorem improving their bound.
@@ -1242,7 +1258,7 @@
\noindent
As can be seen, a pleasing byproduct of our formalisation is that the properties in
this section closely inform an implementation of PIP, namely whether the
- @{text RAG} needs to be reconfigured or current precedences need to
+ RAG needs to be reconfigured or current precedences need to
be recalculated for an event. This information is provided by the lemmas we proved.
We confirmed that our observations translate into practice by implementing
our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at
@@ -1273,16 +1289,16 @@
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-implementation of the function {\tt lock\_aquire},
+ Let us illustrate this with the C-code of the function {\tt lock\_aquire},
shown in Figure~\ref{code}. This function implements the operation that
- the currently running thread asks for the lock of a specific resource.
+ 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\_aquire} 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 have been only initiated by a
- request from a (user) thread, not an interrupt; third we make sure the
+ 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
+ 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.
If not, then the assertions indicate a bug in PINTOS.
@@ -1299,20 +1315,20 @@
enum intr_level old_level;
old_level = intr_disable();
if (lock->value == 0) {
- heap_insert(thread_preced, &lock->wq, &thread_current()->helem);
+ heap_insert(thread_cprec, &lock->wq, &thread_current()->helem);
thread_current()->waiting = lock;
struct thread *pt;
pt = lock->holder;
while (pt) {
- heap_update(lock_preced, &pt->held, &lock->helem);
- if (!(update_cpreced(pt)))
+ heap_update(lock_cprec, &pt->held, &lock->helem);
+ if (!(update_cprec(pt)))
break;
lock = pt->waiting;
if (!lock) {
- heap_update(higher_cpreced, &ready_heap, &pt->helem);
+ heap_update(higher_cprec, &ready_heap, &pt->helem);
break;
};
- heap_update(thread_preced, &lock->wq, &pt->helem);
+ heap_update(thread_cprec, &lock->wq, &pt->helem);
pt = lock->holder;
};
thread_block();
@@ -1324,23 +1340,24 @@
intr_set_level(old_level);
}
\end{lstlisting}
- \caption{Our version of the {\tt lock\_release} function (implementing event @{text P}) in
- PINTOS.\label{code}}
+ \caption{Our version of the {\tt lock\_release} function in
+ PINTOS. It implements the operation corresponding to a @{text P}-event.\label{code}}
\end{figure}
Line 6 and 7 of {\tt lock\_aquire} make the operation of aquiring 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 of the scheduler starts: we
+ In Line 8, the interesting code starts: we
test whether the lock is already taken (its value is then 0 indicating ``already
- taken'', and 1 for being ``free''). In case the lock is taken, we need to
- insert the current thread into the waiting queue of this lock (Line 9,
+ 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"}).
Next we record that the current thread is waiting for the lock (Line 10).
- According to our specification, we need to ``chase'' the holders of locks
- in the RAG (Resource Allocation Graph). For this we assign in Lines 11 and 12
- assign the variable @{ML_text pt} ot the owner of the lock, and enter
- the while-loop in Lines 13 to 24. This loop implements the ``chase''.
+ 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
*}