725 one in it which holds the highest @{term cp}-value, which, by definition, |
725 one in it which holds the highest @{term cp}-value, which, by definition, |
726 is the @{term running}-thread. However, we are going to show more: this running thread |
726 is the @{term running}-thread. However, we are going to show more: this running thread |
727 is exactly @{term "th'"}. |
727 is exactly @{term "th'"}. |
728 *} |
728 *} |
729 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
729 lemma th_blockedE: (* ddd, the other main lemma to be presented: *) |
730 assumes "th \<notin> running (t@s)" |
730 assumes "th \<notin> running (t @ s)" |
731 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
731 obtains th' where "th' \<in> ancestors (tG (t @ s)) th" |
732 "th' \<in> running (t@s)" |
732 "th' \<in> running (t @ s)" |
733 proof - |
733 proof - |
734 -- {* According to @{thm vat_t.th_chain_to_ready}, either |
734 -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either |
735 @{term "th"} is in @{term "readys"} or there is path leading from it to |
735 @{term "th"} is in @{term "readys"} or there is path leading from it to |
736 one thread in @{term "readys"}. *} |
736 one thread in @{term "readys"}. *} |
737 have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" |
737 have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (th, th') \<in> (tG (t @ s))\<^sup>+)" |
738 using th_kept vat_t.th_chain_to_ready by auto |
738 using th_kept vat_t.th_chain_to_ready_tG by blast |
|
739 |
739 -- {* However, @{term th} can not be in @{term readys}, because otherwise, since |
740 -- {* However, @{term th} can not be in @{term readys}, because otherwise, since |
740 @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *} |
741 @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *} |
741 moreover have "th \<notin> readys (t@s)" |
742 moreover have "th \<notin> readys (t @ s)" |
742 using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto |
743 using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto |
|
744 |
743 -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in |
745 -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in |
744 term @{term readys}: *} |
746 term @{term readys}: *} |
745 ultimately obtain th' where th'_in: "th' \<in> readys (t@s)" |
747 ultimately obtain th' where th'_in: "th' \<in> readys (t @ s)" |
746 and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto |
748 and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto |
|
749 |
747 -- {* We are going to show that this @{term th'} is running. *} |
750 -- {* We are going to show that this @{term th'} is running. *} |
748 have "th' \<in> running (t@s)" |
751 have "th' \<in> running (t @ s)" |
749 proof - |
752 proof - |
750 -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} |
753 -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} |
751 have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") |
754 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R") |
752 proof - |
755 proof - |
753 -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), |
756 -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}), |
754 the @{term cp}-value of @{term th'} is the maximum of |
757 the @{term cp}-value of @{term th'} is the maximum of |
755 all precedences of all thread nodes in its @{term tRAG}-subtree: *} |
758 all precedences of all thread nodes in its @{term tRAG}-subtree: *} |
756 have "?L = Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))" |
759 have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))" |
757 by (unfold cp_alt_def1, simp) |
760 by (unfold cp_alt_def2, simp) |
758 also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)" |
761 also have "... = (the_preced (t @ s) th)" |
759 proof(rule image_Max_subset) |
762 proof(rule image_Max_subset) |
760 show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) |
763 show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) |
761 next |
764 next |
762 show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)" |
765 show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)" |
763 by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread) |
766 using readys_def th'_in vat_t.subtree_tG_thread by auto |
764 next |
767 next |
765 show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp |
768 show "th \<in> subtree (tG (t @ s)) th'" |
766 by (unfold tRAG_subtree_eq, auto simp:subtree_def) |
769 by (simp add: dp subtree_def trancl_into_rtrancl) |
767 next |
770 next |
768 show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) = |
771 show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th" |
769 (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _") |
772 by simp |
770 proof - |
773 qed |
771 have "?L = the_preced (t @ s) ` threads (t @ s)" |
|
772 by (unfold image_comp, rule image_cong, auto) |
|
773 thus ?thesis using max_preced the_preced_def by auto |
|
774 qed |
|
775 qed |
|
776 thm the_preced_def |
|
777 also have "... = ?R" |
774 also have "... = ?R" |
778 using th_cp_max th_cp_preced th_kept |
775 using th_cp_max th_cp_preced th_kept |
779 the_preced_def vat_t.max_cp_readys_threads by auto |
776 the_preced_def vat_t.max_cp_readys_threads by auto |
780 thm th_cp_max th_cp_preced th_kept |
777 finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" . |
781 the_preced_def vat_t.max_cp_readys_threads |
|
782 finally show ?thesis . |
|
783 qed |
778 qed |
784 -- {* Now, since @{term th'} holds the highest @{term cp} |
779 |
785 and we have already show it is in @{term readys}, |
780 -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, |
786 it is @{term running} by definition. *} |
781 it is @{term running} by definition. *} |
787 with `th' \<in> readys (t@s)` show ?thesis by (simp add: running_def) |
782 with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def) |
788 qed |
783 qed |
|
784 |
789 -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} |
785 -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} |
790 moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
786 moreover have "th' \<in> ancestors (tG (t @ s)) th" |
791 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
787 by (simp add: ancestors_def dp) |
792 ultimately show ?thesis using that by metis |
788 ultimately show ?thesis using that by metis |
793 qed |
789 qed |
794 |
790 |
795 lemma (* new proof of th_blockedE *) |
791 lemma (* new proof of th_blockedE *) |
796 assumes "th \<notin> running (t @ s)" |
792 assumes "th \<notin> running (t @ s)" |
861 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
857 using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) |
862 ultimately show ?thesis using that by metis |
858 ultimately show ?thesis using that by metis |
863 qed |
859 qed |
864 |
860 |
865 lemma th_blockedE_pretty: |
861 lemma th_blockedE_pretty: |
866 assumes "th \<notin> running (t@s)" |
862 assumes "th \<notin> running (t @ s)" |
867 shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> running (t@s)" |
863 shows "\<exists>th'. th' \<in> ancestors (tG (t @ s)) th \<and> th' \<in> running (t @ s)" |
868 using th_blockedE assms by blast |
864 using th_blockedE assms |
|
865 by blast |
|
866 |
|
867 |
|
868 |
869 |
869 |
870 text {* |
870 text {* |
871 Now it is easy to see there is always a thread to run by case analysis |
871 Now it is easy to see there is always a thread to run by case analysis |
872 on whether thread @{term th} is running: if the answer is Yes, the |
872 on whether thread @{term th} is running: if the answer is yes, the |
873 the running thread is obviously @{term th} itself; otherwise, the running |
873 the running thread is obviously @{term th} itself; otherwise, the running |
874 thread is the @{text th'} given by lemma @{thm th_blockedE}. |
874 thread is the @{text th'} given by lemma @{thm th_blockedE}. |
875 *} |
875 *} |
876 lemma live: "running (t@s) \<noteq> {}" |
876 lemma live: "running (t @ s) \<noteq> {}" |
877 proof(cases "th \<in> running (t@s)") |
877 proof(cases "th \<in> running (t @ s)") |
878 case True thus ?thesis by auto |
878 case True thus ?thesis by auto |
879 next |
879 next |
880 case False |
880 case False |
881 thus ?thesis using th_blockedE by auto |
881 thus ?thesis using th_blockedE by auto |
882 qed |
882 qed |
883 |
883 |
884 lemma blockedE: |
884 lemma blockedE: |
885 assumes "th \<notin> running (t@s)" |
885 assumes "th \<notin> running (t @ s)" |
886 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" |
886 obtains th' where "th' \<in> ancestors (tG (t @ s)) th" |
887 "th' \<in> running (t@s)" |
887 "th' \<in> running (t @ s)" |
888 "th' \<in> threads s" |
888 "th' \<in> threads s" |
889 "\<not>detached s th'" |
889 "\<not>detached s th'" |
890 "cp (t@s) th' = preced th s" |
890 "cp (t @ s) th' = preced th s" |
891 "th' \<noteq> th" |
891 "th' \<noteq> th" |
892 by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE) |
892 using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE |
|
893 by metis |
893 |
894 |
894 lemma detached_not_running: |
895 lemma detached_not_running: |
895 assumes "detached (t@s) th'" |
896 assumes "detached (t @ s) th'" |
896 and "th' \<noteq> th" |
897 and "th' \<noteq> th" |
897 shows "th' \<notin> running (t@s)" |
898 shows "th' \<notin> running (t @ s)" |
898 proof |
899 proof |
899 assume otherwise: "th' \<in> running (t @ s)" |
900 assume otherwise: "th' \<in> running (t @ s)" |
900 have "cp (t@s) th' = cp (t@s) th" |
901 have "cp (t@s) th' = cp (t@s) th" |
901 proof - |
902 proof - |
902 have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise |
903 have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise |
918 qed |
919 qed |
919 |
920 |
920 section {* The correctness theorem of PIP *} |
921 section {* The correctness theorem of PIP *} |
921 |
922 |
922 text {* |
923 text {* |
923 In this section, we identify two more conditions in addition to the ones already |
924 |
924 specified in the forgoing locales, based on which the correctness of PIP is |
925 In this section, we identify two more conditions in addition to the ones |
925 formally proved. |
926 already specified in the current locale, based on which the correctness |
926 |
927 of PIP is formally proved. |
927 Note that Priority Inversion refers to the phenomenon where the thread with highest priority |
928 |
928 is blocked by one with lower priority because the resource it is requesting is |
929 Note that Priority Inversion refers to the phenomenon where the thread |
929 currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion}, |
930 with highest priority is blocked by one with lower priority because the |
930 i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large. |
931 resource it is requesting is currently held by the later. The objective of |
931 |
932 PIP is to avoid {\em Indefinite Priority Inversion}, i.e. the number of |
932 For PIP to be correct, a finite upper bound needs to be found for the occurrence number, |
933 occurrences of {\em Priority Inversion} becomes indefinitely large. |
933 and the existence. This section makes explicit two more conditions so that the existence |
934 |
934 of such a upper bound can be proved to exist. |
935 For PIP to be correct, a finite upper bound needs to be found for the |
935 *} |
936 occurrence number, and the existence. This section makes explicit two more |
|
937 conditions so that the existence of such a upper bound can be proved to |
|
938 exist. *} |
936 |
939 |
937 text {* |
940 text {* |
938 The following set @{text "blockers"} characterizes the set of threads which |
941 The following set @{text "blockers"} characterizes the set of threads which |
939 might block @{term th} in @{term t}: |
942 might block @{term th} in @{term t}: |
940 *} |
943 *} |