pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:242a781135ba
+:8e02fb168350
 locking a resource prevented a high priority thread from running in
 time, leading to a system reset. Once the problem was found, it was
 rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
 \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
 Inheritance Protocol} \cite{Sha90} and others sometimes also call it
-\emph{Priority Boosting} or \emph{Priority Donation}.} in the scheduling software.
+\emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority Lending}.}
+in the scheduling software.
 The idea behind PIP is to let the thread $L$ temporarily inherit
 the high priority from $H$ until $L$ leaves the critical section
 unlocking the resource. This solves the problem of $H$ having to
 wait indefinitely, because $L$ cannot be blocked by threads having
 when a resource is released is irrelevant for PIP being correct---a
 fact that has not been mentioned in the literature and not been used
 in the reference implementation of PIP in PINTOS.  This fact, however, is important
 for an efficient implementation of PIP, because we can give the lock
 to the thread with the highest priority so that it terminates more
-quickly.
+quickly.  We were also bale 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 *}
 text {*
 \begin{center}
 @{thm[mode=Rule] thread_V[where thread=th]}
 \end{center}
 \noindent
+Note, however, that apart from the circularity condition, we do not make any
+assumption on how different resources can locked and released relative to each
+other. In our model it is possible that critical sections overlap. This is in
+contrast to Sha et al \cite{Sha90} who require that critical sections are
+properly nested.
 A valid state of PIP can then be conveniently be defined as follows:
 \begin{center}
 \begin{tabular}{c}
 @{thm[mode=Axiom] vt_nil}\hspace{1cm}
 \begin{center}
 \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
 \hline
 {\bf Event} & {\bf PINTOS function} \\
 \hline
-@{text Create} & @{text "thread_create"}\\
+@{text Create} & @{ML_text "thread_create"}\\
-@{text Exit}   & @{text "thread_exit"}\\
+@{text Exit}   & @{ML_text "thread_exit"}\\
-@{text Set}    & @{text "thread_set_priority"}\\
+@{text Set}    & @{ML_text "thread_set_priority"}\\
-@{text P}      & @{text "lock_acquire"}\\
+@{text P}      & @{ML_text "lock_acquire"}\\
-@{text V}      & @{text "lock_release"}\\
+@{text V}      & @{ML_text "lock_release"}\\
 \hline
 \end{tabular}
 \end{center}
 \noindent
 Our implicit assumption that every event is an atomic operation is ensured by the architecture of
-PINTOS. The case where an unlocked resource is given next to the waiting thread with the
+PINTOS (which allows to disable 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-implementation 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.
+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
+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
+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.
 \begin{figure}
 \begin{lstlisting}
 void lock_acquire (struct lock *lock)
 { ASSERT (lock != NULL);
 if (!lock) {
 heap_update(higher_cpreced, &ready_heap, &pt->helem);
 break;
 };
 heap_update(thread_preced, &lock->wq, &pt->helem);
-pt = lock -> holder;
+pt = lock->holder;
 };
 thread_block();
 } else {
 lock->value--;
 lock->holder = thread_current();
 \end{lstlisting}
 \caption{Our version of the {\tt lock\_release} function (implementing event @{text P}) in
 PINTOS.\label{code}}
 \end{figure}
-Let us illustrate that our specification translates relatively smoothly
-into C-code. The function {\tt lock\_aquire}, shown in Figure~\ref{code},
+Line 6 and 7 of {\tt lock\_aquire} make the operation of aquiring a lock atomic by disabling all
-implements the operation that
+interrupts, but saving them for resumption at the end of the function (Line 31).
-the currently running thread asks for the lock of a specific resource.
+In Line 8, the interesting code of the scheduler starts: we
-In C such a lock is represented as a pointer to the structure {\tt lock}. Lines 2 to
+test whether the lock is already taken (its value is then 0 indicating ``already
-4 contain diagnostic code for PINTOS: first we check that the lock is a ``valid'' lock
+taken'', and 1 for being ``free''). In case the lock is taken, we need to
-by testing it is not {\tt NULL}; second we check that the code is not called
+insert the current thread into the waiting queue of this lock (Line 9,
-as part of an interrupt---aquiring a lock should have been only initiated by a
+the waiting queue is referenced as @{ML_text "&lock-wq"}).
-request from a (user) thread, not an interrupt; third we make sure the
+Next we record that the current thread is waiting for the lock (Line 10).
-current thread does not ask twice for a lock. These assertions are supposed
-to be always satisfied because of the assumptions in PINTOS of how this code is called.
-If not, then there is a bug in PINTOS.
-Line 6 and 7 make the operation of aquiring a lock atomic by disabling all
-interrupts, but saving them for resumption at the ond of the function (Line 31).
-In Line 8, the interesting code of this function starts: we
-test whether lock is already taken (its value is 0 for 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 the lock (Line 9,
-the waiting queue is referenced as @{ML_text "&lock-wq"}). The queues are
-implemented as Braun Trees providing an heap interface, therefore
-the function is called @{ML_text "heap_insert"}. 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 @{text RAG} (Resource Allocation Graph). In Lines 11 and 12 we
+in the RAG (Resource Allocation Graph). For this we assign in Lines 11 and 12
-assign to the variable @{ML_text pt} the owner of the lock, and enter
+assign the variable @{ML_text pt} ot the owner of the lock, and enter
-a while-loop in Lines 13 to 24, which implements the ``chase''.
+the while-loop in Lines 13 to 24. This loop implements the ``chase''.
 *}
 section {* Conclusion *}
 goal: The formalisation allowed us to efficently implement our version
 of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86
 architecture. It also gives the first author enough data to enable
 his undergraduate students to implement PIP (as part of their OS course).
 A byproduct of our formalisation effort is that nearly all
-design choices for the PIP scheduler are backed up with a proved
+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.
+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
+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 11	8e02fb168350
parent 8	5ba3d79622da
child 12	85116bc854c0