472 vat_s.le_cp) |
472 vat_s.le_cp) |
473 |
473 |
474 section {* The `blocking thread` *} |
474 section {* The `blocking thread` *} |
475 |
475 |
476 text {* |
476 text {* |
477 The purpose of PIP is to ensure that the most |
477 |
478 urgent thread @{term th} is not blocked unreasonably. |
478 The purpose of PIP is to ensure that the most urgent thread @{term |
479 Therefore, a clear picture of the blocking thread is essential |
479 th} is not blocked unreasonably. Therefore, below, we will derive |
480 to assure people that the purpose is fulfilled. |
480 properties of the blocking thread. By blocking thread, we mean a |
481 |
481 thread in running state t @ s, but is different from thread @{term |
482 In this section, we are going to derive a series of lemmas |
482 th}. |
483 with finally give rise to a picture of the blocking thread. |
483 |
484 |
484 The first lemmas shows that the @{term cp}-value of the blocking |
485 By `blocking thread`, we mean a thread in running state but |
485 thread @{text th'} equals to the highest precedence in the whole |
486 different from thread @{term th}. |
486 system. |
487 *} |
487 |
488 |
488 *} |
489 text {* |
489 |
490 The following lemmas shows that the @{term cp}-value |
|
491 of the blocking thread @{text th'} equals to the highest |
|
492 precedence in the whole system. |
|
493 *} |
|
494 lemma runing_preced_inversion: |
490 lemma runing_preced_inversion: |
495 assumes runing': "th' \<in> runing (t@s)" |
491 assumes runing': "th' \<in> runing (t @ s)" |
496 shows "cp (t@s) th' = preced th s" (is "?L = ?R") |
492 shows "cp (t @ s) th' = preced th s" |
497 proof - |
493 proof - |
498 have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms |
494 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" |
499 by (unfold runing_def, auto) |
495 using assms by (unfold runing_def, auto) |
500 also have "\<dots> = ?R" |
496 also have "\<dots> = preced th s" |
501 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) |
502 finally show ?thesis . |
498 finally show ?thesis . |
503 qed |
499 qed |
504 |
500 |
505 text {* |
501 text {* |
506 |
502 |
507 The following lemma shows how the counters for @{term "P"} and |
503 The next lemma shows how the counters for @{term "P"} and @{term |
508 @{term "V"} operations relate to the running threads in the states |
504 "V"} operations relate to the running threads in the states @{term |
509 @{term s} and @{term "t @ s"}. The lemma shows that if a thread's |
505 s} and @{term "t @ s"}: if a thread's @{term "P"}-count equals its |
510 @{term "P"}-count equals its @{term "V"}-count (which means it no |
506 @{term "V"}-count (which means it no longer has any resource in its |
511 longer has any resource in its possession), it cannot be a running |
507 possession), it cannot be a running thread. |
512 thread. |
|
513 |
508 |
514 The proof is by contraction with the assumption @{text "th' \<noteq> th"}. |
509 The proof is by contraction with the assumption @{text "th' \<noteq> th"}. |
515 The key is the use of @{thm count_eq_dependants} to derive the |
510 The key is the use of @{thm count_eq_dependants} to derive the |
516 emptiness of @{text th'}s @{term dependants}-set from the balance of |
511 emptiness of @{text th'}s @{term dependants}-set from the balance of |
517 its @{term P} and @{term V} counts. From this, it can be shown |
512 its @{term P} and @{term V} counts. From this, it can be shown |
519 |
514 |
520 On the other hand, since @{text th'} is running, by @{thm |
515 On the other hand, since @{text th'} is running, by @{thm |
521 runing_preced_inversion}, its @{term cp}-value equals to the |
516 runing_preced_inversion}, its @{term cp}-value equals to the |
522 precedence of @{term th}. |
517 precedence of @{term th}. |
523 |
518 |
524 Combining the above two resukts we have that @{text th'} and @{term |
519 Combining the above two results we have that @{text th'} and @{term |
525 th} have the same precedence. By uniqueness of precedences, we have |
520 th} have the same precedence. By uniqueness of precedences, we have |
526 @{text "th' = th"}, which is in contradiction with the assumption |
521 @{text "th' = th"}, which is in contradiction with the assumption |
527 @{text "th' \<noteq> th"}. |
522 @{text "th' \<noteq> th"}. |
528 |
523 |
529 *} |
524 *} |
530 |
525 |
531 lemma eq_pv_blocked: (* ddd *) |
526 lemma eq_pv_blocked: (* ddd *) |
532 assumes neq_th': "th' \<noteq> th" |
527 assumes neq_th': "th' \<noteq> th" |
533 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
528 and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'" |
534 shows "th' \<notin> runing (t@s)" |
529 shows "th' \<notin> runing (t @ s)" |
535 proof |
530 proof |
536 assume otherwise: "th' \<in> runing (t@s)" |
531 assume otherwise: "th' \<in> runing (t @ s)" |
537 show False |
532 show False |
538 proof - |
533 proof - |
539 have th'_in: "th' \<in> threads (t@s)" |
534 have th'_in: "th' \<in> threads (t @ s)" |
540 using otherwise readys_threads runing_def by auto |
535 using otherwise readys_threads runing_def by auto |
541 have "th' = th" |
536 have "th' = th" |
542 proof(rule preced_unique) |
537 proof(rule preced_unique) |
543 -- {* The proof goes like this: |
538 -- {* The proof goes like this: |
544 it is first shown that the @{term preced}-value of @{term th'} |
539 it is first shown that the @{term preced}-value of @{term th'} |
548 show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") |
543 show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") |
549 proof - |
544 proof - |
550 -- {* Since the counts of @{term th'} are balanced, the subtree |
545 -- {* Since the counts of @{term th'} are balanced, the subtree |
551 of it contains only itself, so, its @{term cp}-value |
546 of it contains only itself, so, its @{term cp}-value |
552 equals its @{term preced}-value: *} |
547 equals its @{term preced}-value: *} |
553 have "?L = cp (t@s) th'" |
548 have "?L = cp (t @ s) th'" |
554 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) |
549 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) |
555 -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, |
550 -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, |
556 its @{term cp}-value equals @{term "preced th s"}, |
551 its @{term cp}-value equals @{term "preced th s"}, |
557 which equals to @{term "?R"} by simplification: *} |
552 which equals to @{term "?R"} by simplification: *} |
558 also have "... = ?R" |
553 also have "... = ?R" |
559 thm runing_preced_inversion |
|
560 using runing_preced_inversion[OF otherwise] by simp |
554 using runing_preced_inversion[OF otherwise] by simp |
561 finally show ?thesis . |
555 finally show ?thesis . |
562 qed |
556 qed |
563 qed (auto simp: th'_in th_kept) |
557 qed (auto simp: th'_in th_kept) |
564 with `th' \<noteq> th` show ?thesis by simp |
558 with `th' \<noteq> th` show ?thesis by simp |
572 it will keep hand-emptied in the future @{term "t@s"}. |
566 it will keep hand-emptied in the future @{term "t@s"}. |
573 *} |
567 *} |
574 lemma eq_pv_persist: (* ddd *) |
568 lemma eq_pv_persist: (* ddd *) |
575 assumes neq_th': "th' \<noteq> th" |
569 assumes neq_th': "th' \<noteq> th" |
576 and eq_pv: "cntP s th' = cntV s th'" |
570 and eq_pv: "cntP s th' = cntV s th'" |
577 shows "cntP (t@s) th' = cntV (t@s) th'" |
571 shows "cntP (t @ s) th' = cntV (t @ s) th'" |
578 proof(induction rule:ind) -- {* The proof goes by induction. *} |
572 proof(induction rule: ind) |
579 -- {* The nontrivial case is for the @{term Cons}: *} |
573 -- {* The nontrivial case is for the @{term Cons}: *} |
580 case (Cons e t) |
574 case (Cons e t) |
581 -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} |
575 -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} |
582 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
576 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
583 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
577 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
622 ultimately show ?thesis using Cons(5) by metis |
616 ultimately show ?thesis using Cons(5) by metis |
623 qed |
617 qed |
624 qed (auto simp:eq_pv) |
618 qed (auto simp:eq_pv) |
625 |
619 |
626 text {* |
620 text {* |
627 By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, |
621 |
628 it can be derived easily that @{term th'} can not be running in the future: |
622 By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can |
629 *} |
623 be derived easily that @{term th'} can not be running in the future: |
|
624 |
|
625 *} |
|
626 |
630 lemma eq_pv_blocked_persist: |
627 lemma eq_pv_blocked_persist: |
631 assumes neq_th': "th' \<noteq> th" |
628 assumes neq_th': "th' \<noteq> th" |
632 and eq_pv: "cntP s th' = cntV s th'" |
629 and eq_pv: "cntP s th' = cntV s th'" |
633 shows "th' \<notin> runing (t@s)" |
630 shows "th' \<notin> runing (t @ s)" |
634 using assms |
631 using assms |
635 by (simp add: eq_pv_blocked eq_pv_persist) |
632 by (simp add: eq_pv_blocked eq_pv_persist) |
636 |
633 |
637 text {* |
634 text {* |
638 The following lemma shows the blocking thread @{term th'} |
635 |
639 must hold some resource in the very beginning. |
636 The following lemma shows the blocking thread @{term th'} must hold |
640 *} |
637 some resource in the very beginning. |
|
638 |
|
639 *} |
|
640 |
641 lemma runing_cntP_cntV_inv: (* ddd *) |
641 lemma runing_cntP_cntV_inv: (* ddd *) |
642 assumes is_runing: "th' \<in> runing (t@s)" |
642 assumes is_runing: "th' \<in> runing (t @ s)" |
643 and neq_th': "th' \<noteq> th" |
643 and neq_th': "th' \<noteq> th" |
644 shows "cntP s th' > cntV s th'" |
644 shows "cntP s th' > cntV s th'" |
645 using assms |
645 using assms |
646 proof - |
646 proof - |
647 -- {* First, it can be shown that the number of @{term P} and |
647 -- {* First, it can be shown that the number of @{term P} and |
663 ultimately show ?thesis by auto |
663 ultimately show ?thesis by auto |
664 qed |
664 qed |
665 |
665 |
666 |
666 |
667 text {* |
667 text {* |
668 The following lemmas shows the blocking thread @{text th'} must be live |
668 |
669 at the very beginning, i.e. the moment (or state) @{term s}. |
669 The following lemmas shows the blocking thread @{text th'} must be |
670 |
670 live at the very beginning, i.e. the moment (or state) @{term s}. |
671 The proof is a simple combination of the results above: |
671 The proof is a simple combination of the results above: |
672 *} |
672 |
|
673 *} |
|
674 |
673 lemma runing_threads_inv: |
675 lemma runing_threads_inv: |
674 assumes runing': "th' \<in> runing (t@s)" |
676 assumes runing': "th' \<in> runing (t@s)" |
675 and neq_th': "th' \<noteq> th" |
677 and neq_th': "th' \<noteq> th" |
676 shows "th' \<in> threads s" |
678 shows "th' \<in> threads s" |
677 proof(rule ccontr) -- {* Proof by contradiction: *} |
679 proof(rule ccontr) -- {* Proof by contradiction: *} |
685 qed |
687 qed |
686 with runing' show False by simp |
688 with runing' show False by simp |
687 qed |
689 qed |
688 |
690 |
689 text {* |
691 text {* |
690 The following lemma summarizes several foregoing |
692 |
691 lemmas to give an overall picture of the blocking thread @{text "th'"}: |
693 The following lemma summarises the above lemmas to give an overall |
692 *} |
694 characterisationof the blocking thread @{text "th'"}: |
|
695 |
|
696 *} |
|
697 |
693 lemma runing_inversion: (* ddd, one of the main lemmas to present *) |
698 lemma runing_inversion: (* ddd, one of the main lemmas to present *) |
694 assumes runing': "th' \<in> runing (t@s)" |
699 assumes runing': "th' \<in> runing (t@s)" |
695 and neq_th: "th' \<noteq> th" |
700 and neq_th: "th' \<noteq> th" |
696 shows "th' \<in> threads s" |
701 shows "th' \<in> threads s" |
697 and "\<not>detached s th'" |
702 and "\<not>detached s th'" |
705 next |
710 next |
706 from runing_preced_inversion[OF runing'] |
711 from runing_preced_inversion[OF runing'] |
707 show "cp (t@s) th' = preced th s" . |
712 show "cp (t@s) th' = preced th s" . |
708 qed |
713 qed |
709 |
714 |
|
715 |
710 section {* The existence of `blocking thread` *} |
716 section {* The existence of `blocking thread` *} |
711 |
717 |
712 text {* |
718 text {* |
713 Suppose @{term th} is not running, it is first shown that |
719 |
714 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
720 Suppose @{term th} is not running, it is first shown that there is a |
715 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
721 path in RAG leading from node @{term th} to another thread @{text |
716 |
722 "th'"} in the @{term readys}-set (So @{text "th'"} is an ancestor of |
717 Now, since @{term readys}-set is non-empty, there must be |
723 @{term th}}). |
718 one in it which holds the highest @{term cp}-value, which, by definition, |
724 |
719 is the @{term runing}-thread. However, we are going to show more: this running thread |
725 Now, since @{term readys}-set is non-empty, there must be one in it |
720 is exactly @{term "th'"}. |
726 which holds the highest @{term cp}-value, which, by definition, is |
721 *} |
727 the @{term runing}-thread. However, we are going to show more: this |
|
728 running thread is exactly @{term "th'"}. |
|
729 |
|
730 *} |
|
731 |
722 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
732 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
723 assumes "th \<notin> runing (t@s)" |
733 assumes "th \<notin> runing (t@s)" |
724 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
734 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
725 "th' \<in> runing (t@s)" |
735 "th' \<in> runing (t@s)" |
726 proof - |
736 proof - |
778 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
788 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
779 ultimately show ?thesis using that by metis |
789 ultimately show ?thesis using that by metis |
780 qed |
790 qed |
781 |
791 |
782 text {* |
792 text {* |
783 Now it is easy to see there is always a thread to run by case analysis |
793 |
784 on whether thread @{term th} is running: if the answer is Yes, the |
794 Now it is easy to see there is always a thread to run by case |
785 the running thread is obviously @{term th} itself; otherwise, the running |
795 analysis on whether thread @{term th} is running: if the answer is |
786 thread is the @{text th'} given by lemma @{thm th_blockedE}. |
796 yes, the the running thread is obviously @{term th} itself; |
787 *} |
797 otherwise, the running thread is the @{text th'} given by lemma |
|
798 @{thm th_blockedE}. |
|
799 |
|
800 *} |
|
801 |
788 lemma live: "runing (t@s) \<noteq> {}" |
802 lemma live: "runing (t@s) \<noteq> {}" |
789 proof(cases "th \<in> runing (t@s)") |
803 proof(cases "th \<in> runing (t@s)") |
790 case True thus ?thesis by auto |
804 case True thus ?thesis by auto |
791 next |
805 next |
792 case False |
806 case False |