# HG changeset patch # User Christian Urban # Date 1472048000 -7200 # Node ID 785c0f6b81840870c6af3b750464f746d96db693 # Parent fb3f52fe99d1f9a1a70091d7603503992c8639b3 updated diff -r fb3f52fe99d1 -r 785c0f6b8184 Correctness.thy --- a/Correctness.thy Tue Aug 16 11:49:37 2016 +0100 +++ b/Correctness.thy Wed Aug 24 16:13:20 2016 +0200 @@ -727,68 +727,64 @@ is exactly @{term "th'"}. *} lemma th_blockedE: (* ddd, the other main lemma to be presented: *) - assumes "th \ running (t@s)" - obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ running (t@s)" + assumes "th \ running (t @ s)" + obtains th' where "th' \ ancestors (tG (t @ s)) th" + "th' \ running (t @ s)" proof - - -- {* According to @{thm vat_t.th_chain_to_ready}, either + -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either @{term "th"} is in @{term "readys"} or there is path leading from it to one thread in @{term "readys"}. *} - 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 + have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (th, th') \ (tG (t @ s))\<^sup>+)" + using th_kept vat_t.th_chain_to_ready_tG by blast + -- {* However, @{term th} can not be in @{term readys}, because otherwise, since - @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *} - moreover have "th \ readys (t@s)" + @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *} + moreover have "th \ readys (t @ s)" 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 + ultimately obtain th' where th'_in: "th' \ readys (t @ s)" + and dp: "(th, th') \ (tG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} - have "th' \ running (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") + 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'))" - by (unfold cp_alt_def1, simp) - also have "... = (the_preced (t @ s) \ the_thread) (Th th)" + 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)" proof(rule image_Max_subset) - 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.rg_RAG_threads vat_t.subtree_tRAG_thread) + show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) next - show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp - by (unfold tRAG_subtree_eq, auto simp:subtree_def) + show "subtree (tG (t @ s)) th' \ threads (t @ s)" + using readys_def th'_in vat_t.subtree_tG_thread by auto next - show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = - (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") - proof - - have "?L = the_preced (t @ s) ` threads (t @ s)" - by (unfold image_comp, rule image_cong, auto) - thus ?thesis using max_preced the_preced_def by auto - qed + show "th \ subtree (tG (t @ s)) th'" + by (simp add: dp subtree_def trancl_into_rtrancl) + next + show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" + by simp qed - thm the_preced_def also have "... = ?R" using th_cp_max th_cp_preced th_kept the_preced_def vat_t.max_cp_readys_threads by auto - thm th_cp_max th_cp_preced th_kept - the_preced_def vat_t.max_cp_readys_threads - finally show ?thesis . + finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . qed - -- {* Now, since @{term th'} holds the highest @{term cp} - and we have already show it is in @{term readys}, + + -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, it is @{term running} by definition. *} - with `th' \ readys (t@s)` show ?thesis 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' \ ancestors (tG (t @ s)) th" + by (simp add: ancestors_def dp) ultimately show ?thesis using that by metis qed @@ -863,18 +859,22 @@ qed lemma th_blockedE_pretty: - 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 + assumes "th \ running (t @ s)" + shows "\th'. th' \ ancestors (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 + 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: "running (t@s) \ {}" -proof(cases "th \ running (t@s)") +lemma live: "running (t @ s) \ {}" +proof(cases "th \ running (t @ s)") case True thus ?thesis by auto next case False @@ -882,19 +882,20 @@ qed lemma blockedE: - assumes "th \ running (t@s)" - obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ running (t@s)" + assumes "th \ running (t @ s)" + obtains th' where "th' \ ancestors (tG (t @ s)) th" + "th' \ running (t @ s)" "th' \ threads s" "\detached s th'" - "cp (t@s) th' = preced th s" + "cp (t @ s) th' = preced th s" "th' \ th" -by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE) +using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE +by metis lemma detached_not_running: - assumes "detached (t@s) th'" + assumes "detached (t @ s) th'" and "th' \ th" - shows "th' \ running (t@s)" + shows "th' \ running (t @ s)" proof assume otherwise: "th' \ running (t @ s)" have "cp (t@s) th' = cp (t@s) th" @@ -920,19 +921,21 @@ section {* The correctness theorem of PIP *} text {* - In this section, we identify two more conditions in addition to the ones already - specified in the forgoing locales, based on which the correctness of PIP is - formally proved. + + In this section, we identify two more conditions in addition to the ones + already specified in the current locale, based on which the correctness + of PIP is formally proved. - Note that Priority Inversion refers to the phenomenon where the thread with highest priority - is blocked by one with lower priority because the resource it is requesting is - currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion}, - i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large. + Note that Priority Inversion refers to the phenomenon where the thread + with highest priority is blocked by one with lower priority because the + resource it is requesting is currently held by the later. The objective of + PIP is to avoid {\em Indefinite Priority Inversion}, i.e. the number of + occurrences of {\em Priority Inversion} becomes indefinitely large. - For PIP to be correct, a finite upper bound needs to be found for the occurrence number, - and the existence. This section makes explicit two more conditions so that the existence - of such a upper bound can be proved to exist. -*} + For PIP to be correct, a finite upper bound needs to be found for the + occurrence number, and the existence. This section makes explicit two more + conditions so that the existence of such a upper bound can be proved to + exist. *} text {* The following set @{text "blockers"} characterizes the set of threads which diff -r fb3f52fe99d1 -r 785c0f6b8184 Journal/Paper.thy --- a/Journal/Paper.thy Tue Aug 16 11:49:37 2016 +0100 +++ b/Journal/Paper.thy Wed Aug 24 16:13:20 2016 +0200 @@ -873,6 +873,55 @@ properties that show our model of PIP is correct. *} +section {* Preliminaries *} + +(*<*) +context valid_trace +begin +(*>*) +text {* + + In this section we prove facts that immediately follow from + our definitions of valid traces. + + \begin{lemma}??\label{precedunique} + @{thm [mode=IfThen] preced_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]} + \end{lemma} + + + We can verify that in any valid state, there can only be at most + one running thread---if there are more than one running thread, + say @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, they must be + equal. + + \begin{lemma} + @{thm [mode=IfThen] running_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]} + \end{lemma} + + \begin{proof} + Since @{text "th\<^sub>1"} and @{text "th\<^sub>2"} are running, they must be + roots in the RAG. + According to XXX, there exists a chain in the RAG-subtree of @{text "th\<^sub>1"}, + say starting from @{text "th'\<^sub>1"}, such that @{text "th'\<^sub>1"} has the + highest precedence in this subtree (@{text "th\<^sub>1"} inherited + the precedence of @{text "th'\<^sub>1"}). We have a similar chain starting from, say + @{text "th'\<^sub>2"}, in the RAG-subtree of @{text "th\<^sub>2"}. Since @{text "th\<^sub>1"} + and @{text "th\<^sub>2"} are running we know their cp-value must be the same, that is + \begin{center} + @{term "cp s th\<^sub>1 = cp s th\<^sub>2"} + \end{center} + + \noindent + That means the precedences of @{text "th'\<^sub>1"} and @{text "th'\<^sub>2"} + must be the same (they are the maxima in the respective RAG-subtrees). From this we can + infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"} + and @{text "th'\<^sub>2"} are the same threads. However, this also means the + roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed + \end{proof} + + *} +(*<*)end(*>*) + section {* The Correctness Proof *} (*<*) diff -r fb3f52fe99d1 -r 785c0f6b8184 PIPBasics.thy --- a/PIPBasics.thy Tue Aug 16 11:49:37 2016 +0100 +++ b/PIPBasics.thy Wed Aug 24 16:13:20 2016 +0200 @@ -920,6 +920,8 @@ "dependants s th = {th'. th \ ancestors (tG s) th'}" by (unfold dependants_alt_tG ancestors_def, simp) + + section {* Locales used to investigate the execution of PIP *} text {* @@ -3459,6 +3461,36 @@ qed qed +lemma root_readys: + assumes "th \ readys s" + shows "root (tRAG s) (Th th)" +proof - + { assume "\ root (tRAG s) (Th th)" + then obtain n' where "(Th th, n') \ (tRAG s)^+" + unfolding root_def ancestors_def by auto + then obtain cs where "(Th th, Cs cs) \ RAG s" + unfolding tRAG_alt_def using tranclD by fastforce + then have "th \ readys s" + unfolding readys_def using in_RAG_E by blast + with assms have False by simp + } then show "root (tRAG s) (Th th)" by auto +qed + +lemma root_readys_tG: + assumes "th \ readys s" + shows "root (tG s) th" +proof - + { assume "\ root (tG s) th" + then obtain th' where "(th, th') \ (tG s)^+" + unfolding root_def ancestors_def by auto + then have "(Th th, Th th') \ (tRAG s)^+" + using trancl_tG_tRAG by simp + with root_readys assms + have False + unfolding root_def ancestors_def by auto + } then show "root (tG s) th" by auto +qed + lemma readys_indep: assumes "th1 \ readys s" and "th2 \ readys s" @@ -3509,191 +3541,67 @@ The following two lemmas shows there is at most one running thread in the system. *} + + lemma running_unique: assumes running_1: "th1 \ running s" and running_2: "th2 \ running s" shows "th1 = th2" proof - - -- {* According to lemma @{thm thread_chain}, - each living threads is chained to a thread in its subtree, and this - target thread holds the highest precedence of the subtree. - - The chains for @{term th1} and @{term th2} are established - first in the following in @{text "h1"} and @{text "h2"}: - *} + -- {* + + According to lemma @{thm thread_chain}, each live thread is chained to a + thread in its subtree, who holds the highest precedence of the subtree. + + The chains for @{term th1} and @{term th2} are established first in the + following in @{text "chain1"} and @{text "chain2"}. These chains start + with the threads @{text "th1'"} and @{text "th2'"} respectively. *} + have "th1 \ threads s" using assms by (unfold running_def readys_def, auto) - from thread_chain[OF this] + with thread_chain obtain th1' where - h1: "th1' \ subtree (tG s) th1" + chain1: "th1' \ subtree (tG s) th1" "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)" "th1' \ threads s" by auto have "th2 \ threads s" using assms by (unfold running_def readys_def, auto) - from thread_chain[OF this] + with thread_chain obtain th2' where - h2: "th2' \ subtree (tG s) th2" + chain2: "th2' \ subtree (tG s) th2" "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)" "th2' \ threads s" by auto - -- {* It can be proved that the chained thread for @{term th1} and @{term th2} - must be equal: + -- {* From these two chains we can be prove that the threads + @{term th1} and @{term th2} must be equal. For this we first + show that the starting points of the chains are equal. *} have eq_th': "th1' = th2'" proof - - have "the_preced s th1' = the_preced s th2'" - proof - - from running_1 and running_2 have "cp s th1 = cp s th2" - unfolding running_def by auto - from this[unfolded cp_alt_def2] - have eq_max: "Max (the_preced s ` subtree (tG s) th1) = - Max (the_preced s ` subtree (tG s) th2)" . - with h1(2) h2(2) - show ?thesis by metis - qed - from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)] - show ?thesis . - qed - -- {* From this, it can be derived that the two sub-trees - rooted by @{term th1} and @{term th2} must overlap: *} - have overlapping: "th1' \ subtree (tG s) th1 \ subtree (tG s) th2" - using eq_th' h1(1) h2(1) by auto - -- {* However, this would be in contradiction with the fact - that two independent sub-trees can not overlap, - if @{term "th1 \ th2"} (therefore, each roots an independent sub-trees). - Therefore, @{term th1} and @{term th2} must be equal. - *} - { assume neq: "th1 \ th2" - -- {* According to @{thm readys_indep_tG}, two different threads - in ready queue must be independent with each other: *} - have "indep (tG s) th1 th2" - by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def) - -- {* Therefore, according to lemma @{thm subtree_disjoint}, - the two sub-trees rooted by them can not overlap: - *} - from subtree_disjoint[OF this] - have "subtree (tG s) th1 \ subtree (tG s) th2 = {}" . - -- {* In contradiction with @{thm overlapping}: *} - with overlapping have False by auto - } thus ?thesis by auto -qed - -text {* - The following two lemmas shows there is at most one running thread - in the system. -*} -lemma running_unique_old: - assumes running_1: "th1 \ running s" - and running_2: "th2 \ running s" - shows "th1 = th2" -proof - - from running_1 and running_2 have "cp s th1 = cp s th2" - unfolding running_def by auto - from this[unfolded cp_alt_def] - have eq_max: - "Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th1)}) = - Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th2)})" - (is "Max ?L = Max ?R") . - have "Max ?L \ ?L" - proof(rule Max_in) - show "finite ?L" by (simp add: finite_subtree_threads) - next - show "?L \ {}" using subtree_def by fastforce - qed - then obtain th1' where - h_1: "Th th1' \ subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L" - by auto - have "Max ?R \ ?R" - proof(rule Max_in) - show "finite ?R" by (simp add: finite_subtree_threads) - next - show "?R \ {}" using subtree_def by fastforce + -- {* from @{text th1} and @{text th2} running, we know their + cp-value is the same *} + from running_1 and running_2 have "cp s th1 = cp s th2" + unfolding running_def by auto + -- {* that means the preced of @{text th1'} and @{text th2'} + must be the same *} + then + have eq_max: "Max (the_preced s ` subtree (tG s) th1) = + Max (the_preced s ` subtree (tG s) th2)" + unfolding cp_alt_def2 . + with chain1(2) chain2(2) + have "the_preced s th1' = the_preced s th2'" by simp + -- {* since the precedences are the same, we can conclude + that @{text th1'} and @{text th2'} are the same *} + with preced_unique chain1(3) chain2(3) + show "th1' = th2'" unfolding the_preced_def by auto qed - then obtain th2' where - h_2: "Th th2' \ subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R" - by auto - have "th1' = th2'" - proof(rule preced_unique) - from h_1(1) - show "th1' \ threads s" - proof(cases rule:subtreeE) - case 1 - hence "th1' = th1" by simp - with running_1 show ?thesis by (auto simp:running_def readys_def) - next - case 2 - from this(2) - have "(Th th1', Th th1) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - have "(Th th1') \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] show ?thesis . - qed - next - from h_2(1) - show "th2' \ threads s" - proof(cases rule:subtreeE) - case 1 - hence "th2' = th2" by simp - with running_2 show ?thesis by (auto simp:running_def readys_def) - next - case 2 - from this(2) - have "(Th th2', Th th2) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - have "(Th th2') \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] show ?thesis . - qed - next - have "the_preced s th1' = the_preced s th2'" - using eq_max h_1(2) h_2(2) by metis - thus "preced th1' s = preced th2' s" by (simp add:the_preced_def) - qed - from h_1(1)[unfolded this] - have star1: "(Th th2', Th th1) \ (RAG s)^*" by (auto simp:subtree_def) - from h_2(1)[unfolded this] - have star2: "(Th th2', Th th2) \ (RAG s)^*" by (auto simp:subtree_def) - from star_rpath[OF star1] obtain xs1 - where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)" - by auto - from star_rpath[OF star2] obtain xs2 - where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)" - by auto - from rp1 rp2 - show ?thesis - proof(cases) - case (less_1 xs') - moreover have "xs' = []" - proof(rule ccontr) - assume otherwise: "xs' \ []" - from rpath_plus[OF less_1(3) this] - have "(Th th1, Th th2) \ (RAG s)\<^sup>+" . - from tranclD[OF this] - obtain cs where "waiting s th1 cs" - by (unfold s_RAG_def, fold s_waiting_abv, auto) - with running_1 show False - by (unfold running_def readys_def, auto) - qed - ultimately have "xs2 = xs1" by simp - from rpath_dest_eq[OF rp1 rp2[unfolded this]] - show ?thesis by simp - next - case (less_2 xs') - moreover have "xs' = []" - proof(rule ccontr) - assume otherwise: "xs' \ []" - from rpath_plus[OF less_2(3) this] - have "(Th th2, Th th1) \ (RAG s)\<^sup>+" . - from tranclD[OF this] - obtain cs where "waiting s th2 cs" - by (unfold s_RAG_def, fold s_waiting_abv, auto) - with running_2 show False - by (unfold running_def readys_def, auto) - qed - ultimately have "xs2 = xs1" by simp - from rpath_dest_eq[OF rp1 rp2[unfolded this]] - show ?thesis by simp - qed + moreover + have "root (tG s) th1" "root (tG s) th2" using assms + using assms root_readys_tG + unfolding running_def by auto + ultimately show "th1 = th2" using root_unique chain1(1) chain2(1) + by fastforce qed lemma card_running: diff -r fb3f52fe99d1 -r 785c0f6b8184 RTree.thy --- a/RTree.thy Tue Aug 16 11:49:37 2016 +0100 +++ b/RTree.thy Wed Aug 24 16:13:20 2016 +0200 @@ -73,12 +73,28 @@ nodes (including itself) which can reach @{text "x"} by following some path in @{text "r"}: *} -definition "subtree r x = {node' . (node', x) \ r^*}" +definition "subtree r x = {y . (y, x) \ r^*}" -definition "ancestors r x = {node'. (x, node') \ r^+}" +definition "ancestors r x = {y. (x, y) \ r^+}" definition "root r x = (ancestors r x = {})" +lemma root_indep: + assumes "root r x" + and "root r y" + and "y \ x" + shows "indep r x y" +proof - + { assume "(x, y) \ r^*" + hence False using assms + by (unfold root_def ancestors_def, auto dest:tranclD rtranclD) + } moreover { + assume "(y, x) \ r^*" + hence False using assms + by (unfold root_def ancestors_def, auto dest:tranclD rtranclD) + } ultimately show ?thesis by (auto simp:indep_def) +qed + text {* The following @{text "edge_in r x"} is the set of edges contained in @@ -108,7 +124,7 @@ shows "(a, b) \ edges_in r x" using assms by (unfold edges_in_def subtree_def, auto) -definition "children r x = {node'. (node', x) \ r}" +definition "children r x = {y. (y, x) \ r}" locale fforest = forest + assumes fb: "finite (children r x)" @@ -1067,6 +1083,21 @@ } thus ?thesis by auto qed +lemma root_unique: + assumes "x \ subtree r y" + and "x \ subtree r z" + and "root r y" + and "root r z" + shows "y = z" +proof - + { assume "y \ z" + from root_indep[OF assms(4,3) this] + have "indep r z y" . + from subtree_disjoint[OF this] and assms + have False by auto + } thus ?thesis by auto +qed + text {* The following lemma @{text "subtree_del"} characterizes the change of sub-tree of @{text "x"} with the removal of an inside edge @{text "(a, b)"}. diff -r fb3f52fe99d1 -r 785c0f6b8184 journal.pdf Binary file journal.pdf has changed