diff -r 3fa70b12c117 -r b0054fb0d1ce Correctness.thy~ --- a/Correctness.thy~ Wed Jan 13 15:22:14 2016 +0000 +++ b/Correctness.thy~ Wed Jan 13 23:39:59 2016 +0800 @@ -2,6 +2,7 @@ imports PIPBasics begin + text {* The following two auxiliary lemmas are used to reason about @{term Max}. *} @@ -79,17 +80,15 @@ ultimately show ?thesis by auto qed -lemma highest_cp_preced: "cp s th = Max ((\ th'. preced th' s) ` threads s)" - by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) +lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" + using eq_cp_s_th highest max_cp_eq the_preced_def by presburger + -lemma highest_preced_thread: "preced th s = Max ((\ th'. preced th' s) ` threads s)" +lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)" by (fold eq_cp_s_th, unfold highest_cp_preced, simp) lemma highest': "cp s th = Max (cp s ` threads s)" -proof - - from highest_cp_preced max_cp_eq[symmetric] - show ?thesis by simp -qed + by (simp add: eq_cp_s_th highest) end @@ -125,7 +124,6 @@ qed qed - locale red_extend_highest_gen = extend_highest_gen + fixes i::nat @@ -248,16 +246,15 @@ operations of PIP. All cases follow the same pattern rendered by the generalized introduction rule @{thm "image_Max_eqI"}. - The very essence is to show that precedences, no matter whether they are newly introduced - or modified, are always lower than the one held by @{term "th"}, - which by @{thm th_kept} is preserved along the way. + The very essence is to show that precedences, no matter whether they + are newly introduced or modified, are always lower than the one held + by @{term "th"}, which by @{thm th_kept} is preserved along the way. *} lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" proof(induct rule:ind) case Nil from highest_preced_thread - show ?case - by (unfold the_preced_def, simp) + show ?case by simp next case (Cons e t) interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto @@ -285,7 +282,8 @@ assume "x = thread" thus ?thesis apply (simp add:Create the_preced_def preced_def, fold preced_def) - using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 + preced_th by force next assume h: "x \ threads (t @ s)" from Cons(2)[unfolded Create] @@ -440,10 +438,25 @@ finally show ?thesis . qed -lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" +lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th" using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger -lemma th_cp_preced: "cp (t@s) th = preced th s" +lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))" + by (simp add: th_cp_max_preced) + +lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th" + using max_kept th_kept the_preced_def by auto + +lemma [simp]: "the_preced (t@s) th = preced th (t@s)" + using the_preced_def by auto + +lemma [simp]: "preced th (t@s) = preced th s" + by (simp add: th_kept) + +lemma [simp]: "cp s th = preced th s" + by (simp add: eq_cp_s_th) + +lemma th_cp_preced [simp]: "cp (t@s) th = preced th s" by (fold max_kept, unfold th_cp_max_preced, simp) lemma preced_less: @@ -455,6 +468,21 @@ preced_linorder rev_image_eqI threads_s vat_s.finite_threads vat_s.le_cp) +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}. +*} + text {* The following lemmas shows that the @{term cp}-value of the blocking thread @{text th'} equals to the highest @@ -471,17 +499,31 @@ finally show ?thesis . qed -section {* The `blocking thread` *} +text {* + The following lemma shows how the counting of + @{term "P"} and @{term "V"} operations affects + the running state of threads in @{term t}. + + 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 can not be in running thread. -text {* - Counting of the number of @{term "P"} and @{term "V"} operations - is the cornerstone of a large number of the following proofs. - The reason is that this counting is quite easy to calculate and - convenient to use in the reasoning. + The proof is by contraction with the assumption @{text "th' \ th"}. + 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} @{term V} counts. + From this, it can be shown @{text th'}s @{term cp}-value + equals to its own precedence. - The following lemma shows that the counting controls whether - a thread is running or not. -*} (* ccc *) + 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 we have that @{text th'} and + @{term th} have the same precedence. By uniqueness of precedence, we + have @{text "th' = th"}, which is in contradiction with the + assumption @{text "th' \ th"}. +*} lemma eq_pv_blocked: (* ddd *) assumes neq_th': "th' \ th" @@ -507,16 +549,16 @@ 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) - -- {* Since @{term "th'"} is running by @{thm otherwise}, - it has the highest @{term cp}-value, by definition, - which in turn equals to the @{term cp}-value of @{term th}. *} + -- {* 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" - using runing_preced_inversion[OF otherwise] th_kept by simp + thm runing_preced_inversion + using runing_preced_inversion[OF otherwise] by simp finally show ?thesis . qed qed (auto simp: th'_in th_kept) - moreover have "th' \ th" using neq_th' . - ultimately show ?thesis by simp + with `th' \ th` show ?thesis by simp qed qed @@ -589,15 +631,6 @@ using assms by (simp add: eq_pv_blocked eq_pv_persist) -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. - - The following lemmas will give us such a picture: -*} - text {* The following lemma shows the blocking thread @{term th'} must hold some resource in the very beginning. @@ -757,5 +790,6 @@ thus ?thesis using th_blockedE by auto qed + end end