723 show "cp (t@s) th' = preced th s" . |
723 show "cp (t@s) th' = preced th s" . |
724 qed |
724 qed |
725 |
725 |
726 section {* The existence of `blocking thread` *} |
726 section {* The existence of `blocking thread` *} |
727 |
727 |
728 text {* |
728 lemma th_ancestor_has_max_ready: |
729 Suppose @{term th} is not running, it is first shown that |
729 assumes th'_in: "th' \<in> readys (t@s)" |
730 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
730 and dp: "th' \<in> nancestors (tG (t @ s)) th" |
731 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
731 shows "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R") |
732 |
|
733 Now, since @{term readys}-set is non-empty, there must be |
|
734 one in it which holds the highest @{term cp}-value, which, by definition, |
|
735 is the @{term running}-thread. However, we are going to show more: this |
|
736 running thread is exactly @{term "th'"}. *} |
|
737 |
|
738 |
|
739 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
|
740 obtains th' where "th' \<in> nancestors (tG (t @ s)) th" |
|
741 "th' \<in> running (t @ s)" |
|
742 proof - |
732 proof - |
743 -- {* According to @{thm vat_t.th_chain_to_ready}, there is a |
|
744 ready ancestor of @{term th}. *} |
|
745 have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" |
|
746 using th_kept vat_t.th_chain_to_ready_tG by auto |
|
747 then obtain th' where th'_in: "th' \<in> readys (t@s)" |
|
748 and dp: "th' \<in> nancestors (tG (t @ s)) th" |
|
749 by blast |
|
750 |
|
751 -- {* We are going to first show that this @{term th'} is running. *} |
|
752 have "th' \<in> running (t @ s)" |
|
753 proof - |
|
754 -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *} |
|
755 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R") |
|
756 proof - |
|
757 -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), |
733 -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), |
758 the @{term cp}-value of @{term th'} is the maximum of |
734 the @{term cp}-value of @{term th'} is the maximum of |
759 all precedences of all thread nodes in its @{term tRAG}-subtree: *} |
735 all precedences of all thread nodes in its @{term tRAG}-subtree: *} |
760 have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))" |
736 have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))" |
761 by (unfold cp_alt_def2, simp) |
737 by (unfold cp_alt_def2, simp) |
774 qed |
750 qed |
775 also have "... = ?R" |
751 also have "... = ?R" |
776 using th_cp_max th_cp_preced th_kept |
752 using th_cp_max th_cp_preced th_kept |
777 the_preced_def vat_t.max_cp_readys_threads by auto |
753 the_preced_def vat_t.max_cp_readys_threads by auto |
778 finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . |
754 finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . |
779 qed |
755 qed |
780 |
756 |
781 -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, |
757 |
782 it is @{term running} by definition. *} |
758 text {* |
783 with `th' \<in> readys (t @ s)` |
759 Suppose @{term th} is not running, it is first shown that |
784 show "th' \<in> running (t @ s)" by (simp add: running_def) |
760 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
785 qed |
761 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
786 |
762 |
|
763 Now, since @{term readys}-set is non-empty, there must be |
|
764 one in it which holds the highest @{term cp}-value, which, by definition, |
|
765 is the @{term running}-thread. However, we are going to show more: this |
|
766 running thread is exactly @{term "th'"}. *} |
|
767 |
|
768 |
|
769 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
|
770 obtains th' where "th' \<in> nancestors (tG (t @ s)) th" |
|
771 "th' \<in> running (t @ s)" |
|
772 proof - |
|
773 -- {* According to @{thm vat_t.th_chain_to_ready}, there is a |
|
774 ready ancestor of @{term th}. *} |
|
775 have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" |
|
776 using th_kept vat_t.th_chain_to_ready_tG by auto |
|
777 then obtain th' where th'_in: "th' \<in> readys (t @ s)" |
|
778 and dp: "th' \<in> nancestors (tG (t @ s)) th" |
|
779 by blast |
|
780 |
|
781 -- {* We are going to first show that this @{term th'} is running. *} |
|
782 |
|
783 from th'_in dp |
|
784 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" |
|
785 by (rule th_ancestor_has_max_ready) |
|
786 with `th' \<in> readys (t @ s)` |
|
787 have "th' \<in> running (t @ s)" by (simp add: running_def) |
|
788 |
787 -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} |
789 -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} |
788 moreover have "th' \<in> nancestors (tG (t @ s)) th" |
790 moreover have "th' \<in> nancestors (tG (t @ s)) th" |
789 using dp unfolding nancestors_def2 by simp |
791 using dp unfolding nancestors_def2 by simp |
790 ultimately show ?thesis using that by metis |
792 ultimately show ?thesis using that by metis |
791 qed |
793 qed |
929 thus ?thesis by (unfold detached_test, auto) |
931 thus ?thesis by (unfold detached_test, auto) |
930 qed |
932 qed |
931 thus ?thesis unfolding blockers_def by simp |
933 thus ?thesis unfolding blockers_def by simp |
932 qed |
934 qed |
933 |
935 |
934 text {* |
936 text {* The following lemma shows that a blocker does not die as long as the |
935 The following lemma shows that a blocker may never die |
937 highest thread @{term th} is live. |
936 as long as the highest thread @{term th} is living. |
938 |
937 |
939 The reason for this is that, before a thread can execute an @{term Exit} |
938 The reason for this is that, before a thread can execute an @{term Exit} operation, |
940 operation, it must give up all its resource. However, the high priority |
939 it must give up all its resource. However, the high priority inherited by a blocker |
941 inherited by a blocker thread also goes with the resources it once held, |
940 thread also goes with the resources it once held, and the consequence is the lost of |
942 and the consequence is the lost of right to run, the other precondition |
941 right to run, the other precondition for it to execute its own @{term Exit} operation. |
943 for it to execute its own @{term Exit} operation. For this reason, a |
942 For this reason, a blocker may never exit before the exit of the highest thread @{term th}. |
944 blocker may never exit before the exit of the highest thread @{term th}. |
943 *} |
945 *} |
944 |
946 |
945 lemma blockers_kept: |
947 lemma blockers_kept: |
946 assumes "th' \<in> blockers" |
948 assumes "th' \<in> blockers" |
947 shows "th' \<in> threads (t@s)" |
949 shows "th' \<in> threads (t@s)" |