pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:ab1a9ae35dd6
+:71a3300d497b
 when a thread \emph{holds}, respectively \emph{waits} for, a
 resource @{text cs} given a waiting queue function @{text wq}.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm cs_holding_def[where thread="th"]}\\
+@{thm cs_holding_raw[where thread="th"]}\\
-@{thm cs_waiting_def[where thread="th"]}
+@{thm cs_waiting_raw[where thread="th"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 In this definition we assume @{text "set"} converts a list into a set.
 \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a
 datatype for vertices). Given a waiting queue function, a RAG is defined
 as the union of the sets of waiting and holding edges, namely
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm cs_RAG_def}
+@{thm cs_RAG_raw}
 \end{isabelle}
 \begin{figure}[t]
 \begin{center}
 properties are:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 HERE??
-%@ {thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
+%@ {thm[mode=IfThen] waiting_unique[of _ _ "cs1" "cs2"]}\\
-%@ {thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
+%@ {thm[mode=IfThen] held_unique[of _ "th1" _ "th2"]}\\
-%@ {thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
+%@ {thm[mode=IfThen] runing_unique[of _ "th1" "th2"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 The first property states that every waiting thread can only wait for a single
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 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}
 \noindent
 The acyclicity property follows from how we restricted the events in
 %The following lemmas show how every node in RAG can be chased to ready threads:
 %\begin{enumerate}
 %\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:
 %\begin{enumerate}
 %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
 scheduler and coding how it should react to events.  Below we
 outline how our formalisation guides this implementation for each
 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
 the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
 is allowed to occur). In this situation we can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 HERE ?? %@ {thm eq_dep},\\
-@{thm eq_cp_th}, and\\
+@{thm valid_trace_create.eq_cp_th}, and\\
-@{thm[mode=IfThen] eq_cp}
+@{thm[mode=IfThen] valid_trace_create.eq_cp}
 \end{tabular}
 \end{isabelle}
 \noindent
 This means in an implementation we do not have to recalculate the @{text RAG} and also none of the
 current precedences of the other threads. The current precedence of the created
 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
 the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-HERE %@ {thm eq_dep}, and\\
+HERE %@ {thm valid_trace_create.eq_dep}, and\\
-@{thm[mode=IfThen] eq_cp}
+@{thm[mode=IfThen] valid_trace_create.eq_cp}
 \end{tabular}
 \end{isabelle}
 \noindent
 This means again we do not have to recalculate the @{text RAG} and
 also not the current precedences for the other threads. Since @{term th} is not
 alive anymore in state @{term "s"}, there is no need to calculate its
 current precedence.
 \smallskip
 *}
-(*<*)
-end
-context step_set_cps
-begin
-(*>*)
 text {*
 \noindent
 \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and
 @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm[mode=IfThen] eq_dep}, and\\
+%@ {thm[mode=IfThen] eq_dep}, and\\
-@{thm[mode=IfThen] eq_cp_pre}
+%@ {thm[mode=IfThen] valid_trace_create.eq_cp_pre}
 \end{tabular}
 \end{isabelle}
 \noindent
 The first property is again telling us we do not need to change the @{text RAG}.
 %The second 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.
 \smallskip
 *}
-(*<*)
-end
-context step_v_cps_nt
-begin
-(*>*)
 text {*
 \noindent
 \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and
 @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
 subcases: one where there is a thread to ``take over'' the released
 in turn. Suppose in state @{text s}, the thread @{text th'} takes over
 resource @{text cs} from thread @{text th}. We can prove
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm RAG_s}
+%@ {thm RAG_s}
 \end{isabelle}
 \noindent
 which shows how the @{text RAG} needs to be changed. The next lemma suggests
 how the current precedences need to be recalculated. For threads that are
 not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
 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
 to be recalculated.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm RAG_s}\\
+%@ {thm RAG_s}\\
-@{thm eq_cp}
+%@ {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
 @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
 the one where @{text cs} is not locked, and one where it is. We treat the former case
 first by showing that
 \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}
 \noindent
 \noindent
 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
 be recalculated for an event. This information is provided by the lemmas we proved.
 We confirmed that our observations translate into practice by implementing

changeset 124	71a3300d497b
parent 95	8d2cc27f45f3
child 125	95e7933968f8