Journal/Paper.thy
changeset 200 ff826e28d85c
parent 199 4a75769a93b5
child 201 fcc6f4c3c32f
--- 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 "\<equiv>"} & @{thm (rhs) tG_alt_def}\\
-  @{thm (lhs) cp_s_def}  & @{text "\<equiv>"} & @{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.