--- a/Correctness.thy Fri Jan 29 09:46:07 2016 +0800
+++ b/Correctness.thy Fri Jan 29 10:51:52 2016 +0800
@@ -1,8 +1,7 @@
-theory Correctness
-imports PIPBasics
+theory PrioG
+imports CpsG
begin
-
text {*
The following two auxiliary lemmas are used to reason about @{term Max}.
*}
@@ -474,40 +473,45 @@
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.
- 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.
-
+ By `blocking thread`, we mean a thread in running state but
+ different from thread @{term th}.
*}
+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"
+ assumes runing': "th' \<in> runing (t@s)"
+ shows "cp (t@s) th' = preced th s" (is "?L = ?R")
proof -
- 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)
+ 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)
finally show ?thesis .
qed
text {*
- 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 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 proof is by contraction with the assumption @{text "th' \<noteq> th"}.
- The key is the use of @{thm count_eq_dependants} to derive the
+ The key is the use of @{thm eq_pv_dependants} to derive the
emptiness of @{text th'}s @{term dependants}-set from the balance of
its @{term P} and @{term V} counts. From this, it can be shown
@{text th'}s @{term cp}-value equals to its own precedence.
@@ -516,7 +520,7 @@
runing_preced_inversion}, its @{term cp}-value equals to the
precedence of @{term th}.
- Combining the above two results we have that @{text th'} and @{term
+ Combining the above two resukts 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"}.
@@ -525,13 +529,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)
@@ -545,12 +549,13 @@
-- {* 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'"
- by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
+ have "?L = cp (t@s) th'"
+ by (unfold cp_eq_cpreced cpreced_def eq_dependants vat_t.eq_pv_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
@@ -568,8 +573,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)
+ shows "cntP (t@s) th' = cntV (t@s) th'"
+proof(induction rule:ind) -- {* The proof goes by induction. *}
-- {* 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"}: *}
@@ -618,28 +623,22 @@
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,13 +664,11 @@
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"
@@ -689,12 +686,9 @@
qed
text {*
-
- The following lemma summarises the above lemmas to give an overall
- characterisationof the blocking thread @{text "th'"}:
-
+ The following lemma summarizes several foregoing
+ lemmas to give an overall picture of 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"
@@ -712,23 +706,18 @@
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)"
@@ -760,7 +749,7 @@
show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
next
show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
- by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread)
+ by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread)
next
show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
by (unfold tRAG_subtree_eq, auto simp:subtree_def)
@@ -790,15 +779,11 @@
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
@@ -807,6 +792,5 @@
thus ?thesis using th_blockedE by auto
qed
-
end
end