pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:4a75769a93b5
+:ff826e28d85c
 \emph{Priority Inversion}. Suppose three threads having priorities
 $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
 $H$ blocks any other thread with lower priority and the thread
 itself cannot be blocked indefinitely by threads with lower
 priority. Alas, in a naive implementation of resource locking and
-priorities this property can be violated. For this let $L$ be in the
+priorities, this property can be violated. For this let $L$ be in the
 possession of a lock for a resource that $H$ also needs. $H$ must
 therefore wait for $L$ to exit the critical section and release this
 lock. The problem is that $L$ might in turn be blocked by any thread
 with priority $M$, and so $H$ sits there potentially waiting
 indefinitely (consider the case where threads with propority $M$
 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.
-While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only
+While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are
-formal publications we have found that specify the incorrect
+the only formal publications we have found that specify the
-behaviour, it seems also many informal descriptions of PIP overlook
+incorrect behaviour, it seems also many informal descriptions of the
-the possibility that another high-priority might wait for a
+PIP protocol overlook the possibility that another high-priority
-low-priority process to finish.  A notable exception is the texbook
+process might wait for a low-priority process to finish.  A notable
-\cite{buttazzo}, which gives the correct behaviour of resetting the
+exception is the texbook \cite{buttazzo}, which gives the correct
-priority of a thread to the highest remaining priority of the
+behaviour of resetting the priority of a thread to the highest
-threads it blocks. This textbook also gives an informal proof for
+remaining priority of the threads it blocks. This textbook also
-the correctness of PIP in the style of Sha et al. Unfortunately,
+gives an informal proof for the correctness of PIP in the style of
-this informal proof is too vague to be useful for formalising the
+Sha et al. Unfortunately, this informal proof is too vague to be
-correctness of PIP and the specification leaves out nearly all
+useful for formalising the correctness of PIP and the specification
-details in order to implement PIP efficiently.\medskip\smallskip
+leaves out nearly all details in order to implement PIP
-%
+efficiently.\medskip\smallskip % %The advantage of formalising the
-%The advantage of formalising the
+%correctness of a high-level specification of PIP in a theorem
-%correctness of a high-level specification of PIP in a theorem prover
+prover %is that such issues clearly show up and cannot be overlooked
-%is that such issues clearly show up and cannot be overlooked as in
+as in %informal reasoning (since we have to analyse all possible
-%informal reasoning (since we have to analyse all possible behaviours
+behaviours %of threads, i.e.~\emph{traces}, that could possibly
-%of threads, i.e.~\emph{traces}, that could possibly happen).
+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 do in case two threads have the same priority), but according to precedences.
 Precedences allow us to always discriminate between two threads with equal priority by
 taking into account the time when the priority was last set. We order precedences so
 that threads with the same priority get a higher precedence if their priority has been
 set earlier, since for such threads it is more urgent to finish their work. In an implementation
-this choice would translate to a quite natural FIFO-scheduling of threads with
+this choice would translate to a quite straightforward FIFO-scheduling of threads with
 the same priority.
 Moylan et al.~\cite{deinheritance} considered the alternative of
 ``time-slicing'' threads with equal priority, but found that it does not lead to
 advantages in practice. On the contrary, according to their work having a policy
 \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 few formalisations for graphs already
+about 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 an finite depth
+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
-seemed for our purposes the most convenient represeantation of
+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 "holiding"} are already defined in
+@{text "waiting"} and @{text "holding"} are already defined in
-terms of relations amongst theads and resources. Also, we can easily
+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
 representation as the relation @{text rel} that is \emph{single
 valued} and \emph{acyclic}:
 %\endnote{{\bf Lemma about overlapping paths}}
 The locking mechanism of PIP 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
-resource that is locked already, then the thread is blocked and
+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
 resource is locked. So if the @{text "RAG"} is well-founded and
 finite, we can always start at a thread waiting for a resource and
 ``chase'' outgoing arrows leading to a single root of a tree,
 @{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
 algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
 lowered prematurely (see Introduction). We again introduce an abbreviation for current
-precedeces of a set of threads, written @{text "cprecs wq s ths"}.
+precedences of a set of threads, written @{text "cprecs wq s ths"}.
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cpreceds_def}
 \end{isabelle}
 \end{isabelle}
 \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, respectively wait for, it); the second is a function that
+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
 such records.
 In the initial state, the scheduler starts with all resources unlocked (the corresponding
 about @{text TDG}s and @{term cprec}, which are more convenient to use in
 subsequent proofs.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}rcl}
