4 *} |
4 *} |
5 theory CpsG |
5 theory CpsG |
6 imports PrioG Max RTree |
6 imports PrioG Max RTree |
7 begin |
7 begin |
8 |
8 |
|
9 definition "the_preced s th = preced th s" |
|
10 |
|
11 fun the_thread :: "node \<Rightarrow> thread" where |
|
12 "the_thread (Th th) = th" |
|
13 |
9 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" |
14 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" |
10 |
15 |
11 definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" |
16 definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" |
12 |
17 |
13 definition "tRAG s = wRAG s O hRAG s" |
18 definition "tRAG s = wRAG s O hRAG s" |
|
19 |
|
20 definition "cp_gen s x = |
|
21 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
|
22 (* ccc *) |
14 |
23 |
15 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" |
24 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" |
16 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv |
25 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv |
17 s_holding_abv cs_RAG_def, auto) |
26 s_holding_abv cs_RAG_def, auto) |
18 |
27 |
124 by (unfold eq_n tRAG_alt_def, auto) |
133 by (unfold eq_n tRAG_alt_def, auto) |
125 qed |
134 qed |
126 } ultimately show ?thesis by auto |
135 } ultimately show ?thesis by auto |
127 qed |
136 qed |
128 |
137 |
129 lemma readys_root: |
|
130 assumes "vt s" |
|
131 and "th \<in> readys s" |
|
132 shows "root (RAG s) (Th th)" |
|
133 proof - |
|
134 { fix x |
|
135 assume "x \<in> ancestors (RAG s) (Th th)" |
|
136 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
137 from tranclD[OF this] |
|
138 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
139 with assms(2) have False |
|
140 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
141 by (fold wq_def, blast) |
|
142 } thus ?thesis by (unfold root_def, auto) |
|
143 qed |
|
144 |
|
145 lemma readys_in_no_subtree: |
|
146 assumes "vt s" |
|
147 and "th \<in> readys s" |
|
148 and "th' \<noteq> th" |
|
149 shows "Th th \<notin> subtree (RAG s) (Th th')" |
|
150 proof |
|
151 assume "Th th \<in> subtree (RAG s) (Th th')" |
|
152 thus False |
|
153 proof(cases rule:subtreeE) |
|
154 case 1 |
|
155 with assms show ?thesis by auto |
|
156 next |
|
157 case 2 |
|
158 with readys_root[OF assms(1,2)] |
|
159 show ?thesis by (auto simp:root_def) |
|
160 qed |
|
161 qed |
|
162 |
|
163 lemma image_id: |
|
164 assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x" |
|
165 shows "f ` A = A" |
|
166 using assms by (auto simp:image_def) |
|
167 |
|
168 definition "the_preced s th = preced th s" |
|
169 |
|
170 lemma cp_alt_def: |
138 lemma cp_alt_def: |
171 "cp s th = |
139 "cp s th = |
172 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
140 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
173 proof - |
141 proof - |
174 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = |
142 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = |
219 qed |
181 qed |
220 with that show ?thesis by auto |
182 with that show ?thesis by auto |
221 qed |
183 qed |
222 qed |
184 qed |
223 |
185 |
224 lemma threads_set_eq: |
186 lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*" |
225 "the_thread ` (subtree (tRAG s) (Th th)) = |
187 proof - |
226 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") |
188 have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" |
227 proof - |
189 by (rule rtrancl_mono, auto simp:RAG_split) |
228 { fix th' |
190 also have "... \<subseteq> ((RAG s)^*)^*" |
229 assume "th' \<in> ?L" |
191 by (rule rtrancl_mono, auto) |
230 then obtain n where h: "th' = the_thread n" "n \<in> subtree (tRAG s) (Th th)" by auto |
192 also have "... = (RAG s)^*" by simp |
231 from subtree_nodeE[OF this(2)] |
193 finally show ?thesis by (unfold tRAG_def, simp) |
232 obtain th1 where "n = Th th1" by auto |
194 qed |
233 with h have "Th th' \<in> subtree (tRAG s) (Th th)" by auto |
195 |
234 hence "Th th' \<in> subtree (RAG s) (Th th)" |
196 lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x" |
235 proof(cases rule:subtreeE[consumes 1]) |
197 proof - |
236 case 1 |
198 { fix a |
237 thus ?thesis by (auto simp:subtree_def) |
199 assume "a \<in> subtree (tRAG s) x" |
238 next |
200 hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def) |
239 case 2 |
201 with tRAG_star_RAG[of s] |
240 hence "(Th th', Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def) |
202 have "(a, x) \<in> (RAG s)^*" by auto |
241 thus ?thesis |
203 hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def) |
242 proof(induct) |
204 } thus ?thesis by auto |
243 case (step y z) |
205 qed |
244 from this(2)[unfolded tRAG_alt_def] |
206 |
245 obtain u where |
207 lemma tRAG_subtree_eq: |
246 h: "(y, u) \<in> RAG s" "(u, z) \<in> RAG s" |
208 "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}" |
247 by auto |
209 (is "?L = ?R") |
248 hence "y \<in> subtree (RAG s) z" by (auto simp:subtree_def) |
210 proof - |
249 with step(3) |
211 { fix n |
250 show ?case by (auto simp:subtree_def) |
212 assume "n \<in> ?L" |
251 next |
213 with subtree_nodeE[OF this] |
252 case (base y) |
214 obtain th' where "n = Th th'" "Th th' \<in> subtree (tRAG s) (Th th)" by auto |
253 from this[unfolded tRAG_alt_def] |
215 with tRAG_subtree_RAG[of s "Th th"] |
254 show ?case by (auto simp:subtree_def) |
216 have "n \<in> ?R" by auto |
255 qed |
|
256 qed |
|
257 hence "th' \<in> ?R" by auto |
|
258 } moreover { |
217 } moreover { |
259 fix th' |
218 fix n |
260 assume "th' \<in> ?R" |
219 assume "n \<in> ?R" |
261 hence "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def) |
220 then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" |
262 from star_rpath[OF this] |
221 by (auto simp:subtree_def) |
|
222 from star_rpath[OF this(2)] |
263 obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto |
223 obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto |
264 hence "Th th' \<in> subtree (tRAG s) (Th th)" |
224 hence "Th th' \<in> subtree (tRAG s) (Th th)" |
265 proof(induct xs arbitrary:th' th rule:length_induct) |
225 proof(induct xs arbitrary:th' th rule:length_induct) |
266 case (1 xs th' th) |
226 case (1 xs th' th) |
267 show ?case |
227 show ?case |
342 obtain th where eq_a: "a = Th th" by auto |
306 obtain th where eq_a: "a = Th th" by auto |
343 show "cp_gen s a = (cp s \<circ> the_thread) a" |
307 show "cp_gen s a = (cp s \<circ> the_thread) a" |
344 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
308 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
345 qed |
309 qed |
346 |
310 |
347 |
|
348 |
|
349 locale valid_trace = |
311 locale valid_trace = |
350 fixes s |
312 fixes s |
351 assumes vt : "vt s" |
313 assumes vt : "vt s" |
352 |
314 |
353 context valid_trace |
315 context valid_trace |
354 begin |
316 begin |
|
317 |
|
318 lemma readys_root: |
|
319 assumes "th \<in> readys s" |
|
320 shows "root (RAG s) (Th th)" |
|
321 proof - |
|
322 { fix x |
|
323 assume "x \<in> ancestors (RAG s) (Th th)" |
|
324 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
325 from tranclD[OF this] |
|
326 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
327 with assms(1) have False |
|
328 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
329 by (fold wq_def, blast) |
|
330 } thus ?thesis by (unfold root_def, auto) |
|
331 qed |
|
332 |
|
333 lemma readys_in_no_subtree: |
|
334 assumes "th \<in> readys s" |
|
335 and "th' \<noteq> th" |
|
336 shows "Th th \<notin> subtree (RAG s) (Th th')" |
|
337 proof |
|
338 assume "Th th \<in> subtree (RAG s) (Th th')" |
|
339 thus False |
|
340 proof(cases rule:subtreeE) |
|
341 case 1 |
|
342 with assms show ?thesis by auto |
|
343 next |
|
344 case 2 |
|
345 with readys_root[OF assms(1)] |
|
346 show ?thesis by (auto simp:root_def) |
|
347 qed |
|
348 qed |
355 |
349 |
356 lemma not_in_thread_isolated: |
350 lemma not_in_thread_isolated: |
357 assumes "th \<notin> threads s" |
351 assumes "th \<notin> threads s" |
358 shows "(Th th) \<notin> Field (RAG s)" |
352 shows "(Th th) \<notin> Field (RAG s)" |
359 proof |
353 proof |
564 qed |
558 qed |
565 qed |
559 qed |
566 |
560 |
567 end |
561 end |
568 |
562 |
569 |
563 (* ccc *) |
570 lemma eq_dependants: "dependants (wq s) = dependants s" |
564 |
571 by (simp add: s_dependants_abv wq_def) |
565 |
572 |
|
573 |
566 |
574 (* obvious lemma *) |
567 (* obvious lemma *) |
575 lemma not_thread_holdents: |
|
576 fixes th s |
|
577 assumes vt: "vt s" |
|
578 and not_in: "th \<notin> threads s" |
|
579 shows "holdents s th = {}" |
|
580 proof - |
|
581 from vt not_in show ?thesis |
|
582 proof(induct arbitrary:th) |
|
583 case (vt_cons s e th) |
|
584 assume vt: "vt s" |
|
585 and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}" |
|
586 and stp: "step s e" |
|
587 and not_in: "th \<notin> threads (e # s)" |
|
588 from stp show ?case |
|
589 proof(cases) |
|
590 case (thread_create thread prio) |
|
591 assume eq_e: "e = Create thread prio" |
|
592 and not_in': "thread \<notin> threads s" |
|
593 have "holdents (e # s) th = holdents s th" |
|
594 apply (unfold eq_e holdents_test) |
|
595 by (simp add:RAG_create_unchanged) |
|
596 moreover have "th \<notin> threads s" |
|
597 proof - |
|
598 from not_in eq_e show ?thesis by simp |
|
599 qed |
|
600 moreover note ih ultimately show ?thesis by auto |
|
601 next |
|
602 case (thread_exit thread) |
|
603 assume eq_e: "e = Exit thread" |
|
604 and nh: "holdents s thread = {}" |
|
605 show ?thesis |
|
606 proof(cases "th = thread") |
|
607 case True |
|
608 with nh eq_e |
|
609 show ?thesis |
|
610 by (auto simp:holdents_test RAG_exit_unchanged) |
|
611 next |
|
612 case False |
|
613 with not_in and eq_e |
|
614 have "th \<notin> threads s" by simp |
|
615 from ih[OF this] False eq_e show ?thesis |
|
616 by (auto simp:holdents_test RAG_exit_unchanged) |
|
617 qed |
|
618 next |
|
619 case (thread_P thread cs) |
|
620 assume eq_e: "e = P thread cs" |
|
621 and is_runing: "thread \<in> runing s" |
|
622 from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto |
|
623 have neq_th: "th \<noteq> thread" |
|
624 proof - |
|
625 from not_in eq_e have "th \<notin> threads s" by simp |
|
626 moreover from is_runing have "thread \<in> threads s" |
|
627 by (simp add:runing_def readys_def) |
|
628 ultimately show ?thesis by auto |
|
629 qed |
|
630 hence "holdents (e # s) th = holdents s th " |
|
631 apply (unfold cntCS_def holdents_test eq_e) |
|
632 by (unfold step_RAG_p[OF vtp], auto) |
|
633 moreover have "holdents s th = {}" |
|
634 proof(rule ih) |
|
635 from not_in eq_e show "th \<notin> threads s" by simp |
|
636 qed |
|
637 ultimately show ?thesis by simp |
|
638 next |
|
639 case (thread_V thread cs) |
|
640 assume eq_e: "e = V thread cs" |
|
641 and is_runing: "thread \<in> runing s" |
|
642 and hold: "holding s thread cs" |
|
643 have neq_th: "th \<noteq> thread" |
|
644 proof - |
|
645 from not_in eq_e have "th \<notin> threads s" by simp |
|
646 moreover from is_runing have "thread \<in> threads s" |
|
647 by (simp add:runing_def readys_def) |
|
648 ultimately show ?thesis by auto |
|
649 qed |
|
650 from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto |
|
651 from hold obtain rest |
|
652 where eq_wq: "wq s cs = thread # rest" |
|
653 by (case_tac "wq s cs", auto simp: wq_def s_holding_def) |
|
654 from not_in eq_e eq_wq |
|
655 have "\<not> next_th s thread cs th" |
|
656 apply (auto simp:next_th_def) |
|
657 proof - |
|
658 assume ne: "rest \<noteq> []" |
|
659 and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s") |
|
660 have "?t \<in> set rest" |
|
661 proof(rule someI2) |
|
662 from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq |
|
663 show "distinct rest \<and> set rest = set rest" by auto |
|
664 next |
|
665 fix x assume "distinct x \<and> set x = set rest" with ne |
|
666 show "hd x \<in> set rest" by (cases x, auto) |
|
667 qed |
|
668 with eq_wq have "?t \<in> set (wq s cs)" by simp |
|
669 from wq_threads[OF step_back_vt[OF vtv], OF this] and ni |
|
670 show False by auto |
|
671 qed |
|
672 moreover note neq_th eq_wq |
|
673 ultimately have "holdents (e # s) th = holdents s th" |
|
674 by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) |
|
675 moreover have "holdents s th = {}" |
|
676 proof(rule ih) |
|
677 from not_in eq_e show "th \<notin> threads s" by simp |
|
678 qed |
|
679 ultimately show ?thesis by simp |
|
680 next |
|
681 case (thread_set thread prio) |
|
682 print_facts |
|
683 assume eq_e: "e = Set thread prio" |
|
684 and is_runing: "thread \<in> runing s" |
|
685 from not_in and eq_e have "th \<notin> threads s" by auto |
|
686 from ih [OF this] and eq_e |
|
687 show ?thesis |
|
688 apply (unfold eq_e cntCS_def holdents_test) |
|
689 by (simp add:RAG_set_unchanged) |
|
690 qed |
|
691 next |
|
692 case vt_nil |
|
693 show ?case |
|
694 by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) |
|
695 qed |
|
696 qed |
|
697 |
|
698 (* obvious lemma *) |
|
699 lemma next_th_neq: |
|
700 assumes vt: "vt s" |
|
701 and nt: "next_th s th cs th'" |
|
702 shows "th' \<noteq> th" |
|
703 proof - |
|
704 from nt show ?thesis |
|
705 apply (auto simp:next_th_def) |
|
706 proof - |
|
707 fix rest |
|
708 assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest" |
|
709 and ne: "rest \<noteq> []" |
|
710 have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" |
|
711 proof(rule someI2) |
|
712 from wq_distinct[OF vt, of cs] eq_wq |
|
713 show "distinct rest \<and> set rest = set rest" by auto |
|
714 next |
|
715 fix x |
|
716 assume "distinct x \<and> set x = set rest" |
|
717 hence eq_set: "set x = set rest" by auto |
|
718 with ne have "x \<noteq> []" by auto |
|
719 hence "hd x \<in> set x" by auto |
|
720 with eq_set show "hd x \<in> set rest" by auto |
|
721 qed |
|
722 with wq_distinct[OF vt, of cs] eq_wq show False by auto |
|
723 qed |
|
724 qed |
|
725 |
|
726 (* obvious lemma *) |
|
727 lemma next_th_unique: |
|
728 assumes nt1: "next_th s th cs th1" |
|
729 and nt2: "next_th s th cs th2" |
|
730 shows "th1 = th2" |
|
731 using assms by (unfold next_th_def, auto) |
|
732 |
568 |
733 lemma wf_RAG: |
569 lemma wf_RAG: |
734 assumes vt: "vt s" |
570 assumes vt: "vt s" |
735 shows "wf (RAG s)" |
571 shows "wf (RAG s)" |
736 proof(rule finite_acyclic_wf) |
572 proof(rule finite_acyclic_wf) |
2037 qed auto |
1873 qed auto |
2038 have neq_th_a: "th_a \<noteq> th" |
1874 have neq_th_a: "th_a \<noteq> th" |
2039 proof - |
1875 proof - |
2040 from readys_in_no_subtree[OF vat_s'.vt th_ready assms] |
1876 from readys_in_no_subtree[OF vat_s'.vt th_ready assms] |
2041 have "(Th th) \<notin> subtree (RAG s') (Th th')" . |
1877 have "(Th th) \<notin> subtree (RAG s') (Th th')" . |
2042 find_theorems subtree tRAG RAG (* ccc *) |
1878 with tRAG_subtree_RAG[of s' "Th th'"] |
2043 proof |
1879 have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto |
2044 assume "Th th \<in> subtree (tRAG s') (Th th')" |
|
2045 thus False |
|
2046 proof(cases rule:subtreeE) |
|
2047 case 2 |
|
2048 from ancestors_Field[OF this(2)] |
|
2049 and th_tRAG[unfolded Field_def] |
|
2050 show ?thesis by auto |
|
2051 qed (insert assms, auto) |
|
2052 qed |
|
2053 with a_in[unfolded eq_a] show ?thesis by auto |
1880 with a_in[unfolded eq_a] show ?thesis by auto |
2054 qed |
1881 qed |
2055 from preced_kept[OF this] |
1882 from preced_kept[OF this] |
2056 show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a" |
1883 show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a" |
2057 by (unfold eq_a, simp) |
1884 by (unfold eq_a, simp) |