pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:fe3dbfd9123b
+:5191a09d9928
 how the thread inherited its current priority}'' \cite[Page
 527]{Liu00}. Unfortunately, the important information about actually
 computing the priority to be restored solely from this log is not
 explained in \cite{Liu00} but left as an ``{\it excercise}'' to the
 reader.  As we shall see, a correct version of PIP does not need to
-maintain this (potentially expensive) data structure at
+maintain this (potentially expensive) log data structure at
 all. Surprisingly also the widely read and frequently updated
 textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the
 lock, the [low-priority] thread will revert to its original
 priority.}'' The same error is also repeated later in this popular textbook.
 remaining priority of the threads it blocks. This textbook also
 gives an informal proof for the correctness of PIP in the style of
 Sha et al. Unfortunately, this informal proof is too vague to be
 useful for formalising the correctness of PIP and the specification
 leaves out nearly all details in order to implement PIP
-efficiently.\medskip\smallskip % %The advantage of formalising the
+efficiently.\medskip\smallskip
-%correctness of a high-level specification of PIP in a theorem
-prover %is that such issues clearly show up and cannot be overlooked
-as in %informal reasoning (since we have to analyse all possible
-behaviours %of threads, i.e.~\emph{traces}, that could possibly
-happen).
 \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 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. We
 illustrate this with an implementation of PIP in the educational
-PINTOS operating system \cite{PINTOS}.  For example, we found by
+operating system PINTOS \cite{PINTOS}.  For example, we found by
 ``playing'' with the formalisation that the choice of the next
 thread to take over a lock 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
 \noindent
 If there is no cycle, then every @{text RAG} can be pictured as a forest of trees, as
 for example in Figure~\ref{RAGgraph}.
 Because of the @{text RAG}s, we will need to formalise some results
-about graphs.  While there are a few formalisations for graphs already
+about graphs.
-implemented in Isabelle, we choose to introduce our own library of
+It
-graphs for PIP. The justification for this is that we wanted to have
-a more general theory of graphs which is capable of representing
-potentially infinite graphs (in the sense of infinitely branching
-and infinite size): the property that our @{text RAG}s are actually
-forests of finitely branching trees having only a finite depth
-should be something we can \emph{prove} for our model of PIP---it
-should not be an assumption we build already into our model. It
 seems for our purposes the most convenient representation of
 graphs are binary relations given by sets of pairs shown in
 \eqref{pairs}. The pairs stand for the edges in graphs. This
 relation-based representation has the advantage that the notions
 @{text "waiting"} and @{text "holding"} are already defined in
 terms of relations amongst threads and resources. Also, we can easily
 re-use the standard notions for transitive closure operations @{term
 "trancl DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
-composition for our graphs.  A \emph{forest} is defined in our
+composition for our graphs.
+While there are a few formalisations for graphs already
+implemented in Isabelle, we choose to introduce our own library of
+graphs for PIP. The justification for this is that we wanted to have
+a more general theory of graphs which is capable of representing
+potentially infinite graphs (in the sense of infinitely branching
+and infinite size): the property that our @{text RAG}s are actually
+forests of finitely branching trees having only a finite depth
+should be something we can \emph{prove} for our model of PIP---it
+should not be an assumption we build already into our model.
+A \emph{forest} is defined in our
 representation as the relation @{text rel} that is \emph{single
 valued} and \emph{acyclic}:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \noindent Note that forests can have trees with infinte depth and
 containing nodes with infinitely many children.  A \emph{finite
 forest} is a forest whose underlying relation is
 well-founded\footnote{For \emph{well-founded} we use the quite natural
-definition from Isabelle.}
+definition from Isabelle/HOL.}
 and every node has finitely many children (is only finitely
 branching).
 %\endnote{
 %\begin{isabelle}\ \ \ \ \ %%%
 %}
 %\endnote{{\bf Lemma about overlapping paths}}
