diff -r 4a75769a93b5 -r ff826e28d85c Journal/Paper.thy --- a/Journal/Paper.thy Mon Dec 18 14:52:48 2017 +0000 +++ b/Journal/Paper.thy Tue Dec 19 14:20:29 2017 +0000 @@ -79,7 +79,7 @@ $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 @@ -218,24 +218,24 @@ priority.}'' The same error is also repeated later in this popular textbook. - While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only - formal publications we have found that specify the incorrect - behaviour, it seems also many informal descriptions of PIP overlook - the possibility that another high-priority might wait for a - low-priority process to finish. A notable exception is the texbook - \cite{buttazzo}, which gives the correct behaviour of resetting the - priority of a thread to the highest 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 - %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). + While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are + the only formal publications we have found that specify the + incorrect behaviour, it seems also many informal descriptions of the + PIP protocol overlook the possibility that another high-priority + process might wait for a low-priority process to finish. A notable + exception is the texbook \cite{buttazzo}, which gives the correct + behaviour of resetting the priority of a thread to the highest + 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 + %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 @@ -452,7 +452,7 @@ 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 @@ -567,21 +567,21 @@ 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 - terms of relations amongst theads and resources. Also, we can easily + @{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 @@ -632,7 +632,7 @@ 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 @@ -684,7 +684,7 @@ 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} @@ -702,7 +702,7 @@ \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. @@ -822,8 +822,8 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}rcl} - @{thm (lhs) tG_alt_def} & @{text "\"} & @{thm (rhs) tG_alt_def}\\ - @{thm (lhs) cp_s_def} & @{text "\"} & @{thm (rhs) cp_s_def}\\ + @{thm (lhs) tG_alt_def} & @{text "="} & @{thm (rhs) tG_alt_def}\\ + @{thm (lhs) cp_s_def} & @{text "="} & @{thm (rhs) cp_s_def}\\ \end{tabular}\\ \mbox{}\hfill\numbered{overloaded} \end{isabelle} @@ -896,7 +896,7 @@ 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 @@ -1641,7 +1641,7 @@ @{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 @@ -1649,10 +1649,10 @@ 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 - after @{term s}. Otherwise our PIP scheduler could be ``swamped'' - with @{text "Create"}-requests from of lower priority threads. -So our first assumption states: + 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: \begin{quote} {\bf Assumption on the number of threads created after the state {\boldmath@{text s}}:} Given the @@ -1682,10 +1682,10 @@ @{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: @@ -1849,7 +1849,7 @@ 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}. @@ -1871,17 +1871,17 @@ 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 @@ -2044,9 +2044,9 @@ text {* \noindent In the other case where there is no thread that takes over @{text cs}, - we can show how - to recalculate the @{text RAG} and also show that no current precedence needs - to be recalculated for any thread @{text "th''"}. + we can prove that the updated @{text RAG} merely deletes the relevant edge and + that no current precedence needs to be recalculated + for any thread @{text "th''"}. \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -2235,7 +2235,7 @@ \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 @@ -2279,9 +2279,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.