1958 \smallskip |
1958 \smallskip |
1959 *} |
1959 *} |
1960 |
1960 |
1961 text {* |
1961 text {* |
1962 \noindent |
1962 \noindent |
1963 \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and |
1963 \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s} and |
1964 @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two |
1964 @{term "e#s"} with @{text e} being @{term "V th cs"} are both valid. |
|
1965 We have to consider two |
1965 subcases: one where there is a thread to ``take over'' the released |
1966 subcases: one where there is a thread to ``take over'' the released |
1966 resource @{text cs}, and one where there is not. Let us consider them |
1967 resource @{text cs}, and one where there is not. Let us consider them |
1967 in turn. Suppose in state @{text s}, the thread @{text th'} takes over |
1968 in turn. Suppose in state @{text s}, the thread @{text th'} takes over |
1968 resource @{text cs} from thread @{text th}. We can prove |
1969 resource @{text cs} from thread @{text th}. We can prove |
1969 |
1970 |
1970 |
1971 |
1971 \begin{isabelle}\ \ \ \ \ %%% |
1972 \begin{isabelle}\ \ \ \ \ %%% |
1972 @{thm (concl) valid_trace_v_n.RAG_s}\\ |
1973 %@ { thm (concl) valid_trace_v_n.RAG_s}\\ |
1973 %@ {thm RAG_s} |
1974 @{term "RAG (e#s) = RAG s - {(C cs,T th), (T th',C cs)} \<union> {(C cs, T th')}"} |
1974 \end{isabelle} |
1975 \end{isabelle} |
1975 |
1976 |
1976 \noindent |
1977 \noindent |
1977 which shows how the @{text RAG} needs to be changed. The next lemma suggests |
1978 which shows how the @{text RAG} needs to be changed. The next lemma suggests |
1978 how the current precedences need to be recalculated. For threads that are |
1979 how the current precedences need to be recalculated. For threads that are |
1979 not @{text "th"} and @{text "th'"} nothing needs to be changed, since we |
1980 not @{text "th"} and @{text "th'"} nothing needs to be changed, since we |
1980 can show |
1981 can show |
1981 |
1982 |
1982 \begin{isabelle}\ \ \ \ \ %%% |
1983 \begin{isabelle}\ \ \ \ \ %%% |
1983 %@ {thm[mode=IfThen] cp_kept} |
1984 @{text "If"} @{text "th'' \<noteq> th"} and |
|
1985 @{text "th'' \<noteq> th'"} |
|
1986 @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]} |
1984 \end{isabelle} |
1987 \end{isabelle} |
1985 |
1988 |
1986 \noindent |
1989 \noindent |
1987 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to |
1990 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to |
1988 recalculate their current precedence since their children have changed. *} |
1991 recalculate their current precedence since their children have changed. |
|
1992 |
|
1993 |
|
1994 \begin{isabelle}\ \ \ \ \ %%% |
|
1995 @{thm (concl) valid_trace_v_n.t1}\\ |
|
1996 @{thm (concl) valid_trace_v_n.t2} |
|
1997 \end{isabelle} |
|
1998 *} |
1989 |
1999 |
1990 text {* |
2000 text {* |
1991 \noindent |
2001 \noindent |
1992 In the other case where there is no thread that takes over @{text cs}, we can show how |
2002 In the other case where there is no thread that takes over @{text cs}, |
|
2003 we can show how |
1993 to recalculate the @{text RAG} and also show that no current precedence needs |
2004 to recalculate the @{text RAG} and also show that no current precedence needs |
1994 to be recalculated. |
2005 to be recalculated. |
1995 |
2006 |
1996 \begin{isabelle}\ \ \ \ \ %%% |
2007 \begin{isabelle}\ \ \ \ \ %%% |
1997 \begin{tabular}{@ {}l} |
2008 \begin{tabular}{@ {}l} |
1998 %@ {thm RAG_s}\\ |
2009 @{thm (concl) valid_trace_v_e.RAG_s}\\ |
1999 %@ {thm eq_cp} |
2010 @{thm (concl) valid_trace_v_e.eq_cp} |
2000 \end{tabular} |
2011 \end{tabular} |
2001 \end{isabelle} |
2012 \end{isabelle} |
2002 *} |
2013 *} |
2003 |
2014 |
2004 text {* |
2015 text {* |
2005 \noindent |
2016 \noindent |
2006 \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and |
2017 \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s} and |
2007 @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely |
2018 @{term "e#s"} with @{term "e \<equiv> P th cs"} are both valid. |
2008 the one where @{text cs} is not locked, and one where it is. We treat the former case |
2019 We again have to analyse two subcases, namely |
|
2020 the one where @{text cs} is not locked, and one where it is. We |
|
2021 treat the former case |
2009 first by showing that |
2022 first by showing that |
2010 |
2023 |
2011 \begin{isabelle}\ \ \ \ \ %%% |
2024 \begin{isabelle}\ \ \ \ \ %%% |
2012 \begin{tabular}{@ {}l} |
2025 \begin{tabular}{@ {}l} |
2013 %@ {thm RAG_s}\\ |
2026 @{thm valid_trace_p_h.RAG_es}\\ |
2014 HERE %@ {thm eq_cp} |
2027 %@ { thm valid_trace_p_h.eq_cp} |
2015 \end{tabular} |
2028 \end{tabular} |
2016 \end{isabelle} |
2029 \end{isabelle} |
2017 |
2030 |
2018 \noindent |
2031 \noindent |
2019 This means we need to add a holding edge to the @{text RAG} and no |
2032 This means we need to add a holding edge to the @{text RAG} and no |