--- a/Correctness.thy Tue Aug 16 11:49:37 2016 +0100
+++ b/Correctness.thy Wed Aug 24 16:13:20 2016 +0200
@@ -727,68 +727,64 @@
is exactly @{term "th'"}.
*}
lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
- assumes "th \<notin> running (t@s)"
- obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> running (t@s)"
+ assumes "th \<notin> running (t @ s)"
+ obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
+ "th' \<in> running (t @ s)"
proof -
- -- {* According to @{thm vat_t.th_chain_to_ready}, either
+ -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either
@{term "th"} is in @{term "readys"} or there is path leading from it to
one thread in @{term "readys"}. *}
- have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)"
- using th_kept vat_t.th_chain_to_ready by auto
+ have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (th, th') \<in> (tG (t @ s))\<^sup>+)"
+ using th_kept vat_t.th_chain_to_ready_tG by blast
+
-- {* However, @{term th} can not be in @{term readys}, because otherwise, since
- @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *}
- moreover have "th \<notin> readys (t@s)"
+ @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *}
+ moreover have "th \<notin> readys (t @ s)"
using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto
+
-- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
term @{term readys}: *}
- ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
- and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
+ ultimately obtain th' where th'_in: "th' \<in> readys (t @ s)"
+ and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
+
-- {* We are going to show that this @{term th'} is running. *}
- have "th' \<in> running (t@s)"
+ have "th' \<in> running (t @ s)"
proof -
-- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
- have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
+ have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R")
proof -
-- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
the @{term cp}-value of @{term th'} is the maximum of
all precedences of all thread nodes in its @{term tRAG}-subtree: *}
- have "?L = Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
- by (unfold cp_alt_def1, simp)
- also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
+ have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"
+ by (unfold cp_alt_def2, simp)
+ also have "... = (the_preced (t @ s) th)"
proof(rule image_Max_subset)
- 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)
+ show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
next
- show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
- by (unfold tRAG_subtree_eq, auto simp:subtree_def)
+ show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
+ using readys_def th'_in vat_t.subtree_tG_thread by auto
next
- show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
- (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")
- proof -
- have "?L = the_preced (t @ s) ` threads (t @ s)"
- by (unfold image_comp, rule image_cong, auto)
- thus ?thesis using max_preced the_preced_def by auto
- qed
+ show "th \<in> subtree (tG (t @ s)) th'"
+ by (simp add: dp subtree_def trancl_into_rtrancl)
+ next
+ show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
+ by simp
qed
- thm the_preced_def
also have "... = ?R"
using th_cp_max th_cp_preced th_kept
the_preced_def vat_t.max_cp_readys_threads by auto
- thm th_cp_max th_cp_preced th_kept
- the_preced_def vat_t.max_cp_readys_threads
- finally show ?thesis .
+ finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
qed
- -- {* Now, since @{term th'} holds the highest @{term cp}
- and we have already show it is in @{term readys},
+
+ -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
it is @{term running} by definition. *}
- with `th' \<in> readys (t@s)` show ?thesis by (simp add: running_def)
+ with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def)
qed
+
-- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
- moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
+ moreover have "th' \<in> ancestors (tG (t @ s)) th"
+ by (simp add: ancestors_def dp)
ultimately show ?thesis using that by metis
qed
@@ -863,18 +859,22 @@
qed
lemma th_blockedE_pretty:
- assumes "th \<notin> running (t@s)"
- shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> running (t@s)"
-using th_blockedE assms by blast
+ assumes "th \<notin> running (t @ s)"
+ shows "\<exists>th'. th' \<in> ancestors (tG (t @ s)) th \<and> th' \<in> running (t @ s)"
+using th_blockedE assms
+by blast
+
+
+
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
+ 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: "running (t@s) \<noteq> {}"
-proof(cases "th \<in> running (t@s)")
+lemma live: "running (t @ s) \<noteq> {}"
+proof(cases "th \<in> running (t @ s)")
case True thus ?thesis by auto
next
case False
@@ -882,19 +882,20 @@
qed
lemma blockedE:
- assumes "th \<notin> running (t@s)"
- obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> running (t@s)"
+ assumes "th \<notin> running (t @ s)"
+ obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
+ "th' \<in> running (t @ s)"
"th' \<in> threads s"
"\<not>detached s th'"
- "cp (t@s) th' = preced th s"
+ "cp (t @ s) th' = preced th s"
"th' \<noteq> th"
-by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)
+using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE
+by metis
lemma detached_not_running:
- assumes "detached (t@s) th'"
+ assumes "detached (t @ s) th'"
and "th' \<noteq> th"
- shows "th' \<notin> running (t@s)"
+ shows "th' \<notin> running (t @ s)"
proof
assume otherwise: "th' \<in> running (t @ s)"
have "cp (t@s) th' = cp (t@s) th"
@@ -920,19 +921,21 @@
section {* The correctness theorem of PIP *}
text {*
- In this section, we identify two more conditions in addition to the ones already
- specified in the forgoing locales, based on which the correctness of PIP is
- formally proved.
+
+ In this section, we identify two more conditions in addition to the ones
+ already specified in the current locale, based on which the correctness
+ of PIP is formally proved.
- Note that Priority Inversion refers to the phenomenon where the thread with highest priority
- is blocked by one with lower priority because the resource it is requesting is
- currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion},
- i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large.
+ Note that Priority Inversion refers to the phenomenon where the thread
+ with highest priority is blocked by one with lower priority because the
+ resource it is requesting is currently held by the later. The objective of
+ PIP is to avoid {\em Indefinite Priority Inversion}, i.e. the number of
+ occurrences of {\em Priority Inversion} becomes indefinitely large.
- For PIP to be correct, a finite upper bound needs to be found for the occurrence number,
- and the existence. This section makes explicit two more conditions so that the existence
- of such a upper bound can be proved to exist.
-*}
+ For PIP to be correct, a finite upper bound needs to be found for the
+ occurrence number, and the existence. This section makes explicit two more
+ conditions so that the existence of such a upper bound can be proved to
+ exist. *}
text {*
The following set @{text "blockers"} characterizes the set of threads which