pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:65b178574112
+:4a75769a93b5
 @{thm holding_raw_def[where thread="th"]}\\
 @{thm waiting_raw_def[where thread="th"]}
 \end{tabular}
 \end{isabelle}
-\noindent
+\noindent In this definition we assume that @{text "set"} converts a
-In this definition we assume that @{text "set"} converts a list into a set.
+list into a set.  Note that in the first definition the condition
-Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow
+about @{text "th \<in> set (wq cs)"} does not follow from @{text "th
-from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL.
+= hd (set (wq cs))"}, since the head of an empty list is undefined
-At the beginning, that is in the state where no thread is created yet,
+in Isabelle/HOL.  At the beginning, that is in the state where no
-the waiting queue function will be the function that returns the
+thread is created yet, the waiting queue function will be the
-empty list for every resource.
+function that returns the empty list for every resource.
 \begin{isabelle}\ \ \ \ \ %%%
 @{abbrev all_unlocked}\hfill\numbered{allunlocked}
 \end{isabelle}
 \end{center}
 \caption{An instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}
 \end{figure}
 \noindent
-If there is no cycle, then every @{text RAG} can be pictured as a forrest of trees, as
+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
+Because of the @{text RAG}s, we will need to formalise some results
-graphs.  While there are few formalisations for graphs already
+about graphs.  While there are 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
+graphs for PIP. The justification for this is that we wanted to have
-to have a more general theory of graphs which is capable of
+a more general theory of graphs which is capable of representing
-representing potentially infinite graphs (in the sense of infinitely
+potentially infinite graphs (in the sense of infinitely branching
-branching and infinite size): the property that our @{text RAG}s are
+and infinite size): the property that our @{text RAG}s are actually
-actually forrests of finitely branching trees having only an finite
+forests of finitely branching trees having only an finite depth
-depth should be something we can \emph{prove} for our model of
+should be something we can \emph{prove} for our model of PIP---it
-PIP---it should not be an assumption we build already into our
+should not be an assumption we build already into our model. It
-model. It seemed for our purposes the most convenient
+seemed for our purposes the most convenient represeantation of
-represeantation of graphs are binary relations given by sets of
+graphs are binary relations given by sets of pairs shown in
-pairs shown in \eqref{pairs}. The pairs stand for the edges in
+\eqref{pairs}. The pairs stand for the edges in graphs. This
-graphs. This relation-based representation is convenient since we
+relation-based representation has the advantage that the notions
-can use the notions of transitive closure operations @{term "trancl
+@{text "waiting"} and @{text "holiding"} are already defined in
-DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
+terms of relations amongst theads and resources. Also, we can easily
-composition.  A \emph{forrest} is defined in our representation as the relation @{text
+re-use the standard notions for transitive closure operations @{term
-rel} that is \emph{single valued} and \emph{acyclic}:
+"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}:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm single_valued_def[where ?r="rel", THEN eq_reflection]}\\
 @{thm acyclic_def[where ?r="rel", THEN eq_reflection]}
 @{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
 \end{tabular}\\
 \mbox{}\hfill\numbered{children}
 \end{isabelle}
-\noindent Note that forrests can have trees with infinte depth and
+\noindent Note that forests can have trees with infinte depth and
 containing nodes with infinitely many children.  A \emph{finite
-forrest} is a forrest which is well-founded and every node has
+forest} is a forest whose underlying relation is
-finitely many children (is only finitely branching).
+well-founded\footnote{For \emph{well-founded} we use the quite natural
+definition from Isabelle.}
+and every node has finitely many children (is only finitely
+branching).
 %\endnote{
 %\begin{isabelle}\ \ \ \ \ %%%
 %@ {thm rtrancl_path.intros}
 %\end{isabelle}
 \begin{proof}[of Theorem 1] If @{term "th \<in> running (s' @ s)"},
 then there is nothing to show. So let us assume otherwise. Since the
 @{text "RAG"} is well-founded, we know there exists an ancestor of
-@{text "th"} that is the root of the corrsponding subtree and
+@{text "th"} that is the root of the corresponding subtree and
 therefore is ready (it does not request any resources). Let us call
 this thread @{text "th'"}.  Since in PIP the @{term "cpreced"}-value
 of any thread equals the maximum precedence of all threads in its
 @{term "RAG"}-subtree, and @{text "th"} is in the subtree of @{text
 "th'"}, the @{term "cpreced"}-value of @{text "th'"} cannot be lower
 reasons for this: First, we do not specify what ``running the code''
 of a thread means, for example by giving an operational semantics
 for machine instructions. Therefore we cannot characterise what are
 ``good'' programs that contain for every locking request for a
 resource also a corresponding unlocking request.  Second, we need to
-distinghish between a thread that ``just'' locks a resource for a
+distinguish between a thread that ``just'' locks a resource for a
 finite amount of time (even if it is very long) and one that locks
 it forever (there might be an unbounded loop in between the locking and
 unlocking requests).
 Because of these problems, we decided in our earlier paper
 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
 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 dispence with the first assumption altogether and allow that
+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
 after @{term s}. Otherwise our PIP scheduler could be ``swamped''
-with @{text "Create"}-requests.  So our first assumption states:
+with @{text "Create"}-requests from 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
 state @{text s}, in every ``future'' valid state @{text "es @ s"}, we
 require that the number of created threads is less than
 anymore) after a finite number of events in @{text "es @ s"}. Again
 we have to state this bound to hold in all valid states after @{text
 s}. The bound reflects how each thread @{text "th'"} is programmed:
 Though we cannot express what instructions a thread is executing,
 the events in our model correspond to the system calls made by
-a thread. Our @{text "BND(th')"} binds the number of these ``calls''.
+a thread. Our @{text "BND(th')"} bounds the number of these ``calls''.
 The main reason for these two assumptions is that we can prove the
 following: The number of states after @{text s} in which the thread
 @{text th} is not running (that is where Priority Inversion occurs)
 can be bounded by the number of actions the threads in @{text

changeset 199	4a75769a93b5
parent 197	ca4ddf26a7c7
child 200	ff826e28d85c