pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:85116bc854c0
+:735e36c64a71
 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.  We were also bale to generalise the scheduler of Sha
+quickly.  We were also able to generalise the scheduler of Sha
-et al \cite{Sha90} to the practically relevant case where critical
+et al.~\cite{Sha90} to the practically relevant case where critical
 sections can overlap.
 *}
 section {* Formal Model of the Priority Inheritance Protocol *}
 \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}}
+\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 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.
+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.
+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
 \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, i.e.~the roots of the trees in the RAG, see
+that do not wait for any resource, which are the roots of the trees
-Figure~\ref{RAGgraph}) and the running thread.
+in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread
+is then the thread with the highest current precedence of all ready threads.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm readys_def}\\
 @{thm runing_def}
 If there is one or more threads ready, then there can only be \emph{one} thread
 running, namely the one whose current precedence is equal to the maximum of all ready
 threads. We use sets to capture both possibilities.
 We can now also conveniently define the set of resources that are locked by a thread in a
 given state and also when a thread is detached in a state (meaning the thread neither
-holds nor waits for a resource):
+holds nor waits for a resource---in the RAG this would correspond to an
+isolated node without any incoming and outgoing edges, see Figure~\ref{RAGgraph}):
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm holdents_def}\\
 @{thm detached_def}
 the state @{text "s' @ s"} by a thread @{text th'} that already
 existed in @{text s} and requested or had a lock on at least
 one resource---that means the thread was not \emph{detached} in @{text s}.
 As we shall see shortly, that means there are only finitely
 many threads that can block @{text th} in this way and then they
-need to run with the same current precedence as @{text th}.
+need to run with the same precedence as @{text th}.
 Like in the argument by Sha et al.~our
 finite bound does not guarantee absence of indefinite Priority
 Inversion. For this we further have to assume that every thread
 gives up its resources after a finite amount of time. We found that
 \end{tabular}
 \end{isabelle}
 \noindent
 That means we have to add a waiting edge to the @{text RAG}. Furthermore
-the current precedence for all threads that are not dependants of @{text th}
+the current precedence for all threads that are not dependants of @{text "th'"}
 are unchanged. For the others we need to follow the edges
 in the @{text RAG} and recompute the @{term "cp"}. To do this we can start from @{term "th"}
 and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
 the @{term "cp"} of every
 thread encountered on the way. Since the @{term "depend"}
 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-code of the function {\tt lock\_aquire},
+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
 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\_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
-as part of an interrupt---aquiring a lock should only be initiated by a
+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.
 ASSERT (!lock_held_by_current_thread (lock));
 enum intr_level old_level;
 old_level = intr_disable();
 if (lock->value == 0) {
-heap_insert(thread_cprec, &lock->wq, &thread_current()->helem);
+queue_insert(thread_cprec, &lock->wq, &thread_current()->helem);
 thread_current()->waiting = lock;
 struct thread *pt;
 pt = lock->holder;
 while (pt) {
-heap_update(lock_cprec, &pt->held, &lock->helem);
+queue_update(lock_cprec, &pt->held, &lock->helem);
 if (!(update_cprec(pt)))
 break;
 lock = pt->waiting;
 if (!lock) {
-heap_update(higher_cprec, &ready_heap, &pt->helem);
+queue_update(higher_cprec, &ready_queue, &pt->helem);
 break;
 };
-heap_update(thread_cprec, &lock->wq, &pt->helem);
+queue_update(thread_cprec, &lock->wq, &pt->helem);
 pt = lock->holder;
 };
 thread_block();
 } else {
 lock->value--;
 lock->holder = thread_current();
-heap_insert(lock_prec, &thread_current()->held, &lock->helem);
+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 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
+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 starts: we
+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
 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 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"}).
+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
-in the RAG (Resource Allocation Graph), but we can stop whenever there
+in the RAG (Resource Allocation Graph), but we can stop the ``chase'' whenever
-is no change in the @{text cprec}. Befre we start the loop, we
+there is no change in the @{text cprec}. To start the loop, we
-assign in Lines 11 and 12 assign the variable @{ML_text pt} to the owner
+assign in Lines 11 and 12 the variable @{ML_text pt} to the owner
-of the lock, and enter the while-loop in Lines 13 to 24. \ldots
+of the lock, and then enter the while-loop in Lines 13 to 24.
+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.
 *}
 section {* Conclusion *}
 text {*

changeset 13	735e36c64a71
parent 12	85116bc854c0
child 14	1bf194825a4e