77 by (unfold vat_s.cp_rec, rule Max_ge, |
77 by (unfold vat_s.cp_rec, rule Max_ge, |
78 auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) |
78 auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) |
79 ultimately show ?thesis by auto |
79 ultimately show ?thesis by auto |
80 qed |
80 qed |
81 |
81 |
82 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" |
82 lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" |
83 by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) |
83 using eq_cp_s_th highest max_cp_eq the_preced_def by presburger |
84 |
84 |
85 lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)" |
85 |
|
86 lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)" |
86 by (fold eq_cp_s_th, unfold highest_cp_preced, simp) |
87 by (fold eq_cp_s_th, unfold highest_cp_preced, simp) |
87 |
88 |
88 lemma highest': "cp s th = Max (cp s ` threads s)" |
89 lemma highest': "cp s th = Max (cp s ` threads s)" |
89 proof - |
90 by (simp add: eq_cp_s_th highest) |
90 from highest_cp_preced max_cp_eq[symmetric] |
|
91 show ?thesis by simp |
|
92 qed |
|
93 |
91 |
94 end |
92 end |
95 |
93 |
96 locale extend_highest_gen = highest_gen + |
94 locale extend_highest_gen = highest_gen + |
97 fixes t |
95 fixes t |
246 The proof goes by induction over @{text "t"} using the specialized |
243 The proof goes by induction over @{text "t"} using the specialized |
247 induction rule @{thm ind}, followed by case analysis of each possible |
244 induction rule @{thm ind}, followed by case analysis of each possible |
248 operations of PIP. All cases follow the same pattern rendered by the |
245 operations of PIP. All cases follow the same pattern rendered by the |
249 generalized introduction rule @{thm "image_Max_eqI"}. |
246 generalized introduction rule @{thm "image_Max_eqI"}. |
250 |
247 |
251 The very essence is to show that precedences, no matter whether they are newly introduced |
248 The very essence is to show that precedences, no matter whether they |
252 or modified, are always lower than the one held by @{term "th"}, |
249 are newly introduced or modified, are always lower than the one held |
253 which by @{thm th_kept} is preserved along the way. |
250 by @{term "th"}, which by @{thm th_kept} is preserved along the way. |
254 *} |
251 *} |
255 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" |
252 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" |
256 proof(induct rule:ind) |
253 proof(induct rule:ind) |
257 case Nil |
254 case Nil |
258 from highest_preced_thread |
255 from highest_preced_thread |
259 show ?case |
256 show ?case by simp |
260 by (unfold the_preced_def, simp) |
|
261 next |
257 next |
262 case (Cons e t) |
258 case (Cons e t) |
263 interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto |
259 interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto |
264 interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto |
260 interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto |
265 show ?case |
261 show ?case |
283 thus "?f x \<le> ?f th" |
279 thus "?f x \<le> ?f th" |
284 proof |
280 proof |
285 assume "x = thread" |
281 assume "x = thread" |
286 thus ?thesis |
282 thus ?thesis |
287 apply (simp add:Create the_preced_def preced_def, fold preced_def) |
283 apply (simp add:Create the_preced_def preced_def, fold preced_def) |
288 using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force |
284 using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 |
|
285 preced_th by force |
289 next |
286 next |
290 assume h: "x \<in> threads (t @ s)" |
287 assume h: "x \<in> threads (t @ s)" |
291 from Cons(2)[unfolded Create] |
288 from Cons(2)[unfolded Create] |
292 have "x \<noteq> thread" using h by (cases, auto) |
289 have "x \<noteq> thread" using h by (cases, auto) |
293 hence "?f x = the_preced (t@s) x" |
290 hence "?f x = the_preced (t@s) x" |
438 qed |
435 qed |
439 also have "... = ?R" by (simp add: max_preced the_preced_def) |
436 also have "... = ?R" by (simp add: max_preced the_preced_def) |
440 finally show ?thesis . |
437 finally show ?thesis . |
441 qed |
438 qed |
442 |
439 |
443 lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" |
440 lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th" |
444 using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger |
441 using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger |
445 |
442 |
446 lemma th_cp_preced: "cp (t@s) th = preced th s" |
443 lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))" |
|
444 by (simp add: th_cp_max_preced) |
|
445 |
|
446 lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th" |
|
447 using max_kept th_kept the_preced_def by auto |
|
448 |
|
449 lemma [simp]: "the_preced (t@s) th = preced th (t@s)" |
|
450 using the_preced_def by auto |
|
451 |
|
452 lemma [simp]: "preced th (t@s) = preced th s" |
|
453 by (simp add: th_kept) |
|
454 |
|
455 lemma [simp]: "cp s th = preced th s" |
|
456 by (simp add: eq_cp_s_th) |
|
457 |
|
458 lemma th_cp_preced [simp]: "cp (t@s) th = preced th s" |
447 by (fold max_kept, unfold th_cp_max_preced, simp) |
459 by (fold max_kept, unfold th_cp_max_preced, simp) |
448 |
460 |
449 lemma preced_less: |
461 lemma preced_less: |
450 assumes th'_in: "th' \<in> threads s" |
462 assumes th'_in: "th' \<in> threads s" |
451 and neq_th': "th' \<noteq> th" |
463 and neq_th': "th' \<noteq> th" |
453 using assms |
465 using assms |
454 by (metis Max.coboundedI finite_imageI highest not_le order.trans |
466 by (metis Max.coboundedI finite_imageI highest not_le order.trans |
455 preced_linorder rev_image_eqI threads_s vat_s.finite_threads |
467 preced_linorder rev_image_eqI threads_s vat_s.finite_threads |
456 vat_s.le_cp) |
468 vat_s.le_cp) |
457 |
469 |
|
470 section {* The `blocking thread` *} |
|
471 |
|
472 text {* |
|
473 The purpose of PIP is to ensure that the most |
|
474 urgent thread @{term th} is not blocked unreasonably. |
|
475 Therefore, a clear picture of the blocking thread is essential |
|
476 to assure people that the purpose is fulfilled. |
|
477 |
|
478 In this section, we are going to derive a series of lemmas |
|
479 with finally give rise to a picture of the blocking thread. |
|
480 |
|
481 By `blocking thread`, we mean a thread in running state but |
|
482 different from thread @{term th}. |
|
483 *} |
|
484 |
458 text {* |
485 text {* |
459 The following lemmas shows that the @{term cp}-value |
486 The following lemmas shows that the @{term cp}-value |
460 of the blocking thread @{text th'} equals to the highest |
487 of the blocking thread @{text th'} equals to the highest |
461 precedence in the whole system. |
488 precedence in the whole system. |
462 *} |
489 *} |
469 also have "\<dots> = ?R" |
496 also have "\<dots> = ?R" |
470 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
497 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
471 finally show ?thesis . |
498 finally show ?thesis . |
472 qed |
499 qed |
473 |
500 |
474 section {* The `blocking thread` *} |
501 text {* |
475 |
502 The following lemma shows how the counting of |
476 text {* |
503 @{term "P"} and @{term "V"} operations affects |
477 Counting of the number of @{term "P"} and @{term "V"} operations |
504 the running state of threads in @{term t}. |
478 is the cornerstone of a large number of the following proofs. |
505 |
479 The reason is that this counting is quite easy to calculate and |
506 The lemma shows that if a thread's @{term "P"}-count equals |
480 convenient to use in the reasoning. |
507 its @{term "V"}-count (which means it no longer has any |
481 |
508 resource in its possession), it can not be in running thread. |
482 The following lemma shows that the counting controls whether |
509 |
483 a thread is running or not. |
510 The proof is by contraction with the assumption @{text "th' \<noteq> th"}. |
484 *} (* ccc *) |
511 The key is the use of @{thm count_eq_dependants} |
|
512 to derive the emptiness of @{text th'}s @{term dependants}-set |
|
513 from the balance of its @{term P} @{term V} counts. |
|
514 From this, it can be shown @{text th'}s @{term cp}-value |
|
515 equals to its own precedence. |
|
516 |
|
517 On the other hand, since @{text th'} is running, by |
|
518 @{thm runing_preced_inversion}, its @{term cp}-value |
|
519 equals to the precedence of @{term th}. |
|
520 |
|
521 Combining the above two we have that @{text th'} and |
|
522 @{term th} have the same precedence. By uniqueness of precedence, we |
|
523 have @{text "th' = th"}, which is in contradiction with the |
|
524 assumption @{text "th' \<noteq> th"}. |
|
525 *} |
485 |
526 |
486 lemma eq_pv_blocked: (* ddd *) |
527 lemma eq_pv_blocked: (* ddd *) |
487 assumes neq_th': "th' \<noteq> th" |
528 assumes neq_th': "th' \<noteq> th" |
488 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
529 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
489 shows "th' \<notin> runing (t@s)" |
530 shows "th' \<notin> runing (t@s)" |
505 -- {* Since the counts of @{term th'} are balanced, the subtree |
546 -- {* Since the counts of @{term th'} are balanced, the subtree |
506 of it contains only itself, so, its @{term cp}-value |
547 of it contains only itself, so, its @{term cp}-value |
507 equals its @{term preced}-value: *} |
548 equals its @{term preced}-value: *} |
508 have "?L = cp (t@s) th'" |
549 have "?L = cp (t@s) th'" |
509 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) |
550 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) |
510 -- {* Since @{term "th'"} is running by @{thm otherwise}, |
551 -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, |
511 it has the highest @{term cp}-value, by definition, |
552 its @{term cp}-value equals @{term "preced th s"}, |
512 which in turn equals to the @{term cp}-value of @{term th}. *} |
553 which equals to @{term "?R"} by simplification: *} |
513 also have "... = ?R" |
554 also have "... = ?R" |
514 using runing_preced_inversion[OF otherwise] th_kept by simp |
555 thm runing_preced_inversion |
|
556 using runing_preced_inversion[OF otherwise] by simp |
515 finally show ?thesis . |
557 finally show ?thesis . |
516 qed |
558 qed |
517 qed (auto simp: th'_in th_kept) |
559 qed (auto simp: th'_in th_kept) |
518 moreover have "th' \<noteq> th" using neq_th' . |
560 with `th' \<noteq> th` show ?thesis by simp |
519 ultimately show ?thesis by simp |
|
520 qed |
561 qed |
521 qed |
562 qed |
522 |
563 |
523 text {* |
564 text {* |
524 The following lemma is the extrapolation of @{thm eq_pv_blocked}. |
565 The following lemma is the extrapolation of @{thm eq_pv_blocked}. |
587 and eq_pv: "cntP s th' = cntV s th'" |
628 and eq_pv: "cntP s th' = cntV s th'" |
588 shows "th' \<notin> runing (t@s)" |
629 shows "th' \<notin> runing (t@s)" |
589 using assms |
630 using assms |
590 by (simp add: eq_pv_blocked eq_pv_persist) |
631 by (simp add: eq_pv_blocked eq_pv_persist) |
591 |
632 |
592 text {* |
|
593 The purpose of PIP is to ensure that the most |
|
594 urgent thread @{term th} is not blocked unreasonably. |
|
595 Therefore, a clear picture of the blocking thread is essential |
|
596 to assure people that the purpose is fulfilled. |
|
597 |
|
598 The following lemmas will give us such a picture: |
|
599 *} |
|
600 |
|
601 text {* |
633 text {* |
602 The following lemma shows the blocking thread @{term th'} |
634 The following lemma shows the blocking thread @{term th'} |
603 must hold some resource in the very beginning. |
635 must hold some resource in the very beginning. |
604 *} |
636 *} |
605 lemma runing_cntP_cntV_inv: (* ddd *) |
637 lemma runing_cntP_cntV_inv: (* ddd *) |