# HG changeset patch # User Christian Urban # Date 1460727849 -3600 # Node ID 71a3300d497b1ecfc03627f550003dabd87c30c5 # Parent ab1a9ae35dd6cff9f9d19589727386b2c1dc0760 updated journal paper diff -r ab1a9ae35dd6 -r 71a3300d497b Journal/Paper.thy --- a/Journal/Paper.thy Fri Apr 15 13:52:07 2016 +0100 +++ b/Journal/Paper.thy Fri Apr 15 14:44:09 2016 +0100 @@ -411,8 +411,8 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm cs_holding_def[where thread="th"]}\\ - @{thm cs_waiting_def[where thread="th"]} + @{thm cs_holding_raw[where thread="th"]}\\ + @{thm cs_waiting_raw[where thread="th"]} \end{tabular} \end{isabelle} @@ -445,7 +445,7 @@ as the union of the sets of waiting and holding edges, namely \begin{isabelle}\ \ \ \ \ %%% - @{thm cs_RAG_def} + @{thm cs_RAG_raw} \end{isabelle} @@ -1034,9 +1034,9 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} HERE?? - %@ {thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\ - %@ {thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\ - %@ {thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]} + %@ {thm[mode=IfThen] waiting_unique[of _ _ "cs1" "cs2"]}\\ + %@ {thm[mode=IfThen] held_unique[of _ "th1" _ "th2"]}\\ + %@ {thm[mode=IfThen] runing_unique[of _ "th1" "th2"]} \end{tabular} \end{isabelle} @@ -1053,10 +1053,10 @@ HERE?? %@{text If}~@ {thm (prem 1) acyclic_RAG}~@{text "then"}:\\ \hspace{5mm}@{thm (concl) acyclic_RAG}, @{thm (concl) finite_RAG} and - @{thm (concl) wf_dep_converse},\\ + %@ {thm (concl) wf_dep_converse},\\ %\hspace{5mm}@{text "if"}~@ {thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads} and\\ - %\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}. + %\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~% @ {thm (concl) range_in}. \end{tabular} \end{isabelle} @@ -1135,7 +1135,7 @@ %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): % @ {thm [display] chain_building[rule_format]} %\item The ready thread chased to is unique (@{text "dchain_unique"}): - % @ {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]} + % @ {thm [display] dchain_unique[of _ _ "th1" "th2"]} %\end{enumerate} %Some deeper results about the system: @@ -1305,10 +1305,6 @@ kind of events.\smallskip *} -(*<*) -context step_create_cps -begin -(*>*) text {* \noindent \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and @@ -1318,8 +1314,8 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} HERE ?? %@ {thm eq_dep},\\ - @{thm eq_cp_th}, and\\ - @{thm[mode=IfThen] eq_cp} + @{thm valid_trace_create.eq_cp_th}, and\\ + @{thm[mode=IfThen] valid_trace_create.eq_cp} \end{tabular} \end{isabelle} @@ -1329,11 +1325,7 @@ thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}. \smallskip *} -(*<*) -end -context step_exit_cps -begin -(*>*) + text {* \noindent \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and @@ -1341,8 +1333,8 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - HERE %@ {thm eq_dep}, and\\ - @{thm[mode=IfThen] eq_cp} + HERE %@ {thm valid_trace_create.eq_dep}, and\\ + @{thm[mode=IfThen] valid_trace_create.eq_cp} \end{tabular} \end{isabelle} @@ -1353,11 +1345,7 @@ current precedence. \smallskip *} -(*<*) -end -context step_set_cps -begin -(*>*) + text {* \noindent \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and @@ -1365,8 +1353,8 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm[mode=IfThen] eq_dep}, and\\ - @{thm[mode=IfThen] eq_cp_pre} + %@ {thm[mode=IfThen] eq_dep}, and\\ + %@ {thm[mode=IfThen] valid_trace_create.eq_cp_pre} \end{tabular} \end{isabelle} @@ -1404,11 +1392,7 @@ %have their current precedence changed. \smallskip *} -(*<*) -end -context step_v_cps_nt -begin -(*>*) + text {* \noindent \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and @@ -1420,7 +1404,7 @@ \begin{isabelle}\ \ \ \ \ %%% - @{thm RAG_s} + %@ {thm RAG_s} \end{isabelle} \noindent @@ -1430,12 +1414,14 @@ can show \begin{isabelle}\ \ \ \ \ %%% - @{thm[mode=IfThen] cp_kept} + %@ {thm[mode=IfThen] cp_kept} \end{isabelle} \noindent For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to - recalculate their current precedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {* + recalculate their current precedence since their children have changed. *} + +text {* \noindent In the other case where there is no thread that takes over @{text cs}, we can show how to recalculate the @{text RAG} and also show that no current precedence needs @@ -1443,16 +1429,12 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm RAG_s}\\ - @{thm eq_cp} + %@ {thm RAG_s}\\ + %@ {thm eq_cp} \end{tabular} \end{isabelle} *} -(*<*) -end -context step_P_cps_e -begin -(*>*) + text {* \noindent \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and @@ -1462,20 +1444,22 @@ \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm RAG_s}\\ + %@ {thm RAG_s}\\ HERE %@ {thm eq_cp} \end{tabular} \end{isabelle} \noindent This means we need to add a holding edge to the @{text RAG} and no - current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {* + current precedence needs to be recalculated.*} + +text {* \noindent In the second case we know that resource @{text cs} is locked. We can show that \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{thm RAG_s}\\ + %@ {thm RAG_s}\\ HERE %@ {thm[mode=IfThen] eq_cp} \end{tabular} \end{isabelle} @@ -1505,7 +1489,9 @@ This lemma states that if an intermediate @{term cp}-value does not change, then the procedure can also stop, because none of its dependent threads will have their current precedence changed. - *}(*<*)end(*>*)text {* + *} + +text {* As can be seen, a pleasing byproduct of our formalisation is that the properties in this section closely inform an implementation of PIP, namely whether the RAG needs to be reconfigured or current precedences need to diff -r ab1a9ae35dd6 -r 71a3300d497b journal.pdf Binary file journal.pdf has changed