--- a/Correctness.thy Fri Jan 15 02:05:29 2016 +0000
+++ b/Correctness.thy Wed Jan 27 13:47:08 2016 +0000
@@ -474,42 +474,37 @@
section {* The `blocking thread` *}
text {*
- The purpose of PIP is to ensure that the most
- urgent thread @{term th} is not blocked unreasonably.
- Therefore, a clear picture of the blocking thread is essential
- to assure people that the purpose is fulfilled.
-
- In this section, we are going to derive a series of lemmas
- with finally give rise to a picture of the blocking thread.
- By `blocking thread`, we mean a thread in running state but
- different from thread @{term th}.
+ The purpose of PIP is to ensure that the most urgent thread @{term
+ th} is not blocked unreasonably. Therefore, below, we will derive
+ properties of the blocking thread. By blocking thread, we mean a
+ thread in running state t @ s, but is different from thread @{term
+ th}.
+
+ The first lemmas shows that the @{term cp}-value of the blocking
+ thread @{text th'} equals to the highest precedence in the whole
+ system.
+
*}
-text {*
- The following lemmas shows that the @{term cp}-value
- of the blocking thread @{text th'} equals to the highest
- precedence in the whole system.
-*}
lemma runing_preced_inversion:
- assumes runing': "th' \<in> runing (t@s)"
- shows "cp (t@s) th' = preced th s" (is "?L = ?R")
+ assumes runing': "th' \<in> runing (t @ s)"
+ shows "cp (t @ s) th' = preced th s"
proof -
- have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
- by (unfold runing_def, auto)
- also have "\<dots> = ?R"
- by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
+ have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"
+ using assms by (unfold runing_def, auto)
+ also have "\<dots> = preced th s"
+ by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
finally show ?thesis .
qed
text {*
- The following lemma shows how the counters for @{term "P"} and
- @{term "V"} operations relate to the running threads in the states
- @{term s} and @{term "t @ s"}. The lemma shows that if a thread's
- @{term "P"}-count equals its @{term "V"}-count (which means it no
- longer has any resource in its possession), it cannot be a running
- thread.
+ The next lemma shows how the counters for @{term "P"} and @{term
+ "V"} operations relate to the running threads in the states @{term
+ s} and @{term "t @ s"}: if a thread's @{term "P"}-count equals its
+ @{term "V"}-count (which means it no longer has any resource in its
+ possession), it cannot be a running thread.
The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
The key is the use of @{thm count_eq_dependants} to derive the
@@ -521,7 +516,7 @@
runing_preced_inversion}, its @{term cp}-value equals to the
precedence of @{term th}.
- Combining the above two resukts we have that @{text th'} and @{term
+ Combining the above two results we have that @{text th'} and @{term
th} have the same precedence. By uniqueness of precedences, we have
@{text "th' = th"}, which is in contradiction with the assumption
@{text "th' \<noteq> th"}.
@@ -530,13 +525,13 @@
lemma eq_pv_blocked: (* ddd *)
assumes neq_th': "th' \<noteq> th"
- and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
- shows "th' \<notin> runing (t@s)"
+ and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'"
+ shows "th' \<notin> runing (t @ s)"
proof
- assume otherwise: "th' \<in> runing (t@s)"
+ assume otherwise: "th' \<in> runing (t @ s)"
show False
proof -
- have th'_in: "th' \<in> threads (t@s)"
+ have th'_in: "th' \<in> threads (t @ s)"
using otherwise readys_threads runing_def by auto
have "th' = th"
proof(rule preced_unique)
@@ -550,13 +545,12 @@
-- {* Since the counts of @{term th'} are balanced, the subtree
of it contains only itself, so, its @{term cp}-value
equals its @{term preced}-value: *}
- have "?L = cp (t@s) th'"
+ have "?L = cp (t @ s) th'"
by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
-- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
its @{term cp}-value equals @{term "preced th s"},
which equals to @{term "?R"} by simplification: *}
also have "... = ?R"
- thm runing_preced_inversion
using runing_preced_inversion[OF otherwise] by simp
finally show ?thesis .
qed
@@ -574,8 +568,8 @@
lemma eq_pv_persist: (* ddd *)
assumes neq_th': "th' \<noteq> th"
and eq_pv: "cntP s th' = cntV s th'"
- shows "cntP (t@s) th' = cntV (t@s) th'"
-proof(induction rule:ind) -- {* The proof goes by induction. *}
+ shows "cntP (t @ s) th' = cntV (t @ s) th'"
+proof(induction rule: ind)
-- {* The nontrivial case is for the @{term Cons}: *}
case (Cons e t)
-- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
@@ -624,22 +618,28 @@
qed (auto simp:eq_pv)
text {*
- By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist},
- it can be derived easily that @{term th'} can not be running in the future:
+
+ By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can
+ be derived easily that @{term th'} can not be running in the future:
+
*}
+
lemma eq_pv_blocked_persist:
assumes neq_th': "th' \<noteq> th"
and eq_pv: "cntP s th' = cntV s th'"
- shows "th' \<notin> runing (t@s)"
+ shows "th' \<notin> runing (t @ s)"
using assms
by (simp add: eq_pv_blocked eq_pv_persist)
text {*
- The following lemma shows the blocking thread @{term th'}
- must hold some resource in the very beginning.
+
+ The following lemma shows the blocking thread @{term th'} must hold
+ some resource in the very beginning.
+
*}
+
lemma runing_cntP_cntV_inv: (* ddd *)
- assumes is_runing: "th' \<in> runing (t@s)"
+ assumes is_runing: "th' \<in> runing (t @ s)"
and neq_th': "th' \<noteq> th"
shows "cntP s th' > cntV s th'"
using assms
@@ -665,11 +665,13 @@
text {*
- The following lemmas shows the blocking thread @{text th'} must be live
- at the very beginning, i.e. the moment (or state) @{term s}.
+ The following lemmas shows the blocking thread @{text th'} must be
+ live at the very beginning, i.e. the moment (or state) @{term s}.
The proof is a simple combination of the results above:
+
*}
+
lemma runing_threads_inv:
assumes runing': "th' \<in> runing (t@s)"
and neq_th': "th' \<noteq> th"
@@ -687,9 +689,12 @@
qed
text {*
- The following lemma summarizes several foregoing
- lemmas to give an overall picture of the blocking thread @{text "th'"}:
+
+ The following lemma summarises the above lemmas to give an overall
+ characterisationof the blocking thread @{text "th'"}:
+
*}
+
lemma runing_inversion: (* ddd, one of the main lemmas to present *)
assumes runing': "th' \<in> runing (t@s)"
and neq_th: "th' \<noteq> th"
@@ -707,18 +712,23 @@
show "cp (t@s) th' = preced th s" .
qed
+
section {* The existence of `blocking thread` *}
text {*
- Suppose @{term th} is not running, it is first shown that
- there is a path in RAG leading from node @{term th} to another thread @{text "th'"}
- in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
+
+ Suppose @{term th} is not running, it is first shown that there is a
+ path in RAG leading from node @{term th} to another thread @{text
+ "th'"} in the @{term readys}-set (So @{text "th'"} is an ancestor of
+ @{term th}}).
- Now, since @{term readys}-set is non-empty, there must be
- one in it which holds the highest @{term cp}-value, which, by definition,
- is the @{term runing}-thread. However, we are going to show more: this running thread
- is exactly @{term "th'"}.
- *}
+ Now, since @{term readys}-set is non-empty, there must be one in it
+ which holds the highest @{term cp}-value, which, by definition, is
+ the @{term runing}-thread. However, we are going to show more: this
+ running thread is exactly @{term "th'"}.
+
+*}
+
lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
assumes "th \<notin> runing (t@s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
@@ -780,11 +790,15 @@
qed
text {*
- Now it is easy to see there is always a thread to run by case analysis
- on whether thread @{term th} is running: if the answer is Yes, the
- the running thread is obviously @{term th} itself; otherwise, the running
- thread is the @{text th'} given by lemma @{thm th_blockedE}.
+
+ Now it is easy to see there is always a thread to run by case
+ analysis on whether thread @{term th} is running: if the answer is
+ yes, the the running thread is obviously @{term th} itself;
+ otherwise, the running thread is the @{text th'} given by lemma
+ @{thm th_blockedE}.
+
*}
+
lemma live: "runing (t@s) \<noteq> {}"
proof(cases "th \<in> runing (t@s)")
case True thus ?thesis by auto
--- 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}
Binary file journal.pdf has changed