-The locking mechanism of PIP ensures that for each thread node,
+The locking mechanism ensures that for each thread node,
 there can be many incoming holding edges in the @{text RAG}, but at most one
 out going waiting edge.  The reason is that when a thread asks for
 a resource that is locked already, then the thread is blocked and
 cannot ask for another resource.  Clearly, also every resource can
 only have at most one outgoing holding edge---indicating that the
 there is a circle of dependencies in a @{text RAG} (and thus @{text TDG}), then clearly we have a
 deadlock. Therefore when a thread requests a resource, we must
 ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the
 programmer has to ensure this. Our model will enforce that critical
 resources can only be requested provided no circularity can arise (but
-they can overlap, see Fig~\ref{overlap}).
+critical sections can overlap, see Fig~\ref{overlap}).
 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
 state @{text s}. It is defined as
 \begin{isabelle}\ \ \ \ \ %%%
 \noindent
 While the precedence @{term prec} of any
 thread is determined statically (for example when the thread is
 created), the point of the current precedence is to dynamically
-increase this precedence, if needed according to PIP. Therefore the
+boost this precedence, if needed according to PIP. Therefore the
 current precedence of @{text th} is given as the maximum of the
 precedences of all threads in its subtree (which includes by definition
 @{text th} itself). Since the notion of current precedence is defined as the
 transitive closure of the dependent
 threads in the @{text TDG}, we deal correctly with the problem in the informal
 \noindent
 The first function is a waiting queue function (that is, it takes a
 resource @{text "cs"} and returns the corresponding list of threads
 that lock or wait for it); the second is a function that
 takes a thread and returns its current precedence (see
-the definition in \eqref{cpreced}). We assume the usual getter and setter methods for
+the @{text wq} in \eqref{cpreced}). We assume the usual getter and setter methods for
 such records.
 In the initial state, the scheduler starts with all resources unlocked (the corresponding
 function is defined in \eqref{allunlocked}) and the
 current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
 The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
 we calculate the waiting queue function of the (previous) state @{text s};
 this waiting queue function @{text wq} is unchanged in the next schedule state---because
 none of these events lock or release any resource;
 for calculating the next @{term "cprec_fun"}, we use @{text wq} and
-@{term cpreced}. This gives the following three clauses for @{term schs}:
+@{term cpreced} defined above. This gives the following three clauses for @{term schs}:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\
 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
 @{text "s' @ s"}) in which @{text th} is still alive, either @{text
 th} is running or it is blocked by a thread that was alive in the
 state @{text s} and was waiting for or in the possession of a lock
 in @{text s}. Since in @{text s}, as in every state, the set of
 alive threads is finite, @{text th} can only be blocked by a finite
-number of threads.  We will actually prove a
+number of threads.
-stronger statement where we also provide the current precedence of
-the blocking thread.
 However, the theorem we are going to prove hinges upon a number of
 natural assumptions about the states @{text s} and @{text "s' @ s"}, the
 thread @{text th} and the events happening in @{text s'}. We list
 them next:
 %@{thm "th_blockedE_pretty"} -- thm-blockedE??
 %
 % @{text "th_kept"} shows that th is a thread in s'-s
 % }
-Given our assumptions (on @{text th}), the first property we show
+The next lemma is part of the proof for Theorem~1:
+Given our assumptions (on~@{text th}), the first property we show
 that a running thread @{text "th'"} must either wait for or hold a
 resource in state @{text s}.
 \begin{lemma}\label{notdetached}
 If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}.
 \end{lemma}
 \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state
 @{text "s"}, then, according to the definition of detached, @{text
 "th'"} does not hold or wait for any resource. Hence the @{text
-cp}-value of @{text "th'"} in @{text s} is not boosted, that is
+cprec}-value of @{text "th'"} in @{text s} is not boosted, that is
 @{term "cp s th' = prec th' s"}, and is therefore lower than the
