--- a/Correctness.thy Wed Feb 03 21:41:42 2016 +0800
+++ b/Correctness.thy Wed Feb 03 21:51:57 2016 +0800
@@ -2,6 +2,9 @@
imports PIPBasics
begin
+lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
+ by blast
+
text {*
The following two auxiliary lemmas are used to reason about @{term Max}.
*}
@@ -473,45 +476,40 @@
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 eq_pv_dependants} to derive the
+ The key is the use of @{thm count_eq_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.
@@ -520,7 +518,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"}.
@@ -529,13 +527,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)
@@ -549,13 +547,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'"
- by (unfold cp_eq_cpreced cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
+ 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
@@ -573,8 +570,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 +621,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 +668,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 +692,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,22 +715,27 @@
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)"
+ assumes "th \<notin> runing (t @ s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> runing (t@s)"
+ "th' \<in> runing (t @ s)"
proof -
-- {* According to @{thm vat_t.th_chain_to_ready}, either
@{term "th"} is in @{term "readys"} or there is path leading from it to
@@ -750,7 +763,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.rg_RAG_threads vat_t.subtree_tRAG_thread)
+ by (metis Range.intros dp trancl_range vat_t.range_in 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)
@@ -780,18 +793,23 @@
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)")
+
+lemma live: "runing (t @ s) \<noteq> {}"
+proof(cases "th \<in> runing (t @ s)")
case True thus ?thesis by auto
next
case False
thus ?thesis using th_blockedE by auto
qed
+
end
end