pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:8e02fb168350
+:85116bc854c0
 \noindent
 {\bf Contributions:} There have been earlier formal investigations
 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
 system \cite{PINTOS}.  For example, we found by ``playing'' with the
 formalisation that the choice of the next thread to take over a lock
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_depend_def}
 \end{isabelle}
 \noindent
-Given four threads and three resources, an instance of a RAG can be pictured
+If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:
-as follows:
+\begin{figure}[h]
 \begin{center}
 \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
 \begin{tikzpicture}[scale=1]
 %%\draw[step=2mm] (-3,2) grid (1,-1);
 \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
 \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
 \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
 that the resource is locked.
 \end{isabelle}
 \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}
 @{thm readys_def}\\
 @{thm runing_def}
 Inversion. For this we further have to assume that every thread
 gives up its resources after a finite amount of time. We found that
 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.
 In what follows we will describe properties of PIP that allow us to prove
 (*>*)
 text {*
 \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
 Stanford University \cite{PINTOS}. To implement PIP, we only need to modify the kernel
 functions corresponding to the events in our formal model. The events translate to the following
 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-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
+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
+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
+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.
 ASSERT (!lock_held_by_current_thread (lock));
 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);
+heap_update(lock_cprec, &pt->held, &lock->helem);
-if (!(update_cpreced(pt)))
+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();
 } else {
 lock->value--;
 heap_insert(lock_prec, &thread_current()->held, &lock->helem);
 };
 intr_set_level(old_level);
 }
 \end{lstlisting}
-\caption{Our version of the {\tt lock\_release} function (implementing event @{text P}) in
+\caption{Our version of the {\tt lock\_release} function in
-PINTOS.\label{code}}
+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
+taken'', or 1 for being ``free''). In case the lock is taken, we enter the
-insert the current thread into the waiting queue of this lock (Line 9,
+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
+According to our specification, we need to next ``chase'' the dependants
-in the RAG (Resource Allocation Graph). For this we assign in Lines 11 and 12
+in the RAG (Resource Allocation Graph), but we can stop whenever there
-assign the variable @{ML_text pt} ot the owner of the lock, and enter
+is no change in the @{text cprec}. Befre we start the loop, we
-the while-loop in Lines 13 to 24. This loop implements the ``chase''.
+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
 *}
 section {* Conclusion *}

changeset 12	85116bc854c0
parent 11	8e02fb168350
child 13	735e36c64a71