# HG changeset patch # User Christian Urban # Date 1475415125 -3600 # Node ID 20c1d3a141437fdfb1209dc7da7ed57ecc183e1a # Parent 785c0f6b81840870c6af3b750464f746d96db693 updated diff -r 785c0f6b8184 -r 20c1d3a14143 Correctness.thy --- a/Correctness.thy Wed Aug 24 16:13:20 2016 +0200 +++ b/Correctness.thy Sun Oct 02 14:32:05 2016 +0100 @@ -5,6 +5,17 @@ text {* The following two auxiliary lemmas are used to reason about @{term Max}. *} + +lemma subset_Max: + assumes "finite A" + and "B \ A" + and "c \ B" + and "Max A = c" +shows "Max B = c" +using Max.subset assms +by (metis Max.coboundedI Max_eqI rev_finite_subset subset_eq) + + lemma image_Max_eqI: assumes "finite B" and "b \ B" @@ -101,7 +112,7 @@ locale extend_highest_gen = highest_gen + fixes t - assumes vt_t: "vt (t@s)" + assumes vt_t: "vt (t @ s)" and create_low: "Create th' prio' \ set t \ prio' \ prio" and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" and exit_diff: "Exit th' \ set t \ th' \ th" @@ -131,16 +142,6 @@ qed qed -(* locale red_extend_highest_gen = extend_highest_gen + - fixes i::nat -*) - -(* -sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" - apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) - apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) - by (unfold highest_gen_def, auto dest:step_back_vt_app) -*) context extend_highest_gen begin @@ -183,7 +184,7 @@ lemma th_kept: "th \ threads (t @ s) \ - preced th (t@s) = preced th s" (is "?Q t") + preced th (t @ s) = preced th s" (is "?Q t") proof - show ?thesis proof(induct rule:ind) @@ -246,7 +247,7 @@ qed text {* - According to @{thm th_kept}, thread @{text "th"} has its living status + According to @{thm th_kept}, thread @{text "th"} has its liveness status and precedence kept along the way of @{text "t"}. The following lemma shows that this preserved precedence of @{text "th"} remains as the highest along the way of @{text "t"}. @@ -260,7 +261,8 @@ 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" +lemma max_kept: + shows "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" proof(induct rule:ind) case Nil from highest_preced_thread @@ -723,9 +725,11 @@ 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 running}-thread. However, we are going to show more: this running thread - is exactly @{term "th'"}. - *} + 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 \ running (t @ s)" obtains th' where "th' \ ancestors (tG (t @ s)) th" @@ -744,9 +748,14 @@ -- {* 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)" + ultimately obtain th' where th'_readys: "th' \ readys (t @ s)" and dp: "(th, th') \ (tG (t @ s))\<^sup>+" by auto + -- {* @{text "th'"} is an ancestor of @{term "th"} *} + have "th' \ ancestors (tG (t @ s)) th" using dp + unfolding ancestors_def by simp + + moreover -- {* We are going to show that this @{term th'} is running. *} have "th' \ running (t @ s)" proof - @@ -756,6 +765,72 @@ -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), the @{term cp}-value of @{term th'} is the maximum of all precedences of all thread nodes in its @{term tRAG}-subtree: *} + + have "?L = Max (preceds (subtree (tG (t @ s)) th') (t @ s))" + unfolding cp_alt_def2 image_def the_preced_def by meson + also have "... = (preced th (t @ s))" + thm subset_Max + thm preced_unique + proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"]) + show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) + next + have "subtree (tG (t @ s)) th' \ threads (t @ s)" + using readys_def th'_readys vat_t.subtree_tG_thread by auto + then show "preceds (subtree (tG (t @ s)) th') (t @ s) \ preceds (threads (t @ s)) (t @ s)" + by auto + next + have "th \ subtree (tG (t @ s)) th'" + by (simp add: dp subtree_def trancl_into_rtrancl) + then show " preced th (t @ s) \ preceds (subtree (tG (t @ s)) th') (t @ s)" + by blast + next + have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" + apply(simp only: the_preced_def) + by simp + show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)" + thm th_kept max_kept + apply(simp del: th_kept) + apply(simp only: the_preced_def image_def) + apply(simp add: Bex_def_raw) + + qed + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . + qed + + -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, + it is @{term running} by definition. *} + then show "th' \ running (t @ s)" using th'_readys + unfolding running_def by simp + qed + + ultimately show ?thesis using that by metis +qed +*) + +lemma th_blockedE: (* ddd, the other main lemma to be presented: *) + obtains th' where "th' \ nancestors (tG (t @ s)) th" + "th' \ running (t @ s)" +proof - + -- {* According to @{thm vat_t.th_chain_to_ready}, there is a + ready ancestor of @{term th}. *} + have "\th' \ nancestors (tG (t @ s)) th. th' \ readys (t @ s)" + using th_kept vat_t.th_chain_to_ready_tG by auto + then obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "th' \ nancestors (tG (t @ s)) th" + by blast + + -- {* We are going to first show that this @{term th'} is running. *} + 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") + proof - + -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), + the @{term cp}-value of @{term th'} is the maximum of + all precedences of all thread nodes in its @{term tRAG}-subtree: *} have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))" by (unfold cp_alt_def2, simp) also have "... = (the_preced (t @ s) th)" @@ -765,80 +840,10 @@ show "subtree (tG (t @ s)) th' \ threads (t @ s)" using readys_def th'_in vat_t.subtree_tG_thread by auto next - show "th \ subtree (tG (t @ s)) th'" - by (simp add: dp subtree_def trancl_into_rtrancl) + show "th \ subtree (tG (t @ s)) th'" + using dp unfolding subtree_def nancestors_def2 by simp next - show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" - by simp - qed - also have "... = ?R" - using th_cp_max th_cp_preced th_kept - the_preced_def vat_t.max_cp_readys_threads by auto - finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . - qed - - -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, - 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}: *} - moreover have "th' \ ancestors (tG (t @ s)) th" - by (simp add: ancestors_def dp) - ultimately show ?thesis using that by metis -qed - -lemma (* new proof of th_blockedE *) - assumes "th \ running (t @ s)" - obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "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 "running"}. This would - violate our assumption. *} - have "th \ readys (t @ s)" - 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' \ 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") - proof - - -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), - the @{term cp}-value of @{term th'} is the maximum of - all precedences of all thread nodes in its @{term tRAG}-subtree: *} - have "?L = Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))" - proof - - have "(the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th') = - the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')" - by fastforce - thus ?thesis by (unfold cp_alt_def1, simp) - qed - also have "... = (the_preced (t @ s) th)" - proof(rule image_Max_subset) - show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) - next - show "the_thread ` subtree (tRAG (t @ s)) (Th th') \ threads (t @ s)" - by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in - the_thread.simps vat_t.subtree_tRAG_thread) - next - show "th \ the_thread ` subtree (tRAG (t @ s)) (Th th')" - proof - - have "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp - by (unfold tRAG_subtree_eq, auto simp:subtree_def) - thus ?thesis by force - qed - next - show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" + show " Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" by simp qed also have "... = ?R" @@ -849,24 +854,22 @@ -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, it is @{term running} by definition. *} - with `th' \ readys (t @ s)` show "th' \ running (t @ s)" by (simp add: running_def) + 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}: *} - moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" - using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) + moreover have "th' \ nancestors (tG (t @ s)) th" + using dp unfolding nancestors_def2 by simp ultimately show ?thesis using that by metis qed lemma th_blockedE_pretty: - assumes "th \ running (t @ s)" - shows "\th'. th' \ ancestors (tG (t @ s)) th \ th' \ running (t @ s)" + shows "\th' \ nancestors (tG (t @ s)) th. th' \ running (t @ s)" using th_blockedE assms by blast - - 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 @@ -874,14 +877,35 @@ thread is the @{text th'} given by lemma @{thm th_blockedE}. *} lemma live: "running (t @ s) \ {}" -proof(cases "th \ running (t @ s)") - case True thus ?thesis by auto -next - case False - thus ?thesis using th_blockedE by auto +using th_blockedE by auto + +lemma blockedE: + assumes "th \ running (t @ s)" + obtains th' where "th' \ nancestors (tG (t @ s)) th" + "th' \ running (t @ s)" + "th' \ threads s" + "\detached s th'" + "cp (t @ s) th' = preced th s" + "th' \ th" +proof - + obtain th' where a: "th' \ nancestors (tG (t @ s)) th" "th' \ running (t @ s)" + using th_blockedE by blast + moreover + from a(2) have b: "th' \ threads s" + using running_threads_inv assms by metis + moreover + from a(2) have "\detached s th'" + using running_inversion(2) assms by metis + moreover + from a(2) have "cp (t @ s) th' = preced th s" + using running_preced_inversion by blast + moreover + from a(2) have "th' \ th" using assms a(2) by blast + ultimately show ?thesis using that by metis qed -lemma blockedE: + +lemma nblockedE: assumes "th \ running (t @ s)" obtains th' where "th' \ ancestors (tG (t @ s)) th" "th' \ running (t @ s)" @@ -889,8 +913,9 @@ "\detached s th'" "cp (t @ s) th' = preced th s" "th' \ th" -using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE -by metis +using blockedE unfolding nancestors_def +using assms nancestors3 by auto + lemma detached_not_running: assumes "detached (t @ s) th'" diff -r 785c0f6b8184 -r 20c1d3a14143 Journal/Paper.thy --- a/Journal/Paper.thy Wed Aug 24 16:13:20 2016 +0200 +++ b/Journal/Paper.thy Sun Oct 02 14:32:05 2016 +0100 @@ -403,7 +403,7 @@ We also use the abbreviation \begin{isabelle}\ \ \ \ \ %%% - @{thm preceds_def} + ???%%@ { thm preceds_def} \end{isabelle} \noindent @@ -1070,6 +1070,13 @@ However, we are able to combine their two separate bounds into a single theorem improving their bound. + @{text "th_kept"} shows that th is a thread in s'-s + + \begin{proof}[of Theorem 1] + If @{term "th \ running (s' @ s)"}, then there is nothing to show. So let us + assume otherwise. + \end{proof} + In what follows we will describe properties of PIP that allow us to prove Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. Recall we want to prove that in state @{term "s' @ s"} diff -r 785c0f6b8184 -r 20c1d3a14143 PIPBasics.thy --- a/PIPBasics.thy Wed Aug 24 16:13:20 2016 +0200 +++ b/PIPBasics.thy Sun Oct 02 14:32:05 2016 +0100 @@ -3336,11 +3336,9 @@ context valid_trace begin -text {* - The first lemma is technical, which says out of any node - in the domain of @{term RAG}, - (no matter whether it is thread node or resource node) - there is a path leading to a ready thread. +text {* The first lemma is technical, which says out of any node in the +domain of @{term RAG} (no matter whether it is thread node or resource +node), there is a path leading to a ready thread. *} lemma chain_building: @@ -3409,12 +3407,15 @@ lemma th_chain_to_ready_tG: assumes th_in: "th \ threads s" - shows "th \ readys s \ (\ th'. th' \ readys s \ (th, th') \ (tG s)^+)" + shows "\th'\ nancestors (tG s) th. th' \ readys s" proof - from th_chain_to_ready[OF assms] show ?thesis - using dependants_alt_def1 dependants_alt_tG by blast -qed + using dependants_alt_def1 dependants_alt_tG + unfolding nancestors_def ancestors_def + by blast +qed + text {* The following lemma is a technical one to show diff -r 785c0f6b8184 -r 20c1d3a14143 PIPDefs.thy --- a/PIPDefs.thy Wed Aug 24 16:13:20 2016 +0200 +++ b/PIPDefs.thy Sun Oct 02 14:32:05 2016 +0100 @@ -125,7 +125,7 @@ definition preced :: "thread \ state \ precedence" where "preced th s \ Prc (priority th s) (last_set th s)" -definition preceds :: "thread set \ state \ precedence set" +abbreviation preceds :: "thread set \ state \ precedence set" where "preceds ths s \ {preced th s | th. th \ ths}" text {* @@ -227,7 +227,7 @@ lemma cpreced_def2: "cpreced wq s th \ Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th))" - unfolding cpreced_def image_def preceds_def + unfolding cpreced_def image_def apply(rule eq_reflection) apply(rule_tac f="Max" in arg_cong) by (auto) @@ -379,7 +379,7 @@ apply(rule ext) apply(simp add: cpreced_def) apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def) -apply(simp add: preced_def preceds_def) +apply(simp add: preced_def) done text {* diff -r 785c0f6b8184 -r 20c1d3a14143 RTree.thy --- a/RTree.thy Wed Aug 24 16:13:20 2016 +0200 +++ b/RTree.thy Sun Oct 02 14:32:05 2016 +0100 @@ -77,6 +77,27 @@ definition "ancestors r x = {y. (x, y) \ r^+}" +(* tmp *) +definition + "nancestors r x \ ancestors r x \ {x}" + +lemma nancestors_def2: + "nancestors r x \ {y. (x, y) \ r\<^sup>*}" +unfolding nancestors_def +apply(auto) +by (smt Collect_cong ancestors_def insert_compr mem_Collect_eq rtrancl_eq_or_trancl) + +lemma nancestors2: + "y \ ancestors r x \ y \ nancestors r x" +apply(auto simp add: nancestors_def) +done + +lemma nancestors3: + "\y \ nancestors r x; x \ y\ \ y \ ancestors r x" +apply(auto simp add: nancestors_def) +done +(* end tmp *) + definition "root r x = (ancestors r x = {})" lemma root_indep: diff -r 785c0f6b8184 -r 20c1d3a14143 journal.pdf Binary file journal.pdf has changed