--- a/Journal/Paper.thy Fri Jan 15 02:05:29 2016 +0000
+++ b/Journal/Paper.thy Wed Jan 27 13:47:08 2016 +0000
@@ -784,51 +784,56 @@
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
- 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 a maximum of @{text m} times. Both results on their own, strictly speaking, do
- \emph{not} prevent indefinite, or unbounded, Priority Inversion,
- 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 must ensure that threads are programmed in this way. However, even
- taking this assumption into account, the correctness properties of
- Sha et al.~are
- \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken
- \cite{Yodaiken02} and Moylan et al.~\cite{deinheritance} 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 two bounds.
+ Their second correctness criterion is given 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 a maximum of @{text m} times. Both results on their
+ own, strictly speaking, do \emph{not} prevent indefinite, or
+ unbounded, Priority Inversion, 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 must ensure that
+ threads are programmed in this way. However, even taking this
+ assumption into account, the correctness properties of Sha et
+ al.~are \emph{not} true for their version of PIP---despite being
+ ``proved''. As Yodaiken \cite{Yodaiken02} and Moylan et
+ al.~\cite{deinheritance} 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 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
- and finish with a corresponding @{text V}-event, to arbitrarily overlap
- (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 waiting
- for 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
+ reason is that we allow critical sections, which start with a @{text
+ P}-event and finish with a corresponding @{text V}-event, to
+ arbitrarily overlap (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 waiting for 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
- 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:
+ 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}
{\bf Assumptions on the states {\boldmath@{text s}} and
@@ -872,9 +877,9 @@
\end{isabelle}
\end{quote}
- \noindent
- The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}.
- Under these assumptions we shall prove the following correctness property:
+ \noindent The locale mechanism of Isabelle helps us to manage
+ conveniently such assumptions~\cite{Haftmann08}. Under these
+ assumptions we shall prove the following correctness property:
\begin{theorem}\label{mainthm}
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
@@ -884,29 +889,28 @@
@{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} and requested or had a lock on at least
- 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} in this way and then they
+ \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} and requested or had a lock on at least 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} 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:
- First, we do not specify what ``running'' the code of a thread
+ awkward to formalise in our model. There are mainly two 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 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
@@ -915,6 +919,25 @@
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
@@ -962,13 +985,7 @@
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}