--- a/prio/Paper/Paper.thy Tue Feb 14 03:26:18 2012 +0000
+++ b/prio/Paper/Paper.thy Tue Feb 14 04:13:15 2012 +0000
@@ -597,26 +597,29 @@
begin
(*>*)
text {*
- Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
- for PIP in terms of the number of critical resources: if there are
+ 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 @{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}
- number of times. This result on its own, strictly speaking, does
+ can only be blocked @{text m} times. Both results on their own, strictly speaking, do
\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
@@ -628,9 +631,10 @@
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:
@@ -684,15 +688,21 @@
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
- finitely many threads. Like in the argument by Sha et al.~this
+ 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} 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
@@ -701,6 +711,8 @@
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.
@@ -751,9 +763,7 @@
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
- of a \emph{detached} thread in a state, that is one which does not hold any
- critical resource nor requests one.
+ The key lemma in our proof of Theorem~\ref{mainthm} is as follows:
\begin{lemma}\label{mainlem}
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
@@ -788,27 +798,19 @@
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}
@@ -1243,8 +1245,9 @@
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}