pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:9764023f719e
+:105715a0a807
 \end{tabular}
 \end{isabelle}
 \noindent
 In this definition we assume @{text "set"} converts a list into a set.
+Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow
+from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL.
 At the beginning, that is in the state where no thread is created yet,
 the waiting queue function will be the function that returns the
 empty list for every resource.
 \begin{isabelle}\ \ \ \ \ %%%
 waiting edge. The reason is that when a thread asks for resource that is locked
 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. 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
 the notion of the \emph{dependants} of a thread using the transitive closure
 operation for relations. This gives
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
-\hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
+\hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\
 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
 \end{tabular}
 \end{isabelle}
 Having the scheduler function @{term schs} at our disposal, we can ``lift'', or
 Our implicit assumption that every event is an atomic operation is ensured by the architecture of
 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
+for accessing and updating. In the code we shall describe below, we use the function
+@{ML_text "queue_insert"}, for inserting a new element into a priority queue, and
+@{ML_text "queue_update"}, for updating the position of an element that is already
+in a queue. Both functions take an extra argument that specifies the
+comparison function used for organising the priority queue.
+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 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 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 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, 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 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}.
+a ``kernel panic''.
 \begin{figure}[t]
 \begin{lstlisting}
 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 for the small operating
+\caption{Our version of the {\tt lock\_acquire} function for the small operating
 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
 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 from one thread at hand to another.
+current precedence.
 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
 of the lock.
 Similar operations need to be implementated for the @{ML_text lock_release} function, which
 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}.
+that their C-code satisfies its specification, thought this specification does not contain
-Our verification however provided us with the justification for designing
+anything about PIP \cite{sel4}.
+Our verification of PIP 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.
 *}
 the proof of Sha et al.: they require that critical sections nest properly,
 whereas our scheduler allows critical sections to overlap.
 PIP is a scheduling algorithm for single-processor systems. We are
 now living in a multi-processor world. Priority Inversion certainly
-occurs also there, see for example \cite{Brandenburg11, Davis11}
+occurs also there, see for example \cite{Brandenburg11, Davis11}.
 However, there is very little ``foundational''
 work about PIP-algorithms on multi-processor systems.  We are not
 aware of any correctness proofs, not even informal ones. There is an
 implementation of a PIP-algorithm for multi-processors as part of the
 ``real-time'' effort in Linux, including an informal description of the implemented scheduling

changeset 17	105715a0a807
parent 16	9764023f719e
child 20	b56616fd88dd