pip: comparison Correctness.thy

equal deleted inserted replaced

-:0c89419b4742
+:5454387e42ce
 theory Correctness
 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}.
 *}
 lemma image_Max_eqI:
 vat_s.le_cp)
 section {* The `blocking thread` *}
 text {*
+The purpose of PIP is to ensure that the most
-The purpose of PIP is to ensure that the most urgent thread @{term
+urgent thread @{term th} is not blocked unreasonably.
-th} is not blocked unreasonably. Therefore, below, we will derive
+Therefore, a clear picture of the blocking thread is essential
-properties of the blocking thread. By blocking thread, we mean a
+to assure people that the purpose is fulfilled.
-thread in running state t @ s, but is different from thread @{term
-th}.
+In this section, we are going to derive a series of lemmas
+with finally give rise to a picture of the blocking thread.
-The first lemmas shows that the @{term cp}-value of the blocking
-thread @{text th'} equals to the highest precedence in the whole
+By `blocking thread`, we mean a thread in running state but
-system.
+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)"
+assumes runing': "th' \<in> runing (t@s)"
-shows "cp (t @ s) th' = preced th 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))"
+have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
-using assms by (unfold runing_def, auto)
+by (unfold runing_def, auto)
-also have "\<dots> = preced th s"
+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
+The following lemma shows how the counters for @{term "P"} and
-"V"} operations relate to the running threads in the states @{term
+@{term "V"} operations relate to the running threads in the states
-s} and @{term "t @ s"}: if a thread's @{term "P"}-count equals its
+@{term s} and @{term "t @ s"}.  The lemma shows that if a thread's
-@{term "V"}-count (which means it no longer has any resource in its
+@{term "P"}-count equals its @{term "V"}-count (which means it no
-possession), it cannot be a running thread.
+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.
 On the other hand, since @{text th'} is running, by @{thm
 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"}.
 *}
 lemma eq_pv_blocked: (* ddd *)
 assumes neq_th': "th' \<noteq> th"
-and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'"
+and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
-shows "th' \<notin> runing (t @ s)"
+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)
 -- {* The proof goes like this:
 it is first shown that the @{term preced}-value of @{term th'}
 show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
 proof -
 -- {* 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)
+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
 qed (auto simp: th'_in th_kept)
 with `th' \<noteq> th` show ?thesis by simp
 it will keep hand-emptied in the future @{term "t@s"}.
 *}
 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'"
+shows "cntP (t@s) th' = cntV (t@s) th'"
-proof(induction rule: ind)
+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"}: *}
 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
 ultimately show ?thesis using Cons(5) by metis
 qed
 qed (auto simp:eq_pv)
 text {*
+By combining @{thm  eq_pv_blocked} and @{thm eq_pv_persist},
-By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can
+it can be derived easily that @{term th'} can not be running in the future:
-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'}
-The following lemma shows the blocking thread @{term th'} must hold
+must hold some resource in the very beginning.
-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
 proof -
 -- {* First, it can be shown that the number of @{term P} and
 ultimately show ?thesis by auto
 qed
 text {*
+The following lemmas shows the blocking thread @{text th'} must be live
-The following lemmas shows the blocking thread @{text th'} must be
+at the very beginning, i.e. the moment (or state) @{term s}.
-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"
 shows "th' \<in> threads s"
 proof(rule ccontr) -- {* Proof by contradiction: *}
 qed
 with runing' show False by simp
 qed
 text {*
+The following lemma summarizes several foregoing
-The following lemma summarises the above lemmas to give an overall
+lemmas to give an overall picture of the blocking thread @{text "th'"}:
-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"
 shows "th' \<in> threads s"
 and    "\<not>detached s th'"
 next
 from runing_preced_inversion[OF runing']
 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
-Suppose @{term th} is not running, it is first shown that there is a
+there is a path in RAG leading from node @{term th} to another thread @{text "th'"}
-path in RAG leading from node @{term th} to another thread @{text
+in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
-"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,
-Now, since @{term readys}-set is non-empty, there must be one in it
+is the @{term runing}-thread. However, we are going to show more: this running thread
-which holds the highest @{term cp}-value, which, by definition, is
+is exactly @{term "th'"}.
-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
 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>+)"
 also have "... = (the_preced (t @ s) \<circ> the_thread) (Th 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.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)
 next
 show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
 ultimately show ?thesis using that by metis
 qed
 text {*
+Now it is easy to see there is always a thread to run by case analysis
-Now it is easy to see there is always a thread to run by case
+on whether thread @{term th} is running: if the answer is Yes, the
-analysis on whether thread @{term th} is running: if the answer is
+the running thread is obviously @{term th} itself; otherwise, the running
-yes, the the running thread is obviously @{term th} itself;
+thread is the @{text th'} given by lemma @{thm th_blockedE}.
-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

changeset 106	5454387e42ce
parent 104	43482ab31341
child 107	30ed212f268a