1870 *} |
1870 *} |
1871 |
1871 |
1872 text {* |
1872 text {* |
1873 \noindent |
1873 \noindent |
1874 \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and |
1874 \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and |
1875 the next state @{term "e#s"}, where \mbox{@{term "e = Create th prio"}}, are both valid (meaning the event |
1875 the next state @{term "e#s"}, whereby \mbox{@{term "e \<equiv> Create th prio"}}, are both valid (meaning the event |
1876 is allowed to occur in @{text s}). In this situation we can show that |
1876 @{text "Create"} is allowed to occur in @{text s}). In this situation we can show that |
1877 |
1877 |
1878 \begin{isabelle}\ \ \ \ \ %%% |
1878 \begin{isabelle}\ \ \ \ \ %%% |
1879 \begin{tabular}{@ {}l} |
1879 \begin{tabular}{@ {}l} |
1880 @{thm (concl) valid_trace_create.RAG_es},\\ |
1880 @{thm (concl) valid_trace_create.RAG_es},\\ |
1881 @{thm (concl) valid_trace_create.eq_cp_th}, and\\ |
1881 @{thm (concl) valid_trace_create.eq_cp_th}, and\\ |
1890 \smallskip |
1890 \smallskip |
1891 *} |
1891 *} |
1892 |
1892 |
1893 text {* |
1893 text {* |
1894 \noindent |
1894 \noindent |
1895 \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and |
1895 \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s} and |
1896 the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that |
1896 the next state @{term "e#s"}, whereby this time @{term "e \<equiv> Exit th"}, are both valid. We can show that |
1897 |
1897 |
1898 \begin{isabelle}\ \ \ \ \ %%% |
1898 \begin{isabelle}\ \ \ \ \ %%% |
1899 \begin{tabular}{@ {}l} |
1899 \begin{tabular}{@ {}l} |
1900 HERE %@ {thm valid_trace_create.eq_dep}, and\\ |
1900 @{thm (concl) valid_trace_exit.RAG_es}, and\\ |
1901 @{thm[mode=IfThen] valid_trace_create.eq_cp} |
1901 @{text "If"} @{thm (prem 2) valid_trace_exit.eq_cp} @{text "then"} @{thm (concl) valid_trace_exit.eq_cp} |
1902 \end{tabular} |
1902 \end{tabular} |
1903 \end{isabelle} |
1903 \end{isabelle} |
1904 |
1904 |
1905 \noindent |
1905 \noindent |
1906 This means again we do not have to recalculate the @{text RAG} and |
1906 This means again we do not have to recalculate the @{text RAG} and |
1910 \smallskip |
1910 \smallskip |
1911 *} |
1911 *} |
1912 |
1912 |
1913 text {* |
1913 text {* |
1914 \noindent |
1914 \noindent |
1915 \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and |
1915 \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s} and |
1916 @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that |
1916 @{term "e#s"} with @{term "e \<equiv> Set th prio"} are both valid. We can show that |
1917 |
1917 |
1918 \begin{isabelle}\ \ \ \ \ %%% |
1918 \begin{isabelle}\ \ \ \ \ %%% |
1919 \begin{tabular}{@ {}l} |
1919 \begin{tabular}{@ {}l} |
1920 %@ {thm[mode=IfThen] eq_dep}, and\\ |
1920 @{thm (concl) valid_trace_set.RAG_es}, and\\ |
1921 %@ {thm[mode=IfThen] valid_trace_create.eq_cp_pre} |
1921 @{text "If"} @{thm (prem 2) valid_trace_set.eq_cp} @{text "then"} @{thm (concl) valid_trace_set.eq_cp} |
1922 \end{tabular} |
1922 \end{tabular} |
1923 \end{isabelle} |
1923 \end{isabelle} |
1924 |
1924 |
1925 \noindent |
1925 \noindent The first property is again telling us we do not need to |
1926 The first property is again telling us we do not need to change the @{text RAG}. |
1926 change the @{text RAG}. The second shows that the @{term cp}-values |
1927 The second shows that the @{term cp}-values of all threads other than @{text th} |
1927 of all threads other than @{text th} are unchanged. The reason for |
1928 are unchanged. The reason is that @{text th} is running; therefore it is not in |
1928 this is more subtle: Since @{text th} must be running, that is does |
1929 the @{term dependants} relation of any other thread. This in turn means that the |
1929 not wait for any resource to be released, it cannot be in any |
1930 change of its priority cannot affect other threads. |
1930 subtree of any other thread. So all current precedences of other |
|
1931 threads are unchanged. |
1931 |
1932 |
1932 %The second |
1933 %The second |
1933 %however states that only threads that are \emph{not} dependants of @{text th} have their |
1934 %however states that only threads that are \emph{not} dependants of @{text th} have their |
1934 %current precedence unchanged. For the others we have to recalculate the current |
1935 %current precedence unchanged. For the others we have to recalculate the current |
1935 %precedence. To do this we can start from @{term "th"} |
1936 %precedence. To do this we can start from @{term "th"} |
1966 in turn. Suppose in state @{text s}, the thread @{text th'} takes over |
1967 in turn. Suppose in state @{text s}, the thread @{text th'} takes over |
1967 resource @{text cs} from thread @{text th}. We can prove |
1968 resource @{text cs} from thread @{text th}. We can prove |
1968 |
1969 |
1969 |
1970 |
1970 \begin{isabelle}\ \ \ \ \ %%% |
1971 \begin{isabelle}\ \ \ \ \ %%% |
|
1972 @{thm (concl) valid_trace_v_n.RAG_s}\\ |
1971 %@ {thm RAG_s} |
1973 %@ {thm RAG_s} |
1972 \end{isabelle} |
1974 \end{isabelle} |
1973 |
1975 |
1974 \noindent |
1976 \noindent |
1975 which shows how the @{text RAG} needs to be changed. The next lemma suggests |
1977 which shows how the @{text RAG} needs to be changed. The next lemma suggests |