45 readys ("ready") and |
45 readys ("ready") and |
46 preced ("prec") and |
46 preced ("prec") and |
47 preceds ("precs") and |
47 preceds ("precs") and |
48 cpreced ("cprec") and |
48 cpreced ("cprec") and |
49 cpreceds ("cprecs") and |
49 cpreceds ("cprecs") and |
50 wq_fun ("wq") and |
50 (*wq_fun ("wq") and*) |
51 cp ("cprec") and |
51 cp ("cprec") and |
52 (*cprec_fun ("cp_fun") and*) |
52 (*cprec_fun ("cp_fun") and*) |
53 holdents ("resources") and |
53 holdents ("resources") and |
54 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
54 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
55 cntP ("c\<^bsub>P\<^esub>") and |
55 cntP ("c\<^bsub>P\<^esub>") and |
625 |
625 |
626 The use of relations for representing RAGs allows us to conveniently define |
626 The use of relations for representing RAGs allows us to conveniently define |
627 the notion of the \emph{dependants} of a thread |
627 the notion of the \emph{dependants} of a thread |
628 |
628 |
629 \begin{isabelle}\ \ \ \ \ %%% |
629 \begin{isabelle}\ \ \ \ \ %%% |
630 @{thm dependants_raw_def} |
630 @{thm dependants_raw_def}\hfill\numbered{dependants} |
631 \end{isabelle} |
631 \end{isabelle} |
632 |
632 |
633 \noindent This definition needs to account for all threads that wait |
633 \noindent This definition needs to account for all threads that wait |
634 for a thread to release a resource. This means we need to include |
634 for a thread to release a resource. This means we need to include |
635 threads that transitively wait for a resource to be released (in the |
635 threads that transitively wait for a resource to be released (in the |
649 |
649 |
650 \begin{isabelle}\ \ \ \ \ %%% |
650 \begin{isabelle}\ \ \ \ \ %%% |
651 @{thm cpreced_def3}\hfill\numbered{cpreced} |
651 @{thm cpreced_def3}\hfill\numbered{cpreced} |
652 \end{isabelle} |
652 \end{isabelle} |
653 |
653 |
654 %\endnote{ |
654 \noindent where the dependants of @{text th} are given by the |
655 %\begin{isabelle}\ \ \ \ \ %%% |
|
656 %@ {thm cp_alt_def cp_alt_def1} |
|
657 %\end{isabelle} |
|
658 %} |
|
659 |
|
660 \noindent where the dependants of @{text th} are given by the |
|
661 waiting queue function. While the precedence @{term prec} of any |
655 waiting queue function. While the precedence @{term prec} of any |
662 thread is determined statically (for example when the thread is |
656 thread is determined statically (for example when the thread is |
663 created), the point of the current precedence is to dynamically |
657 created), the point of the current precedence is to dynamically |
664 increase this precedence, if needed according to PIP. Therefore the |
658 increase this precedence, if needed according to PIP. Therefore the |
665 current precedence of @{text th} is given as the maximum of the |
659 current precedence of @{text th} is given as the maximum of the |
790 @{term RAG}, @{term dependants} and @{term cp} to operate on states |
784 @{term RAG}, @{term dependants} and @{term cp} to operate on states |
791 only. |
785 only. |
792 |
786 |
793 \begin{isabelle}\ \ \ \ \ %%% |
787 \begin{isabelle}\ \ \ \ \ %%% |
794 \begin{tabular}{@ {}rcl} |
788 \begin{tabular}{@ {}rcl} |
795 @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\ |
789 @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv[simplified wq_def]}\\ |
796 @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\ |
790 @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv[simplified wq_def]}\\ |
797 @{thm (lhs) s_RAG_abv} & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv}\\ |
791 @{thm (lhs) s_RAG_abv} & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv[simplified wq_def]}\\ |
798 @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv}\\ |
792 @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv[simplified wq_def]}\\ |
799 @{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\ |
793 @{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\ |
800 \end{tabular} |
794 \end{tabular} |
801 \end{isabelle} |
795 \end{isabelle} |
802 |
796 |
803 \noindent |
797 \noindent |
804 With these abbreviations in place we can introduce |
798 With these abbreviations in place we can derive for every valid trace @{text s} |
|
799 the following two facts about @{term dependants} and @{term cprec} (see \eqref{dependants} |
|
800 and \eqref{cpreced}): Given @{thm (prem 1) valid_trace.cp_alt_def}, then |
|
801 |
|
802 \begin{isabelle}\ \ \ \ \ %%% |
|
803 \begin{tabular}{@ {}rcl} |
|
804 @{thm (concl) valid_trace.cp_alt_def3}\\ |
|
805 \end{tabular}\hfill\numbered{overloaded} |
|
806 \end{isabelle} |
|
807 |
|
808 |
|
809 can introduce |
805 the notion of a thread being @{term ready} in a state (i.e.~threads |
810 the notion of a thread being @{term ready} in a state (i.e.~threads |
806 that do not wait for any resource, which are the roots of the trees |
811 that do not wait for any resource, which are the roots of the trees |
807 in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread |
812 in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread |
808 is then the thread with the highest current precedence of all ready threads. |
813 is then the thread with the highest current precedence of all ready threads. |
809 |
814 |
1040 has the highest precedence of all alive threads in @{text s}. Furthermore the |
1045 has the highest precedence of all alive threads in @{text s}. Furthermore the |
1041 priority of @{text th} is @{text prio} (we need this in the next assumptions). |
1046 priority of @{text th} is @{text prio} (we need this in the next assumptions). |
1042 \begin{isabelle}\ \ \ \ \ %%% |
1047 \begin{isabelle}\ \ \ \ \ %%% |
1043 \begin{tabular}{l} |
1048 \begin{tabular}{l} |
1044 @{term "th \<in> threads s"}\\ |
1049 @{term "th \<in> threads s"}\\ |
1045 @{term "prec th s = Max (cprecs s (threads s))"}\\ |
1050 @{term "prec th s = Max (precs s (threads s))"}\\ |
1046 @{term "prec th s = (prio, DUMMY)"} |
1051 @{term "prec th s = (prio, DUMMY)"} |
1047 \end{tabular} |
1052 \end{tabular} |
1048 \end{isabelle} |
1053 \end{isabelle} |
1049 \end{quote} |
1054 \end{quote} |
1050 |
1055 |
1830 \noindent |
1835 \noindent |
1831 where a child is a thread that is only one ``hop'' away from the thread |
1836 where a child is a thread that is only one ``hop'' away from the thread |
1832 @{text th} in the @{term RAG} (and waiting for @{text th} to release |
1837 @{text th} in the @{term RAG} (and waiting for @{text th} to release |
1833 a resource). We can prove the following lemma. |
1838 a resource). We can prove the following lemma. |
1834 |
1839 |
|
1840 \begin{center} |
|
1841 @{thm tG_alt_def}\\ |
|
1842 @{thm dependants_alt_tG} |
|
1843 \end{center} |
|
1844 |
|
1845 \begin{center} |
|
1846 @{thm valid_trace.cp_alt_def3} |
|
1847 \end{center} |
|
1848 |
|
1849 |
1835 \begin{lemma}\label{childrenlem} |
1850 \begin{lemma}\label{childrenlem} |
1836 HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"} |
1851 HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"} |
1837 \begin{center} |
1852 \begin{center} |
1838 @{thm valid_trace.cp_rec}. |
1853 @{thm valid_trace.cp_rec_tG}. |
1839 %@ {thm (concl) cp_rec}. |
1854 %@ {thm (concl) cp_rec}. |
1840 \end{center} |
1855 \end{center} |
1841 \end{lemma} |
1856 \end{lemma} |
1842 |
1857 |
1843 \noindent |
1858 \noindent |