pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:b6ea51cd2e88
+:c0a4e840aefe
 (*<*)
 context extend_highest_gen
 begin
 (*>*)
 text {*
 Sha et al.~state their first correctness criterion for PIP in terms
 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 a maximum of @{text n} times.
-Their second correctness criterion is given
+Their second correctness criterion is given in terms of the number
-in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are
+of critical resources \cite[Theorem 6]{Sha90}: if there are @{text
-@{text m} critical resources, then a blocked job with high priority
+m} critical resources, then a blocked job with high priority can
-can only be blocked a maximum of @{text m} times. Both results on their own, strictly speaking, do
+only be blocked a maximum of @{text m} times. Both results on their
-\emph{not} prevent indefinite, or unbounded, Priority Inversion,
+own, strictly speaking, do \emph{not} prevent indefinite, or
-because if a low-priority thread does not give up its critical
+unbounded, Priority Inversion, because if a low-priority thread does
-resource (the one the high-priority thread is waiting for), then the
+not give up its critical resource (the one the high-priority thread
-high-priority thread can never run.  The argument of Sha et al.~is
+is waiting for), then the high-priority thread can never run.  The
-that \emph{if} threads release locked resources in a finite amount
+argument of Sha et al.~is that \emph{if} threads release locked
-of time, then indefinite Priority Inversion cannot occur---the high-priority
+resources in a finite amount of time, then indefinite Priority
-thread is guaranteed to run eventually. The assumption is that
+Inversion cannot occur---the high-priority thread is guaranteed to
-programmers must ensure that threads are programmed in this way.  However, even
+run eventually. The assumption is that programmers must ensure that
-taking this assumption into account, the correctness properties of
+threads are programmed in this way.  However, even taking this
-Sha et al.~are
+assumption into account, the correctness properties of Sha et
-\emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken
+al.~are \emph{not} true for their version of PIP---despite being
-\cite{Yodaiken02} and Moylan et al.~\cite{deinheritance} pointed out: If a low-priority thread possesses
+``proved''. As Yodaiken \cite{Yodaiken02} and Moylan et
-locks to two resources for which two high-priority threads are
+al.~\cite{deinheritance} pointed out: If a low-priority thread
-waiting for, then lowering the priority prematurely after giving up
+possesses locks to two resources for which two high-priority threads
-only one lock, can cause indefinite Priority Inversion for one of the
+are waiting for, then lowering the priority prematurely after giving
-high-priority threads, invalidating their two bounds.
+up 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 critical sections, which start with a @{text P}-event
+reason is that we allow critical sections, which start with a @{text
-and finish with a corresponding @{text V}-event, to arbitrarily overlap
+P}-event and finish with a corresponding @{text V}-event, to
-(something Sha et al.~explicitly exclude).  Therefore we have
+arbitrarily overlap (something Sha et al.~explicitly exclude).
-designed a different correctness criterion for PIP. The idea behind
+Therefore we have designed a different correctness criterion for
-our criterion is as follows: for all states @{text s}, we know the
+PIP. The idea behind our criterion is as follows: for all states
-corresponding thread @{text th} with the highest precedence; we show
+@{text s}, we know the corresponding thread @{text th} with the
-that in every future state (denoted by @{text "s' @ s"}) in which
+highest precedence; we show that in every future state (denoted by
-@{text th} is still alive, either @{text th} is running or it is
+@{text "s' @ s"}) in which @{text th} is still alive, either @{text
-blocked by a thread that was alive in the state @{text s} and was waiting
+th} is running or it is blocked by a thread that was alive in the
-for or in the possession of a lock in @{text s}. Since in @{text s}, as in
+state @{text s} and was waiting for or in the possession of a lock
-every state, the set of alive threads is finite, @{text th} can only
+in @{text s}. Since in @{text s}, as in every state, the set of
-be blocked a finite number of times. This is independent of how many
+alive threads is finite, @{text th} can only be blocked a finite
-threads of lower priority are created in @{text "s'"}. We will actually prove a
+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
+the blocking thread.
-a number of assumptions about the states @{text s} and @{text "s' @
-s"}, the thread @{text th} and the events happening in @{text
+However, this correctness criterion hinges upon a number of
-s'}. We list them next:
+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}
 {\bf Assumptions on the states {\boldmath@{text s}} and
 {\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and
 @{text "s' @ s"} are valid states:
 {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
 \end{tabular}
 \end{isabelle}
 \end{quote}
-\noindent
+\noindent The locale mechanism of Isabelle helps us to manage
-The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}.
+conveniently such assumptions~\cite{Haftmann08}.  Under these
-Under these assumptions we shall prove the following correctness property:
+assumptions we shall 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
 @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and
 @{term "cp (s' @ s) th' = prec th s"}.
 \end{theorem}
-\noindent
+\noindent This theorem ensures that the thread @{text th}, which has
-This theorem ensures that the thread @{text th}, which has the
+the highest precedence in the state @{text s}, can only be blocked
-highest precedence in the state @{text s}, can only be blocked in
+in the state @{text "s' @ s"} by a thread @{text th'} that already
-the state @{text "s' @ s"} by a thread @{text th'} that already
+existed in @{text s} and requested or had a lock on at least one
-existed in @{text s} and requested or had a lock on at least
+resource---that means the thread was not \emph{detached} in @{text
-one resource---that means the thread was not \emph{detached} in @{text s}.
+s}.  As we shall see shortly, that means there are only finitely
-As we shall see shortly, that means there are only finitely
+many threads that can block @{text th} in this way and then they
-many threads that can block @{text th} in this way and then they
 need to run with the same 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. There are mainly two reasons for this:
+awkward to formalise in our model. There are mainly two reasons for
-First, we do not specify what ``running'' the code of a thread
+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 looking request also a corresponding
 unlocking request for a resource. Second, we would need to specify a
 kind of global clock that tracks the time how long a thread locks a
 resource. But this seems difficult, because how do we conveniently
-distinguish between a thread that ``just'' lock a resource for a
+distinguish between a thread that ``just'' locks a resource for a
 very long time and one that locks it forever.  Therefore we decided
 to leave out this property and let the programmer assume the
 responsibility to program threads in such a benign manner (in
 addition to causing no circularity in the 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 improving their bound.
+In what follows we will describe properties of PIP that allow us to
+prove Theorem~\ref{mainthm} and, when instructive, briefly describe
+our argument. Recall we want to prove that in state @{term "s' @ s"}
+either @{term th} is either running or blocked by a thread @{term
+"th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
+can show that
+\begin{lemma}
+If @{thm (prem 2) eq_pv_blocked}
+then @{thm (concl) eq_pv_blocked}
+\end{lemma}
+\begin{lemma}
+If @{thm (prem 2) eq_pv_persist}
+then @{thm (concl) eq_pv_persist}
+\end{lemma}
 \subsection*{\bf OUTLINE}
 Since @{term "th"} is the most urgent thread, if it is somehow
 blocked, people want to know why and wether this blocking is
 reasonable.
 From these two lemmas we can see the correctness of PIP, which is
 that: the blockage of th is reasonable and under control.
 Lemmas we want to describe:
-\begin{lemma}
-@{thm eq_pv_persist}
-\end{lemma}
-\begin{lemma}
-@{thm eq_pv_blocked}
-\end{lemma}
 \begin{lemma}
 @{thm runing_cntP_cntV_inv}
 \end{lemma}

changeset 82	c0a4e840aefe
parent 76	b6ea51cd2e88
child 95	8d2cc27f45f3