Theory ThreadTracking
section "Thread Tracking"
theory ThreadTracking
imports Main "HOL-Library.Multiset" LTS Misc
begin
text_raw ‹\label{thy:ThreadTracking}›
text ‹
This theory defines some general notion of an interleaving semantics. It defines how to extend a semantics specified on a single thread and a context to a semantic on multisets of threads.
The context is needed in order to keep track of synchronization.
›
subsection "Semantic on multiset configuration"
text ‹The interleaving semantics is defined on a multiset of stacks. The thread to make the next step is nondeterministically chosen from all threads ready to make steps.›
definition
"gtr gtrs == { (add_mset s c,e,add_mset s' c') | s c e s' c' . ((s,c),e,(s',c'))∈gtrs }"
lemma gtrI_s: "((s,c),e,(s',c'))∈gtrs ⟹ (add_mset s c,e,add_mset s' c')∈gtr gtrs"
by (unfold gtr_def, auto)
lemma gtrI: "((s,c),w,(s',c'))∈trcl gtrs
⟹ (add_mset s c,w,add_mset s' c')∈trcl (gtr gtrs)"
by (induct rule: trcl_pair_induct) (auto dest: gtrI_s)
lemma gtrE: "⟦
(c,e,c')∈gtr T;
!!s ce s' ce'. ⟦ c=add_mset s ce; c'=add_mset s' ce'; ((s,ce),e,(s',ce'))∈T ⟧ ⟹ P
⟧ ⟹ P"
by (unfold gtr_def) auto
lemma gtr_empty_conf_s[simp]:
"({#},w,c')∉gtr S"
"(c,w,{#})∉gtr S"
by (auto elim: gtrE)
lemma gtr_empty_conf1[simp]: "(({#},w,c')∈trcl (gtr S)) ⟷ (w=[] ∧ c'={#})"
by (induct w) (auto dest: trcl_uncons)
lemma gtr_empty_conf2[simp]: "((c,w,{#})∈trcl (gtr S)) ⟷ (w=[] ∧ c={#})"
by (induct w rule: rev_induct) (auto dest: trcl_rev_uncons)
lemma gtr_find_thread: "⟦
(c,e,c')∈gtr gtrs;
!!s ce s' ce'. ⟦c=add_mset s ce; c'=add_mset s' ce'; ((s,ce),e,(s',ce'))∈gtrs⟧ ⟹ P
⟧ ⟹ P"
by (unfold gtr_def) auto
lemma gtr_step_cases[cases set, case_names loc other]: "⟦
(add_mset s ce,e,c')∈gtr gtrs;
!!s' ce'. ⟦ c'=add_mset s' ce'; ((s,ce),e,(s',ce'))∈gtrs ⟧ ⟹ P;
!!cc ss ss' ce'. ⟦ ce=add_mset ss cc; c'=add_mset ss' ce';
((ss,add_mset s cc),e,(ss',ce'))∈gtrs ⟧ ⟹ P
⟧ ⟹ P"
by (auto elim!: gtr_find_thread mset_single_cases)
lemma gtr_rev_cases[cases set, case_names loc other]: "⟦
(c,e,add_mset s' ce')∈gtr gtrs;
!!s ce. ⟦ c=add_mset s ce; ((s,ce),e,(s',ce'))∈gtrs ⟧ ⟹ P;
!!cc ss ss' ce. ⟦ c=add_mset ss ce; ce'=add_mset ss' cc;
((ss,ce),e,(ss',add_mset s' cc))∈gtrs ⟧ ⟹ P
⟧ ⟹ P"
by (auto elim!: gtr_find_thread mset_single_cases)
subsection "Invariants"
lemma gtr_preserve_s: "⟦
(c,e,c')∈gtr T;
P c;
!!s c s' c' e. ⟦P (add_mset s c); ((s,c),e,(s',c'))∈T⟧ ⟹ P (add_mset s' c')
⟧ ⟹ P c'"
by (unfold gtr_def) blast
lemma gtr_preserve: "⟦
(c,w,c')∈trcl (gtr T);
P c;
!!s c s' c' e. ⟦P (add_mset s c); ((s,c),e,(s',c'))∈T⟧ ⟹ P (add_mset s' c')
⟧ ⟹ P c'"
apply (induct rule: trcl.induct)
apply simp
apply (subgoal_tac "P c'")
apply blast
apply (blast intro: gtr_preserve_s)
done
subsection "Context preservation assumption"
text ‹
We now assume that the original semantics does not modify threads in the context, i.e. it may only add new threads to the context and use the context to obtain monitor information, but not change any
existing thread in the context. This assumption is valid for our semantics, where the context is just needed to determine the set of allocated monitors. It allows us to generally derive some further properties of
such semantics.
›
locale env_no_step =
fixes gtrs :: "(('s×'s multiset),'l) LTS"
assumes env_no_step_s[cases set, case_names csp]:
"⟦((s,c),e,(s',c'))∈gtrs; !!csp. c'=csp+c ⟹ P ⟧ ⟹ P"
lemma (in env_no_step) env_no_step[cases set, case_names csp]: "⟦
((s,c),w,(s',c'))∈trcl gtrs;
!! csp. c'=csp+c ⟹ P
⟧ ⟹ P"
proof -
have "((s,c),w,(s',c'))∈trcl gtrs ⟹ ∃csp. c'=csp+c" proof (induct rule: trcl_pair_induct)
case empty thus ?case by (auto intro: exI[of _ "{#}"])
next
case (cons s c e sh ch w s' c') note IHP=this
from env_no_step_s[OF IHP(1)] obtain csph where "ch=csph+c" by auto
moreover from IHP(3) obtain csp' where "c'=csp'+ch" by auto
ultimately have "c'=csp'+csph+c" by (simp add: union_assoc)
thus ?case by blast
qed
moreover assume "((s,c),w,(s',c'))∈trcl gtrs" "!! csp. c'=csp+c ⟹ P"
ultimately show ?thesis by blast
qed
text ‹
The following lemma can be used to make a case distinction how a step operated on a given thread in the end configuration:
\begin{description}
\item[‹loc›] The thread made the step
\item[‹spawn›] The thread was spawned by the step
\item[‹env›] The thread was not involved in the step
\end{description}
›
lemma (in env_no_step) rev_cases_p[cases set, case_names loc spawn env]:
assumes STEP: "(c,e,add_mset s' ce')∈gtr gtrs" and
LOC: "!!s ce. ⟦ c={#s#}+ce; ((s,ce),e,(s',ce'))∈gtrs ⟧ ⟹ P" and
SPAWN: "!!ss ss' ce csp.
⟦ c=add_mset ss ce; ce'=add_mset ss' (csp+ce);
((ss,ce),e,(ss',add_mset s' (csp+ce)))∈gtrs ⟧
⟹ P" and
ENV: "!!ss ss' ce csp.
⟦ c=add_mset ss (add_mset s' ce); ce'=add_mset ss' (csp+ce);
((ss,add_mset s' ce),e,(ss',csp+(add_mset s' ce)))∈gtrs ⟧
⟹ P"
shows "P"
proof (rule gtr_rev_cases[OF STEP], goal_cases)
case 1 thus ?thesis using LOC by auto
next
case CASE: (2 cc ss ss' ce)
hence CASE': "c = {#ss#} + ce" "ce' = {#ss'#} + cc" "((ss, ce), e, ss', {#s'#} + cc) ∈ gtrs" by simp_all
from env_no_step_s[OF CASE'(3)] obtain csp where EQ: "add_mset s' cc = csp + ce" by auto
thus ?thesis proof (cases rule: mset_unplusm_dist_cases)
case left note CC=this
with CASE' have "ce'={#ss'#} + (csp-{#s'#}) + ce" by (auto simp add: union_assoc)
moreover from CC(2) have "{#s'#}+cc = {#s'#} + (csp-{#s'#}) + ce" by (simp add: union_assoc)
ultimately show ?thesis using CASE'(1,3) CASE(2) SPAWN by auto
next
case right note CC=this
from CC(1) CASE'(1) have "c=add_mset ss (add_mset s' (ce - {#s'#}))" by (simp add: union_assoc)
moreover from CC(2) CASE'(2) have "ce'=add_mset ss' (csp+(ce-{#s'#}))" by (simp add: union_assoc)
moreover from CC(2) have "add_mset s' cc = csp+(add_mset s' (ce-{#s'#}))" by (simp add: union_ac)
ultimately show ?thesis using CASE'(3) CASE(3) CC(1) ENV by metis
qed
qed
subsection "Explicit local context"
text_raw ‹\label{sec:ThreadTracking:exp_local}›
text ‹
In the multiset semantics, a single thread has no identity. This may become a problem when reasoning about a fixed thread during an execution. For example, in our constraint-system-based approach
the operational characterization of the least solution of the constraint system requires to state properties of the steps of the initial thread in some execution. With the multiset semantics, we are unable
to identify those steps among all steps.
There are many solutions to this problem, for example, using thread ids either as part of the thread's configuration or as part of the whole configuration by using
lists of stacks or maps from ids to stacks as configuration datatype.
In the following we present a special solution that is strong enough to suit our purposes but not meant as a general solution.
Instead of identifying every single thread uniquely, we only distinguish one thread as the {\em local} thread. The other
threads are {\em environment} threads. We then attach to every step the information whether it was on the local or on some environment thread.
We call this semantics {\em loc/env}-semantics in contrast to the {\em multiset}-semantics of the last section.
›
subsubsection "Lifted step datatype"