regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:e44c4055d430
+:4d93486cb302
 checking techniques. This paper presents a formalised and
 mechanically checked proof for the correctness of PIP (to our
 knowledge the first one; the earlier informal proof by Sha et
 al.~\cite{Sha90} is flawed).  In contrast to model checking, our
 formalisation provides insight into why PIP is correct and allows us
-to prove stronger properties that, as we will show, inform an
+to prove stronger properties that, as we will show, can inform an
 implementation.  For example, we found by ``playing'' with the formalisation
 that the choice of the next thread to take over a lock when a
 resource is released is irrelevant for PIP being correct. Something
 which has not been mentioned in the relevant literature.
 *}
 \noindent
 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. In practice, ensuring the latter is
 of course the responsibility of the programmer.  In our formal
-model we just exclude such problematic cases in order to make
+model we just exclude such problematic cases in order to be able to make
 some meaningful statements about PIP.\footnote{This situation is
-similar to the infamous occurs check in Prolog: in order to say
+similar to the infamous occurs check in Prolog: In order to say
 anything meaningful about unification, one needs to perform an occurs
-check, but in practice the occurs check is ommited and the
+check. But in practice the occurs check is ommited and the
 responsibility for avoiding problems rests with the programmer.}
 \begin{center}
 @{thm[mode=Rule] thread_P[where thread=th]}
 \end{center}
 \noindent
 This completes our formal model of PIP. In the next section we present
 properties that show our model of PIP is correct.
 *}
-section {* Correctness Proof *}
+section {* The Correctness Proof *}
 (*<*)
 context extend_highest_gen
 begin
 print_locale extend_highest_gen
 thm extend_highest_gen_def
 thm extend_highest_gen_axioms_def
 thm highest_gen_def
 (*>*)
 text {*
-Sha et al.~\cite{Sha90} state their correctness criterion of PIP in terms
+Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion for PIP in terms
 of the number of critical resources: if there are @{text m} critical
 resources, then a blocked job can only be blocked @{text m} times---that is
 a bounded number of times.
 For their version of PIP, this property is \emph{not} true (as pointed out by
 Yodaiken \cite{Yodaiken02}) as a high-priority thread can be
 blocked an unbounded number of times by creating medium-priority
-threads that block a thread locking a critical resource and having
+threads that block a thread, which in turn locks a critical resource and has
-a too low priority. In the way we have set up our formal model of PIP,
+too low priority to make progress. In the way we have set up our formal model of PIP,
 their proof idea, even when fixed, does not seem to go through.
 The idea behind our correctness criterion of PIP 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 active, either @{text th} is running or it is blocked by a
+@{text th} is still alive, either @{text th} is running or it is blocked by a
-thread that was active in the state @{text s}. Since in @{text s}, as in every
+thread that was alive in the state @{text s}. Since in @{text s}, as in every
-state, the set of active threads is finite, @{text th} can only be blocked a
+state, the set of alive threads is finite, @{text th} can only be blocked a
-finite number of times. We will actually prove a stricter bound. However,
+finite number of times. We will actually prove a stricter bound below. However,
-this correctness criterion hinges on a number of assumptions about the states
+this correctness criterion hinges upon a number of assumptions about the states
 @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening
-in @{text s'}. We list them next.
+in @{text s'}. We list them next:
 \begin{quote}
 {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make
 any meaningful statement, we need to require that @{text "s"} and
 @{text "s' @ s"} are valid states, namely
 \end{tabular}
 \end{isabelle}
 \end{quote}
 \begin{quote}
-{\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be active in @{text s} and
+{\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and
-has the highest precedence of all active threads in @{text s}. Furthermore the
+has the highest precedence of all alive threads in @{text s}. Furthermore the
-priority of @{text th} is @{text prio}.
+priority of @{text th} is @{text prio} (we need this in the next assumptions).
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{l}
 @{term "th \<in> threads s"}\\
 @{term "prec th s = Max (cprec s ` threads s)"}\\
 @{term "prec th s = (prio, DUMMY)"}
 \begin{quote}
 {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
 be blocked indefinitely. Of course this can happen if threads with higher priority
 than @{text th} are continously created in @{text s'}. Therefore we have to assume that
 events in @{text s'} can only create (respectively set) threads with equal or lower
-priority than @{text prio} of the thread @{text th}. We also have to assume that @{text th} does
+priority than @{text prio} of @{text th}. We also need to assume that the
-not get ``exited'' in @{text "s'"}.
+priority of @{text "th"} does not get reset and also that @{text th} does
+not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{l}
-{If}~~@{text "Create _ prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
+{If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
 {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
 {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
 \end{tabular}
 \end{isabelle}
 \end{quote}
 \noindent
-Under these assumptions we will prove the following property:
+Under these assumptions we will prove the following correctness property:
 \begin{theorem}\label{mainthm}
 Given the assumptions about states @{text "s"} and @{text "s' @ s"},
 the thread @{text th} and the events in @{text "s'"},
 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
 \noindent
 This theorem ensures that the thread @{text th}, which has the highest
 precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"}
 by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,
 that means by only finitely many threads. Consequently, indefinite wait of
-@{text th}---whcih is Priority Inversion---cannot occur.
+@{text th}---which would be Priority Inversion---cannot occur.
 In what follows we will describe properties of PIP that allow us to prove
 Theorem~\ref{mainthm}. It is relatively easily to see that
 \begin{isabelle}\ \ \ \ \ %%%
 \end{tabular}
 \end{isabelle}
 \noindent
 The first one states that every waiting thread can only wait for a single
-resource (because it gets suspended after requesting that resource), and
+resource (because it gets suspended after requesting that resource and having
-the second that every resource can only be held by a single thread. The
+to wait for it); the second that every resource can only be held by a single thread;
-third property establishes that in every given valid state, there is
+the third property establishes that in every given valid state, there is
-at most one running thread.
+at most one running thread. We can also show the following properties
+about the RAG in @{text "s"}.
+\begin{isabelle}\ \ \ \ \ %%%
+\begin{tabular}{@ {}l}
+%@{thm[mode=IfThen] }\\
+%@{thm[mode=IfThen] }\\
+%@{thm[mode=IfThen] }
+\end{tabular}
+\end{isabelle}
 TODO
 \noindent
 The following lemmas show how RAG is changed with the execution of events:

changeset 310	4d93486cb302
parent 309	e44c4055d430
child 311	23632f329e10