-@{thm (lhs) tG_alt_def}  & @{text "\<equiv>"} & @{thm (rhs) tG_alt_def}\\
+@{thm (lhs) tG_alt_def}  & @{text "="} & @{thm (rhs) tG_alt_def}\\
-@{thm (lhs) cp_s_def}  & @{text "\<equiv>"} & @{thm (rhs) cp_s_def}\\
+@{thm (lhs) cp_s_def}  & @{text "="} & @{thm (rhs) cp_s_def}\\
 \end{tabular}\\
 \mbox{}\hfill\numbered{overloaded}
 \end{isabelle}
 \noindent Next we can introduce
 \noindent This is because the @{text Set} event is for a thread to change
 its \emph{own} priority---therefore it must be running.
 If a thread wants to lock a resource, then the thread
 needs to be running and also we have to make sure that the resource
-lock does not lead to a cycle in the RAG (the prurpose of the second
+lock does not lead to a cycle in the RAG (the purpose of the second
 premise in the rule below). In practice, ensuring the latter is the
 responsibility of the programmer.  In our formal model we brush
 aside these problematic cases in order to be able to make some
 meaningful statements about PIP.\footnote{This situation is similar
 to the infamous \emph{occurs check} in Prolog: In order to say
 What we will establish in this section is that there can only be a
 finite number of states after state @{term s} in which the thread
 @{term th} is blocked (recall for this that a state is a list of
 events).  For this finiteness bound to exist, Sha et al.~informally
 make two assumptions: first, there is a finite pool of threads
-(active or hibernating) and second, each of them giving up its
+(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
 inversion we are trying to establish is in our model 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
+have been created during the time leading to any future state after
-after @{term s}. Otherwise our PIP scheduler could be ``swamped''
+@{term s}. Otherwise our PIP scheduler could be ``swamped'' with
-with @{text "Create"}-requests from of lower priority threads.
+@{text "Create"}-requests of lower priority threads.  So our first
-So our first assumption states:
+assumption states:
 \begin{quote} {\bf Assumption on the number of threads created
 after the state {\boldmath@{text s}}:} Given the
 state @{text s}, in every ``future'' valid state @{text "es @ s"}, we
 require that the number of created threads is less than
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm blockers_def[THEN eq_reflection]}
 \end{isabelle}
-\noindent This set contains all treads that are not detached in
+\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 Them~1 implies that any of
+some resource in state @{text s} . Our Thm.~1 implies that any of
 those 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}
 While our formalised proof gives us confidence about the correctness of our model of PIP,
 we found that the formalisation can even help us with efficiently implementing it.
 For example Baker complained that calculating the current precedence
 in PIP is quite ``heavy weight'' in Linux (see the Introduction).
 In our model of PIP the current precedence of a thread in a state @{text s}
-depends on the precedenes of all threads in its subtree---a ``global'' transitive notion,
+depends on the precedences of all threads in its subtree---a ``global'' transitive notion,
 which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}).
 We can however improve upon this. For this recall the notion
 of @{term children} of a thread @{text th} defined in \eqref{children}.
 There a child is a thread that is only one ``hop'' away from the thread
 @{text th} in the @{term TDG} (and waiting for @{text th} to release
 \noindent
 That means the current precedence of a thread @{text th} can be
 computed by considering the static precedence of @{text th}
 and
 the current precedences of the children of @{text th}. Their
-@{text "cprec"}s, in general general, need to be computed by recursively decending into
+@{text "cprec"}s, in general, need to be computed by recursively decending into
 deeper ``levels'' of the @{text TDG}.
 However, the current precedence of a thread @{text th}, say,
 only needs to be recomputed when @{text "(i)"} its static
 precedence is re-set or when @{text "(ii)"} one of
 its children changes its current precedence or when @{text "(iii)"} the children set changes
-(for example in an @{text "V"}-event).
+(for example in a @{text "V"}-event).
 If only the static precedence or the children-set changes, then we can
 avoid the recursion and compute the @{text cprec} of @{text th} locally.
 In such cases
-the recursion does not need to decend into the corresponding subtree.
+the recursion does not need to descend into the corresponding subtree.
 Once the current
 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.
 *}
 text {*
 \noindent
 In the other case where there is no thread that takes over @{text cs},
-we can show how
+we can prove that the updated @{text RAG} merely deletes the relevant edge and
-to recalculate the @{text RAG} and also show that no current precedence needs
+that no current precedence needs to be recalculated
-to be recalculated for any thread @{text "th''"}.
+for any thread @{text "th''"}.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (concl) valid_trace_v_e.RAG_s}\\
 @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"}
 \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
+Lines 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
 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 inserting the current thread into the waiting queue of this lock (Line 9).
 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, thought this specification does not contain
+that their C-code satisfies its specification, though this specification does not contain
 anything about PIP \cite{sel4}.
-Our verification of PIP however provided us with the justification for designing
+Our verification of PIP however provided us with (formally proven) insights on how to design
 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.
 *}

changeset 200	ff826e28d85c
parent 199	4a75769a93b5
child 201	fcc6f4c3c32f