658 \end{tabular} |
658 \end{tabular} |
659 \end{isabelle} |
659 \end{isabelle} |
660 \end{quote} |
660 \end{quote} |
661 |
661 |
662 \noindent |
662 \noindent |
663 Under these assumption we will prove the following property: |
663 Under these assumptions we will prove the following property: |
664 |
664 |
665 \begin{theorem} |
665 \begin{theorem}\label{mainthm} |
666 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
666 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
667 the thread @{text th} and the events in @{text "s'"}. |
667 the thread @{text th} and the events in @{text "s'"}, |
668 @{thm[mode=IfThen] runing_inversion_3[where ?th'="th'", THEN |
668 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then |
669 conjunct1]} |
669 @{text "th' \<in> threads s"}. |
670 \end{theorem} |
670 \end{theorem} |
671 |
671 |
672 \begin{theorem} |
672 \noindent |
673 @{thm[mode=IfThen] runing_inversion_2} |
673 This theorem ensures that the thread @{text th}, which has the highest |
674 \end{theorem} |
674 precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} |
675 |
675 by a thread @{text th'} that already existed in @{text s}. As we shall see shortly, |
676 |
676 that means by only finitely many threads. Consequently, indefinite wait of |
677 |
677 @{text th}, that is Priority Inversion, cannot occur. |
678 |
678 |
679 |
679 The following are several very basic prioprites: |
680 TO DO |
680 \begin{enumerate} |
681 |
681 \item All runing threads must be ready (@{text "runing_ready"}): |
|
682 @{thm[display] "runing_ready"} |
|
683 \item All ready threads must be living (@{text "readys_threads"}): |
|
684 @{thm[display] "readys_threads"} |
|
685 \item There are finite many living threads at any moment (@{text "finite_threads"}): |
|
686 @{thm[display] "finite_threads"} |
|
687 \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): |
|
688 @{thm[display] "wq_distinct"} |
|
689 \item All threads in waiting queues are living threads (@{text "wq_threads"}): |
|
690 @{thm[display] "wq_threads"} |
|
691 \item The event which can get a thread into waiting queue must be @{term "P"}-events |
|
692 (@{text "block_pre"}): |
|
693 @{thm[display] "block_pre"} |
|
694 \item A thread may never wait for two different critical resources |
|
695 (@{text "waiting_unique"}): |
|
696 @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]} |
|
697 \item Every resource can only be held by one thread |
|
698 (@{text "held_unique"}): |
|
699 @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]} |
|
700 \item Every living thread has an unique precedence |
|
701 (@{text "preced_unique"}): |
|
702 @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]} |
|
703 \end{enumerate} |
|
704 *} |
|
705 |
|
706 text {* \noindent |
|
707 The following lemmas show how RAG is changed with the execution of events: |
|
708 \begin{enumerate} |
|
709 \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}): |
|
710 @{thm[display] depend_set_unchanged} |
|
711 \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}): |
|
712 @{thm[display] depend_create_unchanged} |
|
713 \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}): |
|
714 @{thm[display] depend_exit_unchanged} |
|
715 \item Execution of @{term "P"} (@{text "step_depend_p"}): |
|
716 @{thm[display] step_depend_p} |
|
717 \item Execution of @{term "V"} (@{text "step_depend_v"}): |
|
718 @{thm[display] step_depend_v} |
|
719 \end{enumerate} |
|
720 *} |
|
721 |
|
722 text {* \noindent |
|
723 These properties are used to derive the following important results about RAG: |
|
724 \begin{enumerate} |
|
725 \item RAG is loop free (@{text "acyclic_depend"}): |
|
726 @{thm [display] acyclic_depend} |
|
727 \item RAGs are finite (@{text "finite_depend"}): |
|
728 @{thm [display] finite_depend} |
|
729 \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}): |
|
730 @{thm [display] wf_dep_converse} |
|
731 \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}): |
|
732 @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]} |
|
733 \item All threads in RAG are living threads |
|
734 (@{text "dm_depend_threads"} and @{text "range_in"}): |
|
735 @{thm [display] dm_depend_threads range_in} |
|
736 \end{enumerate} |
|
737 *} |
|
738 |
|
739 text {* \noindent |
|
740 The following lemmas show how every node in RAG can be chased to ready threads: |
|
741 \begin{enumerate} |
|
742 \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
|
743 @{thm [display] chain_building[rule_format]} |
|
744 \item The ready thread chased to is unique (@{text "dchain_unique"}): |
|
745 @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]} |
|
746 \end{enumerate} |
|
747 *} |
|
748 |
|
749 text {* \noindent |
|
750 Properties about @{term "next_th"}: |
|
751 \begin{enumerate} |
|
752 \item The thread taking over is different from the thread which is releasing |
|
753 (@{text "next_th_neq"}): |
|
754 @{thm [display] next_th_neq} |
|
755 \item The thread taking over is unique |
|
756 (@{text "next_th_unique"}): |
|
757 @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]} |
|
758 \end{enumerate} |
|
759 *} |
|
760 |
|
761 text {* \noindent |
|
762 Some deeper results about the system: |
|
763 \begin{enumerate} |
|
764 \item There can only be one running thread (@{text "runing_unique"}): |
|
765 @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]} |
|
766 \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}): |
|
767 @{thm [display] max_cp_eq} |
|
768 \item There must be one ready thread having the max @{term "cp"}-value |
|
769 (@{text "max_cp_readys_threads"}): |
|
770 @{thm [display] max_cp_readys_threads} |
|
771 \end{enumerate} |
|
772 *} |
|
773 |
|
774 text {* \noindent |
|
775 The relationship between the count of @{text "P"} and @{text "V"} and the number of |
|
776 critical resources held by a thread is given as follows: |
|
777 \begin{enumerate} |
|
778 \item The @{term "V"}-operation decreases the number of critical resources |
|
779 one thread holds (@{text "cntCS_v_dec"}) |
|
780 @{thm [display] cntCS_v_dec} |
|
781 \item The number of @{text "V"} never exceeds the number of @{text "P"} |
|
782 (@{text "cnp_cnv_cncs"}): |
|
783 @{thm [display] cnp_cnv_cncs} |
|
784 \item The number of @{text "V"} equals the number of @{text "P"} when |
|
785 the relevant thread is not living: |
|
786 (@{text "cnp_cnv_eq"}): |
|
787 @{thm [display] cnp_cnv_eq} |
|
788 \item When a thread is not living, it does not hold any critical resource |
|
789 (@{text "not_thread_holdents"}): |
|
790 @{thm [display] not_thread_holdents} |
|
791 \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant |
|
792 thread does not hold any critical resource, therefore no thread can depend on it |
|
793 (@{text "count_eq_dependents"}): |
|
794 @{thm [display] count_eq_dependents} |
|
795 \end{enumerate} |
682 *} |
796 *} |
683 |
797 |
684 (*<*) |
798 (*<*) |
685 end |
799 end |
686 (*>*) |
800 (*>*) |
834 *} |
948 *} |
835 |
949 |
836 section {* General properties of Priority Inheritance \label{general} *} |
950 section {* General properties of Priority Inheritance \label{general} *} |
837 |
951 |
838 text {* |
952 text {* |
839 The following are several very basic prioprites: |
953 |
840 \begin{enumerate} |
|
841 \item All runing threads must be ready (@{text "runing_ready"}): |
|
842 @{thm[display] "runing_ready"} |
|
843 \item All ready threads must be living (@{text "readys_threads"}): |
|
844 @{thm[display] "readys_threads"} |
|
845 \item There are finite many living threads at any moment (@{text "finite_threads"}): |
|
846 @{thm[display] "finite_threads"} |
|
847 \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): |
|
848 @{thm[display] "wq_distinct"} |
|
849 \item All threads in waiting queues are living threads (@{text "wq_threads"}): |
|
850 @{thm[display] "wq_threads"} |
|
851 \item The event which can get a thread into waiting queue must be @{term "P"}-events |
|
852 (@{text "block_pre"}): |
|
853 @{thm[display] "block_pre"} |
|
854 \item A thread may never wait for two different critical resources |
|
855 (@{text "waiting_unique"}): |
|
856 @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]} |
|
857 \item Every resource can only be held by one thread |
|
858 (@{text "held_unique"}): |
|
859 @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]} |
|
860 \item Every living thread has an unique precedence |
|
861 (@{text "preced_unique"}): |
|
862 @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]} |
|
863 \end{enumerate} |
|
864 *} |
|
865 |
|
866 text {* \noindent |
|
867 The following lemmas show how RAG is changed with the execution of events: |
|
868 \begin{enumerate} |
|
869 \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}): |
|
870 @{thm[display] depend_set_unchanged} |
|
871 \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}): |
|
872 @{thm[display] depend_create_unchanged} |
|
873 \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}): |
|
874 @{thm[display] depend_exit_unchanged} |
|
875 \item Execution of @{term "P"} (@{text "step_depend_p"}): |
|
876 @{thm[display] step_depend_p} |
|
877 \item Execution of @{term "V"} (@{text "step_depend_v"}): |
|
878 @{thm[display] step_depend_v} |
|
879 \end{enumerate} |
|
880 *} |
|
881 |
|
882 text {* \noindent |
|
883 These properties are used to derive the following important results about RAG: |
|
884 \begin{enumerate} |
|
885 \item RAG is loop free (@{text "acyclic_depend"}): |
|
886 @{thm [display] acyclic_depend} |
|
887 \item RAGs are finite (@{text "finite_depend"}): |
|
888 @{thm [display] finite_depend} |
|
889 \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}): |
|
890 @{thm [display] wf_dep_converse} |
|
891 \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}): |
|
892 @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]} |
|
893 \item All threads in RAG are living threads |
|
894 (@{text "dm_depend_threads"} and @{text "range_in"}): |
|
895 @{thm [display] dm_depend_threads range_in} |
|
896 \end{enumerate} |
|
897 *} |
|
898 |
|
899 text {* \noindent |
|
900 The following lemmas show how every node in RAG can be chased to ready threads: |
|
901 \begin{enumerate} |
|
902 \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
|
903 @{thm [display] chain_building[rule_format]} |
|
904 \item The ready thread chased to is unique (@{text "dchain_unique"}): |
|
905 @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]} |
|
906 \end{enumerate} |
|
907 *} |
|
908 |
|
909 text {* \noindent |
|
910 Properties about @{term "next_th"}: |
|
911 \begin{enumerate} |
|
912 \item The thread taking over is different from the thread which is releasing |
|
913 (@{text "next_th_neq"}): |
|
914 @{thm [display] next_th_neq} |
|
915 \item The thread taking over is unique |
|
916 (@{text "next_th_unique"}): |
|
917 @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]} |
|
918 \end{enumerate} |
|
919 *} |
|
920 |
|
921 text {* \noindent |
|
922 Some deeper results about the system: |
|
923 \begin{enumerate} |
|
924 \item There can only be one running thread (@{text "runing_unique"}): |
|
925 @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]} |
|
926 \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}): |
|
927 @{thm [display] max_cp_eq} |
|
928 \item There must be one ready thread having the max @{term "cp"}-value |
|
929 (@{text "max_cp_readys_threads"}): |
|
930 @{thm [display] max_cp_readys_threads} |
|
931 \end{enumerate} |
|
932 *} |
|
933 |
|
934 text {* \noindent |
|
935 The relationship between the count of @{text "P"} and @{text "V"} and the number of |
|
936 critical resources held by a thread is given as follows: |
|
937 \begin{enumerate} |
|
938 \item The @{term "V"}-operation decreases the number of critical resources |
|
939 one thread holds (@{text "cntCS_v_dec"}) |
|
940 @{thm [display] cntCS_v_dec} |
|
941 \item The number of @{text "V"} never exceeds the number of @{text "P"} |
|
942 (@{text "cnp_cnv_cncs"}): |
|
943 @{thm [display] cnp_cnv_cncs} |
|
944 \item The number of @{text "V"} equals the number of @{text "P"} when |
|
945 the relevant thread is not living: |
|
946 (@{text "cnp_cnv_eq"}): |
|
947 @{thm [display] cnp_cnv_eq} |
|
948 \item When a thread is not living, it does not hold any critical resource |
|
949 (@{text "not_thread_holdents"}): |
|
950 @{thm [display] not_thread_holdents} |
|
951 \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant |
|
952 thread does not hold any critical resource, therefore no thread can depend on it |
|
953 (@{text "count_eq_dependents"}): |
|
954 @{thm [display] count_eq_dependents} |
|
955 \end{enumerate} |
|
956 *} |
954 *} |
957 |
955 |
958 section {* Key properties \label{extension} *} |
956 section {* Key properties \label{extension} *} |
959 |
957 |
960 (*<*) |
958 (*<*) |