diff -r b6ea51cd2e88 -r c0a4e840aefe Correctness.thy --- a/Correctness.thy Fri Jan 15 02:05:29 2016 +0000 +++ b/Correctness.thy Wed Jan 27 13:47:08 2016 +0000 @@ -474,42 +474,37 @@ 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' \ runing (t@s)" - shows "cp (t@s) th' = preced th s" (is "?L = ?R") + assumes runing': "th' \ 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 "\ = ?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 "\ = 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' \ th"}. The key is the use of @{thm count_eq_dependants} to derive the @@ -521,7 +516,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' \ th"}. @@ -530,13 +525,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) @@ -550,13 +545,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'" + 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 @@ -574,8 +568,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) -- {* 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 +618,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' \ 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 @@ -665,11 +665,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' \ runing (t@s)" and neq_th': "th' \ th" @@ -687,9 +689,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' \ runing (t@s)" and neq_th: "th' \ th" @@ -707,18 +712,23 @@ 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)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" @@ -780,11 +790,15 @@ 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)") case True thus ?thesis by auto