pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:735e36c64a71
+:1bf194825a4e
 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
 ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
 example in libraries for FreeBSD, Solaris and Linux.
 One advantage of PIP is that increasing the priority of a thread
-can be dynamically calculated by the scheduler. This is in contrast
+can be performed dynamically by the scheduler. This is in contrast
 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
 solution to the Priority Inversion problem, which requires static
 analysis of the program in order to prevent Priority
 Inversion. However, there has also been strong criticism against
 PIP. For instance, PIP cannot prevent deadlocks when lock
 quickly.  We were also able to generalise the scheduler of Sha
 et al.~\cite{Sha90} to the practically relevant case where critical
 sections can overlap.
 *}
-section {* Formal Model of the Priority Inheritance Protocol *}
+section {* Formal Model of the Priority Inheritance Protocol\label{model} *}
 text {*
 The Priority Inheritance Protocol, short PIP, is a scheduling
 algorithm for a single-processor system.\footnote{We shall come back
 later to the case of PIP on multi-processor systems.}
 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},
-shown in Figure~\ref{code}.  This function implements the operation that
+shown in Figure~\ref{code}.  This function implements the operation of requesting and, if free,
-the currently running thread asks for the lock of a resource.
+locking of a resource by the currently running thread. The convention in the PINTOS
-In C such a lock is represented as a pointer to the structure {\tt lock} (Line 1).
+code is 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 {\tt lock\_acquire} contain diagnostic code: first, we check that
+Lines 2 to 4 of the function @{ML_text "lock_acquire"} 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 whether it is not {\tt NULL}; second, we 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
 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.
+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.
 \begin{figure}
 \begin{lstlisting}
 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
-test whether the lock is already taken (its value is then 0 indicating ``already
+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 by first inserting the current thread into the waiting queue of this lock (Line 9).
+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).
-According to our specification, we need to next ``chase'' the dependants
+Thus we established two pointers: one in the waiting queue of the lock pointing to the
-in the RAG (Resource Allocation Graph), but we can stop the ``chase'' whenever
+current thread, and the other from the currend thread pointing to the lock.
-there is no change in the @{text cprec}. To start the loop, we
+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.
+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, and then enter the while-loop in Lines 13 to 24.
+of the lock.
+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
+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.
-Inside the loop, we first update the precedence of the lock held by @{ML_text pt} (Line 14).
-Next, we test if 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 the lock
-@{ML_text pt} is waiting for (Lines 17 and 18). If there isn't one, the thread @{ML_text pt}
-is ready (the ``chase'' finished with finding a root) and 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). Finally we need to block the current thread, since the lock
-it asked for was taken (Line 25).
-If the lock was not taken, we take the else-branch (Lines 26 to 30). We first
-decrease the value of the lock to 0, meaning it is taken now (Line 27).
-We update the reference of holder of the lock (Line 28) and finally update
-the queue of locks the current thread already possesses (Line 29).
-Finally, we enable interrupts again, leaving the protected section of PINTOS.
 Similar operations need to be implementated for the @{ML_text lock_release} function, which
-we omit.
+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.
 *}
 section {* Conclusion *}
 text {*
 design choices for the implementation of PIP scheduler are backed up with a proved
 lemma. We were also able to establish the property that the choice of
 the next thread which takes over a lock is irrelevant for the correctness
 of PIP. Moreover, we eliminated a crucial restriction present in
 the proof of Sha et al.: they require that critical sections nest properly,
-whereas our scheduler allows critical sections to overlap. This is the default
+whereas our scheduler allows critical sections to overlap.
-in implementations of PIP.
 PIP is a scheduling algorithm for single-processor systems. We are
 now living in a multi-processor world. Priority Inversion certainly
 occurs also there.  However, there is very little ``foundational''
 work about PIP-algorithms on multi-processor systems.  We are not

changeset 14	1bf194825a4e
parent 13	735e36c64a71
child 15	9e664c268e25