-precedence (as well as the @{text "cp"}-value) of @{term "th"}. This
+precedence (as well as the @{text "cprec"}-value) of @{term "th"}. This
 means @{text "th'"} will not run as long as @{text "th"} is a live
 thread. In turn this means @{text "th'"} cannot take any action in
 state @{text "s' @ s"} to change its current status; therefore
 @{text "th'"} is still detached in state @{text "s' @ s"}.
 Consequently @{text "th'"} is also not boosted in state @{text "s' @
 (active or hibernating) and second, each of these threads will give up its
 resources after a finite amount of time.  However, we do not have
 this concept of active or hibernating threads in our model.  In fact
 we can dispense with the first assumption altogether and allow that
 in our model we can create new threads or exit existing threads
-arbitrarily. Consequently, the avoidance of indefinite priority
+arbitrarily. Consequently, the absence of indefinite priority
-inversion we are trying to establish is in our model not true,
+inversion we are trying to establish in our model is not true,
 unless we stipulate an upper bound on the number of threads that
 have been created during the time leading to any future state after
 @{term s}. Otherwise our PIP scheduler could be ``swamped'' with
 @{text "Create"}-requests of lower priority threads.  So our first
 assumption states:
 \noindent Note that it is not enough to just to state that there are
 only finite number of threads created up until a single state @{text
 "s' @ s"} after @{text s}.  Instead, we need to put this bound on
 the @{text "Create"} events for all valid states after @{text s}.
 This ensures that no matter which ``future'' state is reached, the
-number of @{text "Create"}-events is finite. We use @{text "es @ s"}
+number of @{text "Create"}-events is finite. This bound @{text BC} is assumed
-to stand for \emph{future states} after @{text s}---it is @{text s}
+with respect to all future states @{text "es @ s"}
-extended with some list @{text es} of events.
+of @{text s}, not just a single one.
 For our second assumption about giving up resources after a finite
 amount of ``time'', let us introduce the following definition about
 threads that can potentially block @{text th}:
 \noindent This set contains all threads that are not detached in
 state @{text s}. According to our definiton of @{text "detached"},
 this means a thread in @{text "blockers"} either holds or waits for
 some resource in state @{text s} . Our Thm.~1 implies that any of
-those threads can all potentially block @{text th} after state
+such threads can all potentially block @{text th} after state
 @{text s}. We need to make the following assumption about the
 threads in the @{text "blockers"}-set:
 \begin{quote}
 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:}
 & & +\;
 @{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
 \end{array}
 \end{equation}
-\noindent Second by Thm~\ref{mainthm}, the events are either the
+\noindent
-actions of @{text th} or @{text "Create"}-events or actions of the
+The actions in @{text es} can be partitioned into the actions of @{text th} and the
-threads in blockers. That is
+actions of threads other than @{text th}. The latter can further be divided
+into actions of existing threads and the actions to create new
+ones. Moreover, the actions of existing threads other than @{text th}
+are by Thm 1 the actions of blockers. This gives rise to
 %
 \begin{equation}\label{secondeq}
 \begin{array}{lcl}
 @{text "len es"} & \;=\; & @{text "len (actions_of {th} es)"}\\
 & & +\; @{text "len (filter isCreate es)"}\\
 precedence is computed in this more efficient manner, the selection
 of the thread with highest precedence from a set of ready threads is
 a standard scheduling operation and implemented in most operating
 systems.
-%\begin{proof}[of Lemma~\ref{childrenlem}]
+Below we
-%Test
+outline how our formalisation guides the efficient calculation of @{text cprecs}
-%\end{proof}
+in response to each kind of events.\smallskip
-Of course the main work for implementing PIP involves the
-scheduler and coding how it should react to events.  Below we
-outline how our formalisation guides this implementation for each
-kind of events.\smallskip
 *}
 text {*
 \noindent
 \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and
 not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
 can show
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "If"} @{text "th'' \<noteq> th"} and
-@{text "th'' \<noteq> th'"}
+@{text "th'' \<noteq> th'"} \;\;@{text then}\;\;
 @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]}
 \hfill\numbered{fone}
 \end{isabelle}
 \noindent
 \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 ancestors of @{text "th"} are unchanged. For the ancestors of
+not ancestors of @{text "th"} (in the new @{text RAG} or @{text TDG}) are unchanged. For the ancestors of
 @{text th} we need
 to follow the edges in the @{text TDG} and recompute the @{term
 "cprecs"}. Whereas in all other event we might have to make
 modifications to the @{text "RAG"}, no recalculation of @{text
 cprec} depends on the @{text RAG}. This is the only case where
 taken'', or 1 for being ``free''). In case the lock is taken, we enter the
 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).
 Thus we established two pointers: one in the waiting queue of the lock pointing to the
-current thread, and the other from the currend thread pointing to the lock.
+current thread, and the other from the current 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 ancestor threads
 in the @{text RAG} and update their
 current precedence; however we only have to do this as long as there is change in the
 current precedence.

changeset 204	5191a09d9928
parent 203	fe3dbfd9123b
child 205	12a8dfcb55a7