diff -r 0c89419b4742 -r 5454387e42ce Correctness.thy --- a/Correctness.thy Wed Feb 03 22:17:29 2016 +0800 +++ b/Correctness.thy Wed Feb 03 14:37:35 2016 +0000 @@ -2,9 +2,6 @@ imports PIPBasics begin -lemma Setcompr_eq_image: "{f x | x. x \ A} = f ` A" - by blast - text {* The following two auxiliary lemmas are used to reason about @{term Max}. *} @@ -476,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' \ runing (t @ s)" - shows "cp (t @ s) th' = preced th s" + assumes runing': "th' \ 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 "\ = 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 "\ = ?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' \ 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. @@ -518,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' \ th"}. @@ -527,13 +529,13 @@ lemma eq_pv_blocked: (* ddd *) assumes neq_th': "th' \ th" - and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'" - shows "th' \ runing (t @ s)" + and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" + shows "th' \ runing (t@s)" proof - assume otherwise: "th' \ runing (t @ s)" + assume otherwise: "th' \ runing (t@s)" show False proof - - have th'_in: "th' \ threads (t @ s)" + have th'_in: "th' \ threads (t@s)" using otherwise readys_threads runing_def by auto have "th' = th" proof(rule preced_unique) @@ -547,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 @@ -570,8 +573,8 @@ lemma eq_pv_persist: (* ddd *) assumes neq_th': "th' \ 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"}: *} @@ -621,28 +624,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' \ th" and eq_pv: "cntP s th' = cntV s th'" - shows "th' \ runing (t @ s)" + shows "th' \ 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' \ runing (t @ s)" + assumes is_runing: "th' \ runing (t@s)" and neq_th': "th' \ th" shows "cntP s th' > cntV s th'" using assms @@ -668,13 +665,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' \ runing (t@s)" and neq_th': "th' \ th" @@ -692,12 +687,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' \ runing (t@s)" and neq_th: "th' \ th" @@ -715,27 +707,22 @@ 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 \ runing (t @ s)" + assumes "th \ runing (t@s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ runing (t @ s)" + "th' \ 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 @@ -763,7 +750,7 @@ show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) next show "subtree (tRAG (t @ s)) (Th th') \ 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 \ subtree (tRAG (t @ s)) (Th th')" using dp by (unfold tRAG_subtree_eq, auto simp:subtree_def) @@ -793,23 +780,18 @@ 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) \ {}" -proof(cases "th \ runing (t @ s)") +lemma live: "runing (t@s) \ {}" +proof(cases "th \ runing (t@s)") case True thus ?thesis by auto next case False thus ?thesis using th_blockedE by auto qed - end end