regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:41da10da16a5
+:c62db88ab197
 (*<*)
 context extend_highest_gen
 begin
 (*>*)
 text {*
-Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
+Sha et al.~state their first correctness criterion for PIP in terms
-for PIP in terms of the number of critical resources: if there are
+of the number of low-priority threads \cite[Theorem 3]{Sha90}: if
+there are @{text n} low-priority threads, then a blocked job with
+high priority can only be blocked @{text n} times.
+Their second correctness criterion is stated
+in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are
 @{text m} critical resources, then a blocked job with high priority
-can only be blocked @{text m} times---that is a \emph{bounded}
+can only be blocked @{text m} times. Both results on their own, strictly speaking, do
-number of times. This result on its own, strictly speaking, does
 \emph{not} prevent indefinite, or unbounded, Priority Inversion,
-because if one low-priority thread does not give up its critical
+because if a low-priority thread does not give up its critical
 resource (the one the high-priority thread is waiting for), then the
 high-priority thread can never run.  The argument of Sha et al.~is
 that \emph{if} threads release locked resources in a finite amount
 of time, then indefinite Priority Inversion cannot occur---the high-priority
 thread is guaranteed to run eventually. The assumption is that
 programmers always ensure that this is the case.  However, even
-taking this assumption into account, ther correctness property is
+taking this assumption into account, their correctness properties are
 \emph{not} true for their version of PIP. As Yodaiken
 \cite{Yodaiken02} pointed out: If a low-priority thread possesses
 locks to two resources for which two high-priority threads are
 waiting for, then lowering the priority prematurely after giving up
 only one lock, can cause indefinite Priority Inversion for one of the
-high-priority threads, invalidating their bound.
+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.  The
 reason is that we allow that critical sections can intersect
 (something Sha et al.~explicitly exclude).  Therefore we have a
 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}. Since in @{text s}, as in every state, the set of alive
+@{text s} and was 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. We will actually prove a stricter bound below. However, this
+times. We will actually prove astronger statement where we also provide
+the current precedence of the blocking thread. However, 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:
 \begin{quote}
 \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
-@{text "th' \<in> threads s"}.
+@{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and
+@{term "cp (s' @ s) th' = prec th s"}.
 \end{theorem}
 \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
+existed in @{text s} and requested or had a lock on at least
-finitely many threads. Like in the argument by Sha et al.~this
+one resource---that means the thread was not \emph{detached} in @{text s}.
+As we shall see shortly, that means there are only finitely
+many threads that can block @{text th} and then need to run
+with the same current precedence as @{text th}.
+Like in the argument by Sha et al.~our
 finite bound does not guarantee absence of indefinite Priority
 Inversion. For this we further have to assume that every thread
 gives up its resources after a finite amount of time. We found that
 this assumption is awkward to formalise in our model. Therefore we
 leave it out and let the programmer assume the responsibility to
 program threads in such a benign manner (in addition to causeing no
 circularity in the @{text RAG}). In this detail, we do not
 make any progress in comparison with the work by Sha et al.
+However, we are able to combine their two separate bounds into a
+single theorem.
 In what follows we will describe properties of PIP that allow us to prove
 Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
 It is relatively easily to see that
 The acyclicity property follow from how we restricted the events in
 @{text step}; similarly the finiteness and well-foundedness property.
 The last two properties establish that every thread in a @{text "RAG"}
 (either holding or waiting for a resource) is a live thread.
-To state the key lemma in our proof, it will be convenient to introduce the notion
+The key lemma in our proof of Theorem~\ref{mainthm} is as follows:
-of a \emph{detached} thread in a state, that is one which does not hold any
-critical resource nor requests one.
 \begin{lemma}\label{mainlem}
 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> treads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
 Since @{text "th'"} is not able to run at state @{text "s' @ s"}, it is not able to
 issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
 one step further, @{text "th'"} still cannot hold any resource. The situation will
 not change in further extensions as long as @{text "th"} holds the highest precedence.
-From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that
+From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be
+blocked by a thread @{text th'} that
 held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
 that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the
 precedence of @{text th} in @{text "s"}.
-\begin{theorem}
-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)"}, @{text "th' \<noteq> th"}, then
-@{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and
-@{term "cp (s' @ s) th' = prec th s"}.
-\end{theorem}
-\noindent
 We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
 This theorem gives a stricter bound on the processes that can block @{text th}:
 only threads that were alive in state @{text s} and moreover held a resource.
-Finally, the theorem establishes that the blocking threads have the
+This means our bound is in terms of both---alive threads in state @{text s}
+and number of critical resources. Finally, the theorem establishes that the blocking threads have the
 current precedence raised to the precedence of @{text th}.
-We can furthermore prove that no deadlock exists in the state @{text "s' @ s"}
+We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"}
 by showing that @{text "running (s' @ s)"} is not empty.
 \begin{lemma}
 Given the assumptions about states @{text "s"} and @{text "s' @ s"},
 the thread @{text th} and the events in @{text "s'"},
 know whether this includes also code for proofs).  Our formalisation
 consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
 code with a few apply-scripts interspersed. The formal model of PIP
 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
 definitions and proofs took 770 lines of code. The properties relevant
-for an implementation took 2000 lines.  %%Our code can be downloaded from
+for an implementation took 2000 lines. The code of our formalisation
-%%...
+can be downloaded from\\
+\url{http://www.dcs.kcl.ac.uk/staff/urbanc/pip.html}.
 \bibliographystyle{plain}
 \bibliography{root}
 *}

changeset 329	c62db88ab197
parent 328	41da10da16a5
child 331	c5442db6a5cb