2010 \noindent |
2010 \noindent |
2011 This means the recalculation of the @{text cprec} of @{text "th"} and |
2011 This means the recalculation of the @{text cprec} of @{text "th"} and |
2012 @{text "th'"} can be done independently and also done locally by only |
2012 @{text "th'"} can be done independently and also done locally by only |
2013 looking at the children: according to \eqref{fone} and \eqref{ftwo} |
2013 looking at the children: according to \eqref{fone} and \eqref{ftwo} |
2014 none of the @{text cprecs} of the children |
2014 none of the @{text cprecs} of the children |
2015 changes, just the children-sets changes by a @{text V}-event. This |
2015 changes, just the children-sets changes by a @{text V}-event. |
2016 in turn means the recalculation of |
2016 |
2017 @{text cprec} for @{text th} and @{text "th'"} terminates since |
|
2018 none of the @{text cprec} need the be recalculated. |
|
2019 |
2017 |
2020 *} |
2018 *} |
2021 |
2019 |
2022 text {* |
2020 text {* |
2023 \noindent |
2021 \noindent |
2024 In the other case where there is no thread that takes over @{text cs}, |
2022 In the other case where there is no thread that takes over @{text cs}, |
2025 we can show how |
2023 we can show how |
2026 to recalculate the @{text RAG} and also show that no current precedence needs |
2024 to recalculate the @{text RAG} and also show that no current precedence needs |
2027 to be recalculated. |
2025 to be recalculated for any thread @{text "th''"}. |
2028 |
2026 |
2029 \begin{isabelle}\ \ \ \ \ %%% |
2027 \begin{isabelle}\ \ \ \ \ %%% |
2030 \begin{tabular}{@ {}l} |
2028 \begin{tabular}{@ {}l} |
2031 @{thm (concl) valid_trace_v_e.RAG_s}\\ |
2029 @{thm (concl) valid_trace_v_e.RAG_s}\\ |
2032 @{thm (concl) valid_trace_v_e.eq_cp} |
2030 @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"} |
2033 \end{tabular} |
2031 \end{tabular} |
2034 \end{isabelle} |
2032 \end{isabelle} |
2035 *} |
2033 *} |
2036 |
2034 |
2037 text {* |
2035 text {* |
2043 treat the former case |
2041 treat the former case |
2044 first by showing that |
2042 first by showing that |
2045 |
2043 |
2046 \begin{isabelle}\ \ \ \ \ %%% |
2044 \begin{isabelle}\ \ \ \ \ %%% |
2047 \begin{tabular}{@ {}l} |
2045 \begin{tabular}{@ {}l} |
2048 @{thm valid_trace_p_h.RAG_es}\\ |
2046 @{thm (concl) valid_trace_p_h.RAG_es}\\ |
2049 %@ { thm valid_trace_p_h.eq_cp} |
2047 @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"} |
2050 \end{tabular} |
2048 \end{tabular} |
2051 \end{isabelle} |
2049 \end{isabelle} |
2052 |
2050 |
2053 \noindent |
2051 \noindent This means we need to add a holding edge to the @{text |
2054 This means we need to add a holding edge to the @{text RAG} and no |
2052 RAG}. However, note while the @{text RAG} changes the corresponding |
2055 current precedence needs to be recalculated.*} |
2053 @{text TDG} does not change. Together with the fact that the |
|
2054 precedences of all threads are unchanged, no @{text cprec} value is |
|
2055 changed. Therefore, no recalucation of the @{text cprec} value |
|
2056 of any thread @{text "th''"} is needed. |
|
2057 |
|
2058 *} |
2056 |
2059 |
2057 text {* |
2060 text {* |
2058 \noindent |
2061 \noindent |
2059 In the second case we know that resource @{text cs} is locked. We can show that |
2062 In the second case we know that resource @{text cs} is locked. We can show that |
2060 |
2063 |
2061 \begin{isabelle}\ \ \ \ \ %%% |
2064 \begin{isabelle}\ \ \ \ \ %%% |
2062 \begin{tabular}{@ {}l} |
2065 \begin{tabular}{@ {}l} |
2063 %@ {thm RAG_s}\\ |
2066 %@ {thm (concl) valid_trace_p_hRAG_s}\\ |
2064 HERE %@ {thm[mode=IfThen] eq_cp} |
2067 %@ {thm (concl) valid_trace_p_h.eq_cp} |
2065 \end{tabular} |
2068 \end{tabular} |
2066 \end{isabelle} |
2069 \end{isabelle} |
2067 |
2070 |
2068 \noindent |
2071 \noindent |
2069 That means we have to add a waiting edge to the @{text RAG}. Furthermore |
2072 That means we have to add a waiting edge to the @{text RAG}. Furthermore |