equal
deleted
inserted
replaced
2047 @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"} |
2047 @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"} |
2048 \end{tabular} |
2048 \end{tabular} |
2049 \end{isabelle} |
2049 \end{isabelle} |
2050 |
2050 |
2051 \noindent This means we need to add a holding edge to the @{text |
2051 \noindent This means we need to add a holding edge to the @{text |
2052 RAG}. However, note while the @{text RAG} changes the corresponding |
2052 RAG}. However, note that while the @{text RAG} changes the corresponding |
2053 @{text TDG} does not change. Together with the fact that the |
2053 @{text TDG} does not change. Together with the fact that the |
2054 precedences of all threads are unchanged, no @{text cprec} value is |
2054 precedences of all threads are unchanged, no @{text cprec} value is |
2055 changed. Therefore, no recalucation of the @{text cprec} value |
2055 changed. Therefore, no recalucation of the @{text cprec} value |
2056 of any thread @{text "th''"} is needed. |
2056 of any thread @{text "th''"} is needed. |
2057 |
2057 |
2061 \noindent |
2061 \noindent |
2062 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 |
2063 |
2063 |
2064 \begin{isabelle}\ \ \ \ \ %%% |
2064 \begin{isabelle}\ \ \ \ \ %%% |
2065 \begin{tabular}{@ {}l} |
2065 \begin{tabular}{@ {}l} |
2066 %@ {thm (concl) valid_trace_p_hRAG_s}\\ |
2066 @{thm (concl) valid_trace_p_w.RAG_es}\\ |
2067 %@ {thm (concl) valid_trace_p_h.eq_cp} |
2067 @{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept} @{text "then"} |
|
2068 @{thm (concl) valid_trace_p_w.cp_kept_tG} |
2068 \end{tabular} |
2069 \end{tabular} |
2069 \end{isabelle} |
2070 \end{isabelle} |
2070 |
2071 |
2071 \noindent |
2072 \noindent |
2072 That means we have to add a waiting edge to the @{text RAG}. Furthermore |
2073 That means we have to add a waiting edge to the @{text RAG}. Furthermore |