diff -r a88af0e4731f -r 38c6acf03f68 Correctness.thy --- a/Correctness.thy Tue Jun 07 13:51:39 2016 +0100 +++ b/Correctness.thy Thu Jun 09 23:01:36 2016 +0100 @@ -498,12 +498,12 @@ 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)" +lemma running_preced_inversion: + assumes running': "th' \ running (t@s)" shows "cp (t@s) th' = preced th s" (is "?L = ?R") proof - have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms - by (unfold runing_def, auto) + by (unfold running_def, auto) also have "\ = ?R" by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) finally show ?thesis . @@ -525,7 +525,7 @@ @{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 + running_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 @@ -538,13 +538,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)" + shows "th' \ running (t@s)" proof - assume otherwise: "th' \ runing (t@s)" + assume otherwise: "th' \ running (t@s)" show False proof - have th'_in: "th' \ threads (t@s)" - using otherwise readys_threads runing_def by auto + using otherwise readys_threads running_def by auto have "th' = th" proof(rule preced_unique) -- {* The proof goes like this: @@ -559,12 +559,12 @@ equals its @{term preced}-value: *} have "?L = cp (t@s) th'" by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp) - -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, + -- {* Since @{term "th'"} is running, by @{thm running_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 + thm running_preced_inversion + using running_preced_inversion[OF otherwise] by simp finally show ?thesis . qed qed (auto simp: th'_in th_kept) @@ -600,11 +600,11 @@ from cntP_diff_inv[OF this[simplified]] obtain cs' where "e = P th' cs'" by auto from vat_es.pip_e[unfolded this] - have "th' \ runing (t@s)" + have "th' \ running (t@s)" by (cases, simp) -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis shows @{term th'} can not be running at moment @{term "t@s"}: *} - moreover have "th' \ runing (t@s)" + moreover have "th' \ running (t@s)" using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . -- {* Contradiction is finally derived: *} ultimately show False by simp @@ -618,8 +618,8 @@ from cntV_diff_inv[OF this[simplified]] obtain cs' where "e = V th' cs'" by auto from vat_es.pip_e[unfolded this] - have "th' \ runing (t@s)" by (cases, auto) - moreover have "th' \ runing (t@s)" + have "th' \ running (t@s)" by (cases, auto) + moreover have "th' \ running (t@s)" using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . ultimately show False by simp qed @@ -637,7 +637,7 @@ 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' \ running (t@s)" using assms by (simp add: eq_pv_blocked eq_pv_persist) @@ -645,8 +645,8 @@ 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)" +lemma running_cntP_cntV_inv: (* ddd *) + assumes is_running: "th' \ running (t@s)" and neq_th': "th' \ th" shows "cntP s th' > cntV s th'" using assms @@ -660,9 +660,9 @@ -- {* By applying @{thm eq_pv_blocked_persist} to this: *} from eq_pv_blocked_persist[OF neq_th' otherwise] -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} - have "th' \ runing (t@s)" . - -- {* This is obvious in contradiction with assumption @{thm is_runing} *} - thus False using is_runing by simp + have "th' \ running (t@s)" . + -- {* This is obvious in contradiction with assumption @{thm is_running} *} + thus False using is_running by simp qed -- {* However, the number of @{term V} is always less or equal to @{term P}: *} moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto @@ -677,40 +677,40 @@ The proof is a simple combination of the results above: *} -lemma runing_threads_inv: - assumes runing': "th' \ runing (t@s)" +lemma running_threads_inv: + assumes running': "th' \ running (t@s)" and neq_th': "th' \ th" shows "th' \ threads s" proof(rule ccontr) -- {* Proof by contradiction: *} assume otherwise: "th' \ threads s" - have "th' \ runing (t @ s)" + have "th' \ running (t @ s)" proof - from vat_s.cnp_cnv_eq[OF otherwise] have "cntP s th' = cntV s th'" . from eq_pv_blocked_persist[OF neq_th' this] show ?thesis . qed - with runing' show False by simp + with running' show False by simp qed text {* 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)" +lemma running_inversion: (* ddd, one of the main lemmas to present *) + assumes running': "th' \ running (t@s)" and neq_th: "th' \ th" shows "th' \ threads s" and "\detached s th'" and "cp (t@s) th' = preced th s" proof - - from runing_threads_inv[OF assms] + from running_threads_inv[OF assms] show "th' \ threads s" . next - from runing_cntP_cntV_inv[OF runing' neq_th] + from running_cntP_cntV_inv[OF running' neq_th] show "\detached s th'" using vat_s.detached_eq by simp next - from runing_preced_inversion[OF runing'] + from running_preced_inversion[OF running'] show "cp (t@s) th' = preced th s" . qed @@ -723,13 +723,13 @@ 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 the @{term running}-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 \ running (t@s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ runing (t@s)" + "th' \ running (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 @@ -737,15 +737,15 @@ have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" using th_kept vat_t.th_chain_to_ready by auto -- {* However, @{term th} can not be in @{term readys}, because otherwise, since - @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} + @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *} moreover have "th \ readys (t@s)" - using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + 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' \ readys (t@s)" and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto -- {* We are going to show that this @{term th'} is running. *} - have "th' \ runing (t@s)" + have "th' \ 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") @@ -783,8 +783,8 @@ qed -- {* Now, since @{term th'} holds the highest @{term cp} and we have already show it is in @{term readys}, - it is @{term runing} by definition. *} - with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) + it is @{term running} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: running_def) qed -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" @@ -793,26 +793,26 @@ qed lemma (* new proof of th_blockedE *) - assumes "th \ runing (t @ s)" + assumes "th \ running (t @ s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ runing (t @ s)" + "th' \ running (t @ s)" proof - -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is in @{term "readys"} or there is path in the @{term RAG} leading from it to a thread that is in @{term "readys"}. However, @{term th} cannot be in @{term readys}, because otherwise, since @{term th} holds the - highest @{term cp}-value, it must be @{term "runing"}. This would + highest @{term cp}-value, it must be @{term "running"}. This would violate our assumption. *} have "th \ readys (t @ s)" - using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto then have "\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+" using th_kept vat_t.th_chain_to_ready by auto then obtain th' where th'_in: "th' \ readys (t@s)" and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto -- {* We are going to first show that this @{term th'} is running. *} - have "th' \ runing (t @ s)" + have "th' \ running (t @ s)" proof - -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *} have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R") @@ -852,8 +852,8 @@ qed -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, - it is @{term runing} by definition. *} - with `th' \ readys (t @ s)` show "th' \ runing (t @ s)" by (simp add: runing_def) + it is @{term running} by definition. *} + with `th' \ readys (t @ s)` show "th' \ running (t @ s)" by (simp add: running_def) qed -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} @@ -863,8 +863,8 @@ qed lemma th_blockedE_pretty: - assumes "th \ runing (t@s)" - shows "\th'. Th th' \ ancestors (RAG (t @ s)) (Th th) \ th' \ runing (t@s)" + assumes "th \ running (t@s)" + shows "\th'. Th th' \ ancestors (RAG (t @ s)) (Th th) \ th' \ running (t@s)" using th_blockedE assms by blast text {* @@ -873,8 +873,8 @@ 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: "running (t@s) \ {}" +proof(cases "th \ running (t@s)") case True thus ?thesis by auto next case False @@ -882,25 +882,25 @@ qed lemma blockedE: - assumes "th \ runing (t@s)" + assumes "th \ running (t@s)" obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ runing (t@s)" + "th' \ running (t@s)" "th' \ threads s" "\detached s th'" "cp (t@s) th' = preced th s" "th' \ th" -by (metis assms runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE) +by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE) -lemma detached_not_runing: +lemma detached_not_running: assumes "detached (t@s) th'" and "th' \ th" - shows "th' \ runing (t@s)" + shows "th' \ running (t@s)" proof - assume otherwise: "th' \ runing (t @ s)" + assume otherwise: "th' \ running (t @ s)" have "cp (t@s) th' = cp (t@s) th" proof - have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise - by (simp add:runing_def) + by (simp add:running_def) moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads) ultimately show ?thesis by simp qed @@ -911,7 +911,7 @@ from preced_unique[OF this] have "th' \ threads (t @ s) \ th \ threads (t @ s) \ th' = th" . moreover have "th' \ threads (t@s)" - using otherwise by (unfold runing_def readys_def, auto) + using otherwise by (unfold running_def readys_def, auto) moreover have "th \ threads (t@s)" by (simp add: th_kept) ultimately have "th' = th" by metis with assms(2) show False by simp @@ -945,11 +945,11 @@ The following lemma shows that the definition of @{term "blockers"} is correct, i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}. *} -lemma runingE: - assumes "th' \ runing (t@s)" +lemma runningE: + assumes "th' \ running (t@s)" obtains (is_th) "th' = th" | (is_other) "th' \ blockers" - using assms blockers_def runing_inversion(2) by auto + using assms blockers_def running_inversion(2) by auto text {* The following lemma shows that the number of blockers are finite. @@ -1009,11 +1009,11 @@ have False proof(cases) case h: (thread_exit) - hence "th' \ readys (t@s)" by (auto simp:runing_def) + hence "th' \ readys (t@s)" by (auto simp:running_def) from readys_holdents_detached[OF this h(2)] have "detached (t @ s) th'" . - from et.detached_not_runing[OF this] assms[unfolded blockers_def] - have "th' \ runing (t @ s)" by auto + from et.detached_not_running[OF this] assms[unfolded blockers_def] + have "th' \ running (t @ s)" by auto with h(1) show ?thesis by simp qed } thus ?thesis by auto @@ -1094,7 +1094,7 @@ *} lemma actions_th_occs_pre: assumes "t = e'#t'" - shows "length (actions_of {th} t) \ occs (\ t'. th \ runing (t'@s)) t'" + shows "length (actions_of {th} t) \ occs (\ t'. th \ running (t'@s)) t'" using assms proof(induct arbitrary: e' t' rule:ind) case h: (Cons e t e' t') @@ -1111,7 +1111,7 @@ from ve'.th_no_create[OF _ this] have "\ isCreate e" by auto from PIP_actorE[OF h(2) True this] Nil - have "th \ runing s" by simp + have "th \ running s" by simp hence "?R = 1" using Nil h by simp moreover have "?L = 1" using True Nil by (simp add:actions_of_def) ultimately show ?thesis by simp @@ -1124,7 +1124,7 @@ case h1: (Cons e1 t1) hence eq_t': "t' = e1#t1" using h by simp from h(5)[OF h1] - have le: "length (actions_of {th} t) \ occs (\t'. th \ runing (t' @ s)) t1" + have le: "length (actions_of {th} t) \ occs (\t'. th \ running (t' @ s)) t1" (is "?F t \ ?G t1") . show ?thesis proof(cases "actor e = th") @@ -1132,7 +1132,7 @@ from ve'.th_no_create[OF _ this] have "\ isCreate e" by auto from PIP_actorE[OF h(2) True this] - have "th \ runing (t@s)" by simp + have "th \ running (t@s)" by simp hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp) moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def) ultimately show ?thesis using le by simp @@ -1149,12 +1149,12 @@ lemma really needed in later proofs. *} lemma actions_th_occs: - shows "length (actions_of {th} t) \ occs (\ t'. th \ runing (t'@s)) t" + shows "length (actions_of {th} t) \ occs (\ t'. th \ running (t'@s)) t" proof(cases t) case (Cons e' t') from actions_th_occs_pre[OF this] - have "length (actions_of {th} t) \ occs (\t'. th \ runing (t' @ s)) t'" . - moreover have "... \ occs (\t'. th \ runing (t' @ s)) t" + have "length (actions_of {th} t) \ occs (\t'. th \ running (t' @ s)) t'" . + moreover have "... \ occs (\t'. th \ running (t' @ s)) t" by (unfold Cons, auto) ultimately show ?thesis by simp qed (auto simp:actions_of_def) @@ -1187,10 +1187,10 @@ interpret ve : extend_highest_gen s th prio tm t using h by simp interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)") - proof(cases "actor e \ runing (t@s)") + proof(cases "actor e \ running (t@s)") case True thus ?thesis - proof(rule ve.runingE) + proof(rule ve.runningE) assume 1: "actor e = th" have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def) moreover have "?O (e#t) = ?O t" @@ -1273,17 +1273,17 @@ *} theorem bound_priority_inversion: - "occs (\ t'. th \ runing (t'@s)) t \ + "occs (\ t'. th \ running (t'@s)) t \ 1 + (length (actions_of blockers t) + length (filter (isCreate) t))" (is "?L \ ?R") proof - - let ?Q = "(\ t'. th \ runing (t'@s))" + let ?Q = "(\ t'. th \ running (t'@s))" from occs_le[of ?Q t] have "?L \ (1 + length t) - occs ?Q t" by simp also have "... \ ?R" proof - have "length t - (length (actions_of blockers t) + length (filter (isCreate) t)) - \ occs (\ t'. th \ runing (t'@s)) t" (is "?L1 \ ?R1") + \ occs (\ t'. th \ running (t'@s)) t" (is "?L1 \ ?R1") proof - have "?L1 = length (actions_of {th} t)" using actions_split by arith also have "... \ ?R1" using actions_th_occs by simp @@ -1400,12 +1400,12 @@ from ve'.blockers_no_create [OF assms _ this] have "\ isCreate e" by auto from PIP_actorE[OF h(2) otherwise this] - have "th' \ runing (t @ s)" . - moreover have "th' \ runing (t @ s)" + have "th' \ running (t @ s)" . + moreover have "th' \ running (t @ s)" proof - from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" . - from extend_highest_gen.detached_not_runing[OF h(3) this] assms + from extend_highest_gen.detached_not_running[OF h(3) this] assms show ?thesis by (auto simp:blockers_def) qed ultimately show False by simp @@ -1441,7 +1441,7 @@ blocked occurrences of the most urgent thread @{term th} is finitely bounded: *} theorem priority_inversion_is_finite: - "occs (\ t'. th \ runing (t'@s)) t \ + "occs (\ t'. th \ running (t'@s)) t \ 1 + ((\ th' \ blockers . span th') + BC)" (is "?L \ ?R" is "_ \ 1 + (?A + ?B)" ) proof - from bound_priority_inversion