regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:d47c2143ab8a
+:7fe2a20017c0
 (*<*)
 theory Paper
 imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
 begin
+(*
+find_unused_assms CpsG
+find_unused_assms ExtGG
+find_unused_assms Moment
+find_unused_assms Precedence_ord
+find_unused_assms PrioG
+find_unused_assms PrioGDef
+*)
 ML {*
 open Printer;
 show_question_marks_default := false;
 *}
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_depend_def}
 \end{isabelle}
 \noindent
-Given three threads and three resources, an instance of a RAG can be pictured
+Given four threads and three resources, an instance of a RAG can be pictured
 as follows:
 \begin{center}
 \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
 \begin{tikzpicture}[scale=1]
 @{thm (lhs) cp_def}        & @{text "\<equiv>"} & @{thm (rhs) cp_def}
 \end{tabular}
 \end{isabelle}
 \noindent
-With these abbreviations we can introduce
+With these abbreviations in place we can introduce
 the notion of threads being @{term readys} in a state (i.e.~threads
 that do not wait for any resource) and the running thread.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 only one lock, can cause indefinite Priority Inversion for one of the
 high-priority threads, invalidating their two bounds.
 Even when fixed, their proof idea does not seem to go through for
 us, because of the way we have set up our formal model of PIP.  One
-reason is that we allow that critical sections can intersect
+reason is that we allow critical sections to intersect
 (something Sha et al.~explicitly exclude).  Therefore we have
 designed a different correctness criterion for PIP. The idea behind
 our criterion is as follows: for all states @{text s}, we know the
 corresponding thread @{text th} with the highest precedence; we show
 that in every future state (denoted by @{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 in
+blocked by a thread that was alive in the state @{text s} and was waiting
-the possession of a lock in @{text s}. Since in @{text s}, as in
+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 a finite number of times. This is independent of how many
 threads of lower priority are created in @{text "s'"}. We will actually prove a
 stronger statement where we also provide the current precedence of
 the blocking thread. However, this correctness criterion hinges upon
 current precedence unchanged. For the others we have to recalculate the current
 precedence. To do this we can start from @{term "th"}
 and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
 the @{term "cp"} of every
 thread encountered on the way. Since the @{term "depend"}
-is loop free, this procedure will always stop. The following two lemmas show, however,
+is assumed to be loop free, this procedure will always stop. The following two lemmas show, however,
 that this procedure can actually stop often earlier without having to consider all
 dependants.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}

changeset 335	7fe2a20017c0
parent 333	813e7257c7c3
child 336	f9e0d3274c14