Theory JMM_Framework
section ‹Combination of locales for heap operations and interleaving›
theory JMM_Framework
imports
JMM_Heap
"../Framework/FWInitFinLift"
"../Common/WellForm"
begin
lemma enat_plus_eq_enat_conv:
"enat m + n = enat k ⟷ k ≥ m ∧ n = enat (k - m)"
by(cases n) auto
declare convert_new_thread_action_id [simp]
context heap begin
lemma init_fin_lift_state_start_state:
"init_fin_lift_state s (start_state f P C M vs) = start_state (λC M Ts T meth vs. (s, f C M Ts T meth vs)) P C M vs"
by(simp add: start_state_def init_fin_lift_state_def split_beta fun_eq_iff)
lemma non_speculative_start_heap_obs:
"non_speculative P vs (llist_of (map snd (lift_start_obs start_tid start_heap_obs)))"
apply(rule non_speculative_nthI)
using start_heap_obs_not_Read
by(clarsimp simp add: lift_start_obs_def lnth_LCons o_def eSuc_enat[symmetric] in_set_conv_nth split: nat.split_asm)
lemma ta_seq_consist_start_heap_obs:
"ta_seq_consist P Map.empty (llist_of (map snd (lift_start_obs start_tid start_heap_obs)))"
using start_heap_obs_not_Read
by(auto intro: ta_seq_consist_nthI simp add: lift_start_obs_def o_def lnth_LCons in_set_conv_nth split: nat.split_asm)
end
context allocated_heap begin
lemma w_addrs_lift_start_heap_obs:
"w_addrs (w_values P vs (map snd (lift_start_obs start_tid start_heap_obs))) ⊆ w_addrs vs"
by(simp add: lift_start_obs_def o_def w_addrs_start_heap_obs)
end
context heap begin
lemma w_values_start_heap_obs_typeable:
assumes wf: "wf_syscls P"
and mrws: "v ∈ w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs)) (ad, al)"
shows "∃T. P,start_heap ⊢ ad@al : T ∧ P,start_heap ⊢ v :≤ T"
proof -
from in_w_valuesD[OF mrws]
obtain obs' wa obs''
where eq: "map snd (lift_start_obs start_tid start_heap_obs) = obs' @ wa # obs''"
and "is_write_action wa"
and adal: "(ad, al) ∈ action_loc_aux P wa"
and vwa: "value_written_aux P wa al = v"
by blast
from ‹is_write_action wa› show ?thesis
proof cases
case (WriteMem ad' al' v')
with vwa adal eq have "WriteMem ad al v ∈ set start_heap_obs"
by(auto simp add: map_eq_append_conv Cons_eq_append_conv lift_start_obs_def)
thus ?thesis by(rule start_heap_write_typeable)
next
case (NewHeapElem ad' hT)
with vwa adal eq have "NewHeapElem ad hT ∈ set start_heap_obs"
by(auto simp add: map_eq_append_conv Cons_eq_append_conv lift_start_obs_def)
hence "typeof_addr start_heap ad = ⌊hT⌋"
by(rule NewHeapElem_start_heap_obsD[OF wf])
thus ?thesis using adal vwa NewHeapElem
apply(cases hT)
apply(auto intro!: addr_loc_type.intros dest: has_field_decl_above)
apply(frule has_field_decl_above)
apply(auto intro!: addr_loc_type.intros dest: has_field_decl_above)
done
qed
qed
lemma start_state_vs_conf:
"wf_syscls P ⟹ vs_conf P start_heap (w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs)))"
by(rule vs_confI)(rule w_values_start_heap_obs_typeable)
end
subsection ‹JMM traces for Jinja semantics›
context multithreaded_base begin
inductive_set ℰ :: "('l,'t,'x,'m,'w) state ⇒ ('t × 'o) llist set"
for σ :: "('l,'t,'x,'m,'w) state"
where
"mthr.Runs σ E'
⟹ lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') ∈ ℰ σ"
lemma actions_ℰE_aux:
fixes σ E'
defines "E == lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
assumes mthr: "mthr.Runs σ E'"
and a: "enat a < llength E"
obtains m n t ta
where "lnth E a = (t, ⦃ta⦄⇘o⇙ ! n)"
and "n < length ⦃ta⦄⇘o⇙" and "enat m < llength E'"
and "a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n"
and "lnth E' m = (t, ta)"
proof -
from lnth_lconcat_conv[OF a[unfolded E_def], folded E_def]
obtain m n
where "lnth E a = lnth (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') m) n"
and "enat n < llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') m)"
and "enat m < llength (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
and "enat a = (∑i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) + enat n"
by blast
moreover
obtain t ta where "lnth E' m = (t, ta)" by(cases "lnth E' m")
ultimately have E_a: "lnth E a = (t, ⦃ta⦄⇘o⇙ ! n)"
and n: "n < length ⦃ta⦄⇘o⇙"
and m: "enat m < llength E'"
and a: "enat a = (∑i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) + enat n"
by(simp_all)
note a
also have "(∑i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) =
sum (enat ∘ (λi. length ⦃snd (lnth E' i)⦄⇘o⇙)) {..<m}"
using m by(simp add: less_trans[where y="enat m"] split_beta)
also have "… = enat (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
by(subst sum_comp_morphism)(simp_all add: zero_enat_def)
finally have a: "a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n" by simp
with E_a n m show thesis using ‹lnth E' m = (t, ta)› by(rule that)
qed
lemma actions_ℰE:
assumes E: "E ∈ ℰ σ"
and a: "enat a < llength E"
obtains E' m n t ta
where "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
and "mthr.Runs σ E'"
and "lnth E a = (t, ⦃ta⦄⇘o⇙ ! n)"
and "n < length ⦃ta⦄⇘o⇙" and "enat m < llength E'"
and "a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n"
and "lnth E' m = (t, ta)"
proof -
from E obtain E' ws
where E: "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
and "mthr.Runs σ E'" by(rule ℰ.cases) blast
from ‹mthr.Runs σ E'› a[unfolded E]
show ?thesis
by(rule actions_ℰE_aux)(fold E, rule that[OF E ‹mthr.Runs σ E'›])
qed
end
context τmultithreaded_wf begin
text ‹Alternative characterisation for @{term "ℰ"}›
lemma ℰ_conv_Runs:
"ℰ σ = lconcat ` lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ` llist_of_tllist ` {E. mthr.τRuns σ E}"
(is "?lhs = ?rhs")
proof(intro equalityI subsetI)
fix E
assume "E ∈ ?rhs"
then obtain E' where E: "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of_tllist E'))"
and τRuns: "mthr.τRuns σ E'" by(blast)
obtain E'' where E': "E' = tmap (λ(tls, s', tl, s''). tl) (case_sum (λ(tls, s'). ⌊s'⌋) Map.empty) E''"
and τRuns': "mthr.τRuns_table2 σ E''"
using τRuns by(rule mthr.τRuns_into_τRuns_table2)
have "mthr.Runs σ (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E''))
(LCons (case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil)))"
(is "mthr.Runs _ ?E'''")
using τRuns' by(rule mthr.τRuns_table2_into_Runs)
moreover
let ?tail = "λE''. case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls"
{
have "E = lconcat (lfilter (λxs. ¬ lnull xs) (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of_tllist E')))"
unfolding E by(simp add: lconcat_lfilter_neq_LNil)
also have "… = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E''))))"
by(simp add: E' lfilter_lmap llist.map_comp o_def split_def)
also
from ‹mthr.τRuns_table2 σ E''›
have "lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E'')) =
lfilter (λ(t, ta). ⦃ta⦄⇘o⇙ ≠ []) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (?tail E'') LNil)))"
(is "?lhs σ E'' = ?rhs σ E''")
proof(coinduction arbitrary: σ E'' rule: llist.coinduct_strong)
case (Eq_llist σ E'')
have ?lnull
by(cases "lfinite (llist_of_tllist E'')")(fastforce split: sum.split_asm simp add: split_beta lset_lconcat_lfinite lappend_inf mthr.silent_move2_def dest: mthr.τRuns_table2_silentsD[OF Eq_llist] mthr.τRuns_table2_terminal_silentsD[OF Eq_llist] mthr.τRuns_table2_terminal_inf_stepD[OF Eq_llist] mτmove_silentD inf_step_silentD silent_moves2_silentD split: sum.split_asm)+
moreover
have ?LCons
proof(intro impI conjI)
assume lhs': "¬ lnull (lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E'')))"
(is "¬ lnull ?lhs'")
and "¬ lnull (lfilter (λ(t, ta). ⦃ta⦄⇘o⇙ ≠ []) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil))))"
(is "¬ lnull ?rhs'")
note τRuns' = ‹mthr.τRuns_table2 σ E''›
from lhs' obtain tl tls' where "?lhs σ E'' = LCons tl tls'"
by(auto simp only: not_lnull_conv)
then obtain tls s' s'' tlsstlss'
where tls': "tls' = lmap (λ(tls, s', tta, s''). tta) tlsstlss'"
and filter: "lfilter (λ(tls, s', (t, ta), s''). obs_a ta ≠ []) (llist_of_tllist E'') = LCons (tls, s', tl, s'') tlsstlss'"
using lhs' by(fastforce simp add: lmap_eq_LCons_conv)
from lfilter_eq_LConsD[OF filter]
obtain us vs where eq: "llist_of_tllist E'' = lappend us (LCons (tls, s', tl, s'') vs)"
and fin: "lfinite us"
and empty: "∀(tls, s', (t, ta), s'')∈lset us. obs_a ta = []"
and neq_empty: "obs_a (snd tl) ≠ []"
and tlsstlss': "tlsstlss' = lfilter (λ(tls, s', (t, ta), s''). obs_a ta ≠ []) vs"
by(auto simp add: split_beta)
from eq obtain E''' where E'': "E'' = lappendt us E'''"
and eq': "llist_of_tllist E''' = LCons (tls, s', tl, s'') vs"
and terminal: "terminal E''' = terminal E''"
unfolding llist_of_tllist_eq_lappend_conv by auto
from τRuns' fin E'' obtain σ' where τRuns'': "mthr.τRuns_table2 σ' E'''"
by(auto dest: mthr.τRuns_table2_lappendtD)
then obtain σ'' E'''' where "mthr.τRuns_table2 σ'' E''''" "E''' = TCons (tls, s', tl, s'') E''''"
using eq' by cases auto
moreover from τRuns' E'' fin
have "∀(tls, s, tl, s')∈lset us. ∀(t, ta)∈set tls. ta = ε"
by(fastforce dest: mthr.τRuns_table2_silentsD mτmove_silentD simp add: mthr.silent_move2_def)
hence "lfilter (λ(t, ta). obs_a ta ≠ []) (lconcat (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) us)) = LNil"
using empty by(auto simp add: lfilter_empty_conv lset_lconcat_lfinite split_beta)
moreover from τRuns'' eq' have "snd ` set tls ⊆ {ε}"
by(cases)(fastforce dest: silent_moves2_silentD)+
hence "[(t, ta)←tls . obs_a ta ≠ []] = []"
by(auto simp add: filter_empty_conv split_beta)
ultimately
show "lhd ?lhs' = lhd ?rhs'"
and "(∃σ E''. ltl ?lhs' = lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E'')) ∧
ltl ?rhs' = lfilter (λ(t, ta). ⦃ta⦄⇘o⇙ ≠ []) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil))) ∧
τtrsys.τRuns_table2 redT mτmove σ E'') ∨
ltl ?lhs' = ltl ?rhs'"
using lhs' E'' fin tls' tlsstlss' filter eq' neq_empty
by(auto simp add: lmap_lappend_distrib lappend_assoc split_beta filter_empty_conv simp del: split_paired_Ex)
qed
ultimately show ?case ..
qed
also have "lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) … = lfilter (λobs. ¬ lnull obs) (lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (?tail E'') LNil))))"
unfolding lfilter_lmap by(simp add: o_def split_def llist_of_eq_LNil_conv)
finally have "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?E''')"
by(simp add: lconcat_lfilter_neq_LNil) }
ultimately show "E ∈ ?lhs" by(blast intro: ℰ.intros)
next
fix E
assume "E ∈ ?lhs"
then obtain E' where E: "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) E')"
and Runs: "mthr.Runs σ E'" by(blast elim: ℰ.cases)
from Runs obtain E'' where E': "E' = lmap (λ(s, tl, s'). tl) E''"
and Runs': "mthr.Runs_table σ E''" by(rule mthr.Runs_into_Runs_table)
have "mthr.τRuns σ (tmap (λ(s, tl, s'). tl) id (tfilter None (λ(s, tl, s'). ¬ mτmove s tl s') (tllist_of_llist (Some (llast (LCons σ (lmap (λ(s, tl, s'). s') E'')))) E'')))"
(is "mthr.τRuns _ ?E'''")
using Runs' by(rule mthr.Runs_table_into_τRuns)
moreover
have "(λ(s, (t, ta), s'). obs_a ta ≠ []) = (λ(s, (t, ta), s'). obs_a ta ≠ [] ∧ ¬ mτmove s (t, ta) s')"
by(rule ext)(auto dest: mτmove_silentD)
hence "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) (llist_of_tllist ?E'''))"
unfolding E E'
by(subst (1 2) lconcat_lfilter_neq_LNil[symmetric])(simp add: lfilter_lmap lfilter_lfilter o_def split_def)
ultimately show "E ∈ ?rhs" by(blast)
qed
end
text ‹Running threads have been started before›
definition Status_no_wait_locks :: "('l,'t,status × 'x) thread_info ⇒ bool"
where
"Status_no_wait_locks ts ⟷
(∀t status x ln. ts t = ⌊((status, x), ln)⌋ ⟶ status ≠ Running ⟶ ln = no_wait_locks)"
lemma Status_no_wait_locks_PreStartD:
"⋀ln. ⟦ Status_no_wait_locks ts; ts t = ⌊((PreStart, x), ln)⌋ ⟧ ⟹ ln = no_wait_locks"
unfolding Status_no_wait_locks_def by blast
lemma Status_no_wait_locks_FinishedD:
"⋀ln. ⟦ Status_no_wait_locks ts; ts t = ⌊((Finished, x), ln)⌋ ⟧ ⟹ ln = no_wait_locks"
unfolding Status_no_wait_locks_def by blast
lemma Status_no_wait_locksI:
"(⋀t status x ln. ⟦ ts t = ⌊((status, x), ln)⌋; status = PreStart ∨ status = Finished ⟧ ⟹ ln = no_wait_locks)
⟹ Status_no_wait_locks ts"
unfolding Status_no_wait_locks_def
apply clarify
apply(case_tac status)
apply auto
done
context heap_base begin
lemma Status_no_wait_locks_start_state:
"Status_no_wait_locks (thr (init_fin_lift_state status (start_state f P C M vs)))"
by(clarsimp simp add: Status_no_wait_locks_def init_fin_lift_state_def start_state_def split_beta)
end
context multithreaded_base begin
lemma init_fin_preserve_Status_no_wait_locks:
assumes ok: "Status_no_wait_locks (thr s)"
and redT: "multithreaded_base.redT init_fin_final init_fin (map NormalAction ∘ convert_RA) s tta s'"
shows "Status_no_wait_locks (thr s')"
using redT
proof(cases rule: multithreaded_base.redT.cases[consumes 1, case_names redT_normal redT_acquire])
case redT_acquire
with ok show ?thesis
by(auto intro!: Status_no_wait_locksI dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD split: if_split_asm)
next
case redT_normal
show ?thesis
proof(rule Status_no_wait_locksI)
fix t' status' x' ln'
assume tst': "thr s' t' = ⌊((status', x'), ln')⌋"
and status: "status' = PreStart ∨ status' = Finished"
show "ln' = no_wait_locks"
proof(cases "thr s t'")
case None
with redT_normal tst' show ?thesis
by(fastforce elim!: init_fin.cases dest: redT_updTs_new_thread simp add: final_thread.actions_ok_iff split: if_split_asm)
next
case (Some sxln)
obtain status'' x'' ln''
where [simp]: "sxln = ((status'', x''), ln'')" by(cases sxln) auto
show ?thesis
proof(cases "fst tta = t'")
case True
with redT_normal tst' status show ?thesis by(auto simp add: expand_finfun_eq fun_eq_iff)
next
case False
with tst' redT_normal Some status have "status'' = status'" "ln'' = ln'"
by(force dest: redT_updTs_Some simp add: final_thread.actions_ok_iff)+
with ok Some status show ?thesis
by(auto dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD)
qed
qed
qed
qed
lemma init_fin_Running_InitialThreadAction:
assumes redT: "multithreaded_base.redT init_fin_final init_fin (map NormalAction ∘ convert_RA) s tta s'"
and not_running: "⋀x ln. thr s t ≠ ⌊((Running, x), ln)⌋"
and running: "thr s' t = ⌊((Running, x'), ln')⌋"
shows "tta = (t, ⦃InitialThreadAction⦄)"
using redT
proof(cases rule: multithreaded_base.redT.cases[consumes 1, case_names redT_normal redT_acquire])
case redT_acquire
with running not_running show ?thesis by(auto split: if_split_asm)
next
case redT_normal
show ?thesis
proof(cases "thr s t")
case None
with redT_normal running not_running show ?thesis
by(fastforce simp add: final_thread.actions_ok_iff elim: init_fin.cases dest: redT_updTs_new_thread split: if_split_asm)
next
case (Some a)
with redT_normal running not_running show ?thesis
apply(cases a)
apply(auto simp add: final_thread.actions_ok_iff split: if_split_asm elim: init_fin.cases)
apply((drule (1) redT_updTs_Some)?, fastforce)+
done
qed
qed
end
context if_multithreaded begin
lemma init_fin_Trsys_preserve_Status_no_wait_locks:
assumes ok: "Status_no_wait_locks (thr s)"
and Trsys: "if.mthr.Trsys s ttas s'"
shows "Status_no_wait_locks (thr s')"
using Trsys ok
by(induct)(blast dest: init_fin_preserve_Status_no_wait_locks)+
lemma init_fin_Trsys_Running_InitialThreadAction:
assumes redT: "if.mthr.Trsys s ttas s'"
and not_running: "⋀x ln. thr s t ≠ ⌊((Running, x), ln)⌋"
and running: "thr s' t = ⌊((Running, x'), ln')⌋"
shows "(t, ⦃InitialThreadAction⦄) ∈ set ttas"
using redT not_running running
proof(induct arbitrary: x' ln')
case rtrancl3p_refl thus ?case by(fastforce)
next
case (rtrancl3p_step s ttas s' tta s'') thus ?case
by(cases "∃x ln. thr s' t = ⌊((Running, x), ln)⌋")(fastforce dest: init_fin_Running_InitialThreadAction)+
qed
end
locale heap_multithreaded_base =
heap_base
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
+
mthr: multithreaded_base final r convert_RA
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and final :: "'x ⇒ bool"
and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
and convert_RA :: "'addr released_locks ⇒ ('addr, 'thread_id) obs_event list"
sublocale heap_multithreaded_base < mthr: if_multithreaded_base final r convert_RA
.
context heap_multithreaded_base begin
abbreviation ℰ_start ::
"(cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'md ⇒ 'addr val list ⇒ 'x)
⇒ 'md prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ status
⇒ ('thread_id × ('addr, 'thread_id) obs_event action) llist set"
where
"ℰ_start f P C M vs status ≡
lappend (llist_of (lift_start_obs start_tid start_heap_obs)) `
mthr.if.ℰ (init_fin_lift_state status (start_state f P C M vs))"
end
locale heap_multithreaded =
heap_multithreaded_base
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
final r convert_RA
+
heap
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
P
+
mthr: multithreaded final r convert_RA
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and final :: "'x ⇒ bool"
and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
and convert_RA :: "'addr released_locks ⇒ ('addr, 'thread_id) obs_event list"
and P :: "'md prog"
sublocale heap_multithreaded < mthr: if_multithreaded final r convert_RA
by(unfold_locales)
sublocale heap_multithreaded < "if": jmm_multithreaded
mthr.init_fin_final mthr.init_fin "map NormalAction ∘ convert_RA" P
.
context heap_multithreaded begin
lemma thread_start_actions_ok_init_fin_RedT:
assumes Red: "mthr.if.RedT (init_fin_lift_state status (start_state f P C M vs)) ttas s'"
(is "mthr.if.RedT ?start_state _ _")
shows "thread_start_actions_ok (llist_of (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas)))"
(is "thread_start_actions_ok (llist_of (?obs_prefix @ ?E'))")
proof(rule thread_start_actions_okI)
let ?E = "llist_of (?obs_prefix @ ?E')"
fix a
assume a: "a ∈ actions ?E"
and new: "¬ is_new_action (action_obs ?E a)"
show "∃i ≤ a. action_obs ?E i = InitialThreadAction ∧ action_tid ?E i = action_tid ?E a"
proof(cases "action_tid ?E a = start_tid")
case True thus ?thesis
by(auto simp add: lift_start_obs_def action_tid_def action_obs_def)
next
case False
let ?a = "a - length ?obs_prefix"
from False have a_len: "a ≥ length ?obs_prefix"
by(rule contrapos_np)(auto simp add: lift_start_obs_def action_tid_def lnth_LCons nth_append split: nat.split)
hence [simp]: "action_tid ?E a = action_tid (llist_of ?E') ?a" "action_obs ?E a = action_obs (llist_of ?E') ?a"
by(simp_all add: action_tid_def nth_append action_obs_def)
from False have not_running: "⋀x ln. thr ?start_state (action_tid (llist_of ?E') ?a) ≠ ⌊((Running, x), ln)⌋"
by(auto simp add: start_state_def split_beta init_fin_lift_state_def split: if_split_asm)
from a a_len have "?a < length ?E'" by(simp add: actions_def)
from nth_concat_conv[OF this]
obtain m n where E'_a: "?E' ! ?a = (λ(t, ta). (t, ⦃ta⦄⇘o⇙ ! n)) (ttas ! m)"
and n: "n < length ⦃snd (ttas ! m)⦄⇘o⇙"
and m: "m < length ttas"
and a_conv: "?a = (∑i<m. length (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas ! i)) + n"
by(clarsimp simp add: split_def)
from Red obtain s'' s''' where Red1: "mthr.if.RedT ?start_state (take m ttas) s''"
and red: "mthr.if.redT s'' (ttas ! m) s'''"
and Red2: "mthr.if.RedT s''' (drop (Suc m) ttas) s'"
unfolding mthr.if.RedT_def
by(subst (asm) (4) id_take_nth_drop[OF m])(blast elim: rtrancl3p_appendE rtrancl3p_converseE)
from E'_a m n have [simp]: "action_tid (llist_of ?E') ?a = fst (ttas ! m)"
by(simp add: action_tid_def split_def)
from red obtain status x ln where tst: "thr s'' (fst (ttas ! m)) = ⌊((status, x), ln)⌋" by cases auto
show ?thesis
proof(cases "status = PreStart ∨ status = Finished")
case True
from Red1 have "Status_no_wait_locks (thr s'')"
unfolding mthr.if.RedT_def
by(rule mthr.init_fin_Trsys_preserve_Status_no_wait_locks[OF Status_no_wait_locks_start_state])
with True tst have "ln = no_wait_locks"
by(auto dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD)
with red tst True have "⦃snd (ttas ! m)⦄⇘o⇙ = [InitialThreadAction]" by(cases) auto
hence "action_obs ?E a = InitialThreadAction" using a_conv n a_len E'_a
by(simp add: action_obs_def nth_append split_beta)
thus ?thesis by(auto)
next
case False
hence "status = Running" by(cases status) auto
with tst mthr.init_fin_Trsys_Running_InitialThreadAction[OF Red1[unfolded mthr.if.RedT_def] not_running]
have "(fst (ttas ! m), ⦃InitialThreadAction⦄) ∈ set (take m ttas)"
using E'_a by(auto simp add: action_tid_def split_beta)
then obtain i where i: "i < m"
and nth_i: "ttas ! i = (fst (ttas ! m), ⦃InitialThreadAction⦄)"
unfolding in_set_conv_nth by auto
let ?i' = "length (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (take i ttas)))"
let ?i = "length ?obs_prefix + ?i'"
from i m nth_i
have "?i' < length (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (take m ttas)))"
apply(simp add: length_concat o_def split_beta)
apply(subst (6) id_take_nth_drop[where i=i])
apply(simp_all add: take_map[symmetric] min_def)
done
also from m have "… ≤ ?a" unfolding a_conv
by(simp add: length_concat sum_list_sum_nth min_def split_def atLeast0LessThan)
finally have "?i < a" using a_len by simp
moreover
from i m nth_i have "?i' < length ?E'"
apply(simp add: length_concat o_def split_def)
apply(subst (7) id_take_nth_drop[where i=i])
apply(simp_all add: take_map[symmetric])
done
from nth_i i E'_a a_conv m
have "lnth ?E ?i = (fst (ttas ! m), InitialThreadAction)"
by(simp add: lift_start_obs_def nth_append length_concat o_def split_def)(rule nth_concat_eqI[where k=0 and i=i], simp_all add: take_map o_def split_def)
ultimately show ?thesis using E'_a
by(cases "ttas ! m")(auto simp add: action_obs_def action_tid_def nth_append intro!: exI[where x="?i"])
qed
qed
qed
lemma thread_start_actions_ok_init_fin:
assumes E: "E ∈ mthr.if.ℰ (init_fin_lift_state status (start_state f P C M vs))"
shows "thread_start_actions_ok (lappend (llist_of (lift_start_obs start_tid start_heap_obs)) E)"
(is "thread_start_actions_ok ?E")
proof(rule thread_start_actions_okI)
let ?start_heap_obs = "lift_start_obs start_tid start_heap_obs"
let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"
fix a
assume a: "a ∈ actions ?E"
and a_new: "¬ is_new_action (action_obs ?E a)"
show "∃i. i ≤ a ∧ action_obs ?E i = InitialThreadAction ∧ action_tid ?E i = action_tid ?E a"
proof(cases "action_tid ?E a = start_tid")
case True thus ?thesis
by(auto simp add: lift_start_obs_def action_tid_def action_obs_def)
next
case False
let ?a = "a - length ?start_heap_obs"
from False have "a ≥ length ?start_heap_obs"
by(rule contrapos_np)(auto simp add: lift_start_obs_def action_tid_def lnth_LCons lnth_lappend1 split: nat.split)
hence [simp]: "action_tid ?E a = action_tid E ?a" "action_obs ?E a = action_obs E ?a"
by(simp_all add: action_tid_def lnth_lappend2 action_obs_def)
from False have not_running: "⋀x ln. thr ?start_state (action_tid E ?a) ≠ ⌊((Running, x), ln)⌋"
by(auto simp add: start_state_def split_beta init_fin_lift_state_def split: if_split_asm)
from E obtain E' where E': "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
and τRuns: "mthr.if.mthr.Runs ?start_state E'" by(rule mthr.if.ℰ.cases)
from a E' ‹a ≥ length ?start_heap_obs›
have enat_a: "enat ?a < llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E'))"
by(cases "llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E'))")(auto simp add: actions_def)
with τRuns obtain m n t ta
where a_obs: "lnth (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')) (a - length ?start_heap_obs) = (t, ⦃ta⦄⇘o⇙ ! n)"
and n: "n < length ⦃ta⦄⇘o⇙"
and m: "enat m < llength E'"
and a_conv: "?a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n"
and E'_m: "lnth E' m = (t, ta)"
by(rule mthr.if.actions_ℰE_aux)
from a_obs have [simp]: "action_tid E ?a = t" "action_obs E ?a = ⦃ta⦄⇘o⇙ ! n"
by(simp_all add: E' action_tid_def action_obs_def)
let ?E' = "ldropn (Suc m) E'"
let ?m_E' = "ltake (enat m) E'"
have E'_unfold: "E' = lappend (ltake (enat m) E') (LCons (lnth E' m) ?E')"
unfolding ldropn_Suc_conv_ldropn[OF m] by simp
hence "mthr.if.mthr.Runs ?start_state (lappend ?m_E' (LCons (lnth E' m) ?E'))"
using τRuns by simp
then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of ?m_E') σ'"
and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' m) ?E')"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns' obtain σ''' where red_a: "mthr.if.redT σ' (t, ta) σ'''"
and τRuns'': "mthr.if.mthr.Runs σ''' ?E'"
unfolding E'_m by cases
from red_a obtain status x ln where tst: "thr σ' t = ⌊((status, x), ln)⌋" by cases auto
show ?thesis
proof(cases "status = PreStart ∨ status = Finished")
case True
have "Status_no_wait_locks (thr σ')"
by(rule mthr.init_fin_Trsys_preserve_Status_no_wait_locks[OF _ σ_σ'])(rule Status_no_wait_locks_start_state)
with True tst have "ln = no_wait_locks"
by(auto dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD)
with red_a tst True have "⦃ta⦄⇘o⇙ = [InitialThreadAction]" by(cases) auto
hence "action_obs E ?a = InitialThreadAction" using a_obs n unfolding E'
by(simp add: action_obs_def)
thus ?thesis by(auto)
next
case False
hence "status = Running" by(cases status) auto
with tst mthr.init_fin_Trsys_Running_InitialThreadAction[OF σ_σ' not_running]
have "(action_tid E ?a, ⦃InitialThreadAction⦄) ∈ set (list_of (ltake (enat m) E'))"
using a_obs E' by(auto simp add: action_tid_def)
then obtain i where "i < m" "enat i < llength E'"
and nth_i: "lnth E' i = (action_tid E ?a, ⦃InitialThreadAction⦄)"
unfolding in_set_conv_nth
by(cases "llength E'")(auto simp add: length_list_of_conv_the_enat lnth_ltake)
let ?i' = "∑i<i. length ⦃snd (lnth E' i)⦄⇘o⇙"
let ?i = "length ?start_heap_obs + ?i'"
from ‹i < m› have "(∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) = ?i' + (∑i=i..<m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
hence "?i' ≤ ?a" unfolding a_conv by simp
hence "?i ≤ a" using ‹a ≥ length ?start_heap_obs› by arith
from ‹?i' ≤ ?a› have "enat ?i' < llength E" using enat_a E'
by(simp add: le_less_trans[where y="enat ?a"])
from lnth_lconcat_conv[OF this[unfolded E'], folded E']
obtain k l
where nth_i': "lnth E ?i' = lnth (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') k) l"
and l: "l < length ⦃snd (lnth E' k)⦄⇘o⇙"
and k: "enat k < llength E'"
and i_conv: "enat ?i' = (∑i<k. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) + enat l"
by(fastforce simp add: split_beta)
have "(∑i<k. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) =
(∑i<k. (enat ∘ (λi. length ⦃snd (lnth E' i)⦄⇘o⇙)) i)"
by(rule sum.cong)(simp_all add: less_trans[where y="enat k"] split_beta k)
also have "… = enat (∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙)"
by(rule sum_comp_morphism)(simp_all add: zero_enat_def)
finally have i_conv: "?i' = (∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙) + l" using i_conv by simp
have [simp]: "i = k"
proof(rule ccontr)
assume "i ≠ k"
thus False unfolding neq_iff
proof
assume "i < k"
hence "(∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙) =
(∑i<i. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i=i..<k. length ⦃snd (lnth E' i)⦄⇘o⇙)"
unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
with i_conv have "(∑i=i..<k. length ⦃snd (lnth E' i)⦄⇘o⇙) = l" "l = 0" by simp_all
moreover have "(∑i=i..<k. length ⦃snd (lnth E' i)⦄⇘o⇙) ≥ length ⦃snd (lnth E' i)⦄⇘o⇙"
by(subst sum.atLeast_Suc_lessThan[OF ‹i < k›]) simp
ultimately show False using nth_i by simp
next
assume "k < i"
hence "?i' = (∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i=k..<i. length ⦃snd (lnth E' i)⦄⇘o⇙)"
unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
with i_conv have "(∑i=k..<i. length ⦃snd (lnth E' i)⦄⇘o⇙) = l" by simp
moreover have "(∑i=k..<i. length ⦃snd (lnth E' i)⦄⇘o⇙) ≥ length ⦃snd (lnth E' k)⦄⇘o⇙"
by(subst sum.atLeast_Suc_lessThan[OF ‹k < i›]) simp
ultimately show False using l by simp
qed
qed
with l nth_i have [simp]: "l = 0" by simp
hence "lnth E ?i' = (action_tid E ?a, InitialThreadAction)"
using nth_i nth_i' k by simp
with ‹?i ≤ a› show ?thesis
by(auto simp add: action_tid_def action_obs_def lnth_lappend2)
qed
qed
qed
end
text ‹In the subsequent locales, ‹convert_RA› refers to @{term "convert_RA"} and is no longer a parameter!›
lemma convert_RA_not_write:
"⋀ln. ob ∈ set (convert_RA ln) ⟹ ¬ is_write_action (NormalAction ob)"
by(auto simp add: convert_RA_def)
lemma ta_seq_consist_convert_RA:
fixes ln shows
"ta_seq_consist P vs (llist_of ((map NormalAction ∘ convert_RA) ln))"
proof(rule ta_seq_consist_nthI)
fix i ad al v
assume "enat i < llength (llist_of ((map NormalAction ∘ convert_RA) ln :: ('b, 'c) obs_event action list))"
and "lnth (llist_of ((map NormalAction ∘ convert_RA) ln :: ('b, 'c) obs_event action list)) i = NormalAction (ReadMem ad al v)"
hence "ReadMem ad al v ∈ set (convert_RA ln :: ('b, 'c) obs_event list)"
by(auto simp add: in_set_conv_nth)
hence False by(auto simp add: convert_RA_def)
thus "∃b. mrw_values P vs (list_of (ltake (enat i) (llist_of ((map NormalAction ∘ convert_RA) ln)))) (ad, al) = ⌊(v, b)⌋" ..
qed
lemma ta_hb_consistent_convert_RA:
"⋀ln. ta_hb_consistent P E (llist_of (map (Pair t) ((map NormalAction ∘ convert_RA) ln)))"
by(rule ta_hb_consistent_not_ReadI)(auto simp add: convert_RA_def)
locale allocated_multithreaded =
allocated_heap
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated
P
+
mthr: multithreaded final r convert_RA
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
and final :: "'x ⇒ bool"
and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
and P :: "'md prog"
+
assumes red_allocated_mono: "t ⊢ (x, m) -ta→ (x', m') ⟹ allocated m ⊆ allocated m'"
and red_New_allocatedD:
"⟦ t ⊢ (x, m) -ta→ (x', m'); NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ad ∈ allocated m' ∧ ad ∉ allocated m"
and red_allocated_NewD:
"⟦ t ⊢ (x, m) -ta→ (x', m'); ad ∈ allocated m'; ad ∉ allocated m ⟧
⟹ ∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
and red_New_same_addr_same:
"⟦ t ⊢ (x, m) -ta→ (x', m');
⦃ta⦄⇘o⇙ ! i = NewHeapElem a CTn; i < length ⦃ta⦄⇘o⇙;
⦃ta⦄⇘o⇙ ! j = NewHeapElem a CTn'; j < length ⦃ta⦄⇘o⇙ ⟧
⟹ i = j"
sublocale allocated_multithreaded < heap_multithreaded
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
final r convert_RA P
by(unfold_locales)
context allocated_multithreaded begin
lemma redT_allocated_mono:
assumes "mthr.redT σ (t, ta) σ'"
shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms
by cases(auto dest: red_allocated_mono del: subsetI)
lemma RedT_allocated_mono:
assumes "mthr.RedT σ ttas σ'"
shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms unfolding mthr.RedT_def
by induct(auto dest!: redT_allocated_mono intro: subset_trans del: subsetI)
lemma init_fin_allocated_mono:
"t ⊢ (x, m) -ta→i (x', m') ⟹ allocated m ⊆ allocated m'"
by(cases rule: mthr.init_fin.cases)(auto dest: red_allocated_mono)
lemma init_fin_redT_allocated_mono:
assumes "mthr.if.redT σ (t, ta) σ'"
shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms
by cases(auto dest: init_fin_allocated_mono del: subsetI)
lemma init_fin_RedT_allocated_mono:
assumes "mthr.if.RedT σ ttas σ'"
shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms unfolding mthr.if.RedT_def
by induct(auto dest!: init_fin_redT_allocated_mono intro: subset_trans del: subsetI)
lemma init_fin_red_New_allocatedD:
assumes "t ⊢ (x, m) -ta→i (x', m')" "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
shows "ad ∈ allocated m' ∧ ad ∉ allocated m"
using assms
by cases(auto dest: red_New_allocatedD)
lemma init_fin_red_allocated_NewD:
assumes "t ⊢ (x, m) -ta→i (x', m')" "ad ∈ allocated m'" "ad ∉ allocated m"
shows "∃CTn. NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
using assms
by(cases)(auto dest!: red_allocated_NewD)
lemma init_fin_red_New_same_addr_same:
assumes "t ⊢ (x, m) -ta→i (x', m')"
and "⦃ta⦄⇘o⇙ ! i = NormalAction (NewHeapElem a CTn)" "i < length ⦃ta⦄⇘o⇙"
and "⦃ta⦄⇘o⇙ ! j = NormalAction (NewHeapElem a CTn')" "j < length ⦃ta⦄⇘o⇙"
shows "i = j"
using assms
by cases(auto dest: red_New_same_addr_same)
lemma init_fin_redT_allocated_NewHeapElemD:
assumes "mthr.if.redT s (t, ta) s'"
and "ad ∈ allocated (shr s')"
and "ad ∉ allocated (shr s)"
shows "∃CTn. NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
using assms
by(cases)(auto dest: init_fin_red_allocated_NewD)
lemma init_fin_RedT_allocated_NewHeapElemD:
assumes "mthr.if.RedT s ttas s'"
and "ad ∈ allocated (shr s')"
and "ad ∉ allocated (shr s)"
shows "∃t ta CTn. (t, ta) ∈ set ttas ∧ NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
using assms
proof(induct rule: mthr.if.RedT_induct')
case refl thus ?case by simp
next
case (step ttas s' t ta s'') thus ?case
by(cases "ad ∈ allocated (shr s')")(fastforce simp del: split_paired_Ex dest: init_fin_redT_allocated_NewHeapElemD)+
qed
lemma ℰ_new_actions_for_unique:
assumes E: "E ∈ ℰ_start f P C M vs status"
and a: "a ∈ new_actions_for P E adal"
and a': "a' ∈ new_actions_for P E adal"
shows "a = a'"
using a a'
proof(induct a a' rule: wlog_linorder_le)
case symmetry thus ?case by simp
next
case (le a a')
note a = ‹a ∈ new_actions_for P E adal›
and a' = ‹a' ∈ new_actions_for P E adal›
and a_a' = ‹a ≤ a'›
obtain ad al where adal: "adal = (ad, al)" by(cases adal)
let ?init_obs = "lift_start_obs start_tid start_heap_obs"
let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"
have distinct: "distinct (filter (λobs. ∃a CTn. obs = NormalAction (NewHeapElem a CTn)) (map snd ?init_obs))"
unfolding start_heap_obs_def
by(fastforce intro: inj_onI intro!: distinct_filter simp add: distinct_map distinct_zipI1 distinct_initialization_list)
from start_addrs_allocated
have dom_start_state: "{a. ∃CTn. NormalAction (NewHeapElem a CTn) ∈ snd ` set ?init_obs} ⊆ allocated (shr ?start_state)"
by(fastforce simp add: init_fin_lift_state_conv_simps shr_start_state dest: NewHeapElem_start_heap_obs_start_addrsD subsetD)
show ?case
proof(cases "a' < length ?init_obs")
case True
with a' adal E obtain t_a' CTn_a'
where CTn_a': "?init_obs ! a' = (t_a', NormalAction (NewHeapElem ad CTn_a'))"
by(cases "?init_obs ! a'")(fastforce elim!: is_new_action.cases action_loc_aux_cases simp add: action_obs_def lnth_lappend1 new_actions_for_def )+
from True a_a' have len_a: "a < length ?init_obs" by simp
with a adal E obtain t_a CTn_a
where CTn_a: "?init_obs ! a = (t_a, NormalAction (NewHeapElem ad CTn_a))"
by(cases "?init_obs ! a")(fastforce elim!: is_new_action.cases action_loc_aux_cases simp add: action_obs_def lnth_lappend1 new_actions_for_def )+
from CTn_a CTn_a' True len_a
have "NormalAction (NewHeapElem ad CTn_a') ∈ snd ` set ?init_obs"
and "NormalAction (NewHeapElem ad CTn_a) ∈ snd ` set ?init_obs" unfolding set_conv_nth
by(fastforce intro: rev_image_eqI)+
hence [simp]: "CTn_a' = CTn_a" using distinct_start_addrs'
by(auto simp add: in_set_conv_nth distinct_conv_nth start_heap_obs_def start_addrs_def) blast
from distinct_filterD[OF distinct, of a' a "NormalAction (NewHeapElem ad CTn_a)"] len_a True CTn_a CTn_a'
show "a = a'" by simp
next
case False
obtain n where n: "length ?init_obs = n" by blast
with False have "n ≤ a'" by simp
from E obtain E'' where E: "E = lappend (llist_of ?init_obs) E''"
and E'': "E'' ∈ mthr.if.ℰ ?start_state" by auto
from E'' obtain E' where E': "E'' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
and τRuns: "mthr.if.mthr.Runs ?start_state E'" by(rule mthr.if.ℰ.cases)
from E E'' a' n ‹n ≤ a'› adal have a': "a' - n ∈ new_actions_for P E'' adal"
by(auto simp add: new_actions_for_def lnth_lappend2 action_obs_def actions_lappend elim: actionsE)
from a' have "a' - n ∈ actions E''" by(auto elim: new_actionsE)
hence "enat (a' - n) < llength E''" by(rule actionsE)
with τRuns obtain a'_m a'_n t_a' ta_a'
where E_a': "lnth E'' (a' - n) = (t_a', ⦃ta_a'⦄⇘o⇙ ! a'_n)"
and a'_n: "a'_n < length ⦃ta_a'⦄⇘o⇙" and a'_m: "enat a'_m < llength E'"
and a'_conv: "a' - n = (∑i<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + a'_n"
and E'_a'_m: "lnth E' a'_m = (t_a', ta_a')"
unfolding E' by(rule mthr.if.actions_ℰE_aux)
from a' have "is_new_action (action_obs E'' (a' - n))"
and "(ad, al) ∈ action_loc P E'' (a' - n)"
unfolding adal by(auto elim: new_actionsE)
then obtain CTn'
where "action_obs E'' (a' - n) = NormalAction (NewHeapElem ad CTn')"
by cases(fastforce)+
hence New_ta_a': "⦃ta_a'⦄⇘o⇙ ! a'_n = NormalAction (NewHeapElem ad CTn')"
using E_a' a'_n unfolding action_obs_def by simp
show ?thesis
proof(cases "a < n")
case True
with a adal E n obtain t_a CTn_a where "?init_obs ! a = (t_a, NormalAction (NewHeapElem ad CTn_a))"
by(cases "?init_obs ! a")(fastforce elim!: is_new_action.cases simp add: action_obs_def lnth_lappend1 new_actions_for_def)+
with subsetD[OF dom_start_state, of ad] n True
have a_shr_σ: "ad ∈ allocated (shr ?start_state)"
by(fastforce simp add: set_conv_nth intro: rev_image_eqI)
have E'_unfold': "E' = lappend (ltake (enat a'_m) E') (LCons (lnth E' a'_m) (ldropn (Suc a'_m) E'))"
unfolding ldropn_Suc_conv_ldropn[OF a'_m] by simp
hence "mthr.if.mthr.Runs ?start_state (lappend (ltake (enat a'_m) E') (LCons (lnth E' a'_m) (ldropn (Suc a'_m) E')))"
using τRuns by simp
then obtain σ'
where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of (ltake (enat a'_m) E')) σ'"
and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' a'_m) (ldropn (Suc a'_m) E'))"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns' obtain σ''
where red_a': "mthr.if.redT σ' (t_a', ta_a') σ''"
and τRuns'': "mthr.if.mthr.Runs σ'' (ldropn (Suc a'_m) E')"
unfolding E'_a'_m by cases
from New_ta_a' a'_n have "NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙"
unfolding in_set_conv_nth by blast
with red_a' obtain x_a' x'_a' m'_a'
where red'_a': "mthr.init_fin t_a' (x_a', shr σ') ta_a' (x'_a', m'_a')"
and σ''': "redT_upd σ' t_a' ta_a' x'_a' m'_a' σ''"
and ts_t_a': "thr σ' t_a' = ⌊(x_a', no_wait_locks)⌋"
by cases auto
from red'_a' ‹NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙›
obtain ta'_a' X_a' X'_a'
where x_a': "x_a' = (Running, X_a')"
and x'_a': "x'_a' = (Running, X'_a')"
and ta_a': "ta_a' = convert_TA_initial (convert_obs_initial ta'_a')"
and red''_a': "t_a' ⊢ ⟨X_a', shr σ'⟩ -ta'_a'→ ⟨X'_a', m'_a'⟩"
by cases fastforce+
from ta_a' New_ta_a' a'_n have New_ta'_a': "⦃ta'_a'⦄⇘o⇙ ! a'_n = NewHeapElem ad CTn'"
and a'_n': "a'_n < length ⦃ta'_a'⦄⇘o⇙" by auto
hence "NewHeapElem ad CTn' ∈ set ⦃ta'_a'⦄⇘o⇙" unfolding in_set_conv_nth by blast
with red''_a' have allocated_ad': "ad ∉ allocated (shr σ')"
by(auto dest: red_New_allocatedD)
have "allocated (shr ?start_state) ⊆ allocated (shr σ')"
using σ_σ' unfolding mthr.if.RedT_def[symmetric] by(rule init_fin_RedT_allocated_mono)
hence False using allocated_ad' a_shr_σ by blast
thus ?thesis ..
next
case False
hence "n ≤ a" by simp
from E E'' a n ‹n ≤ a› adal have a: "a - n ∈ new_actions_for P E'' adal"
by(auto simp add: new_actions_for_def lnth_lappend2 action_obs_def actions_lappend elim: actionsE)
from a have "a - n ∈ actions E''" by(auto elim: new_actionsE)
hence "enat (a - n) < llength E''" by(rule actionsE)
with τRuns obtain a_m a_n t_a ta_a
where E_a: "lnth E'' (a - n) = (t_a, ⦃ta_a⦄⇘o⇙ ! a_n)"
and a_n: "a_n < length ⦃ta_a⦄⇘o⇙" and a_m: "enat a_m < llength E'"
and a_conv: "a - n = (∑i<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + a_n"
and E'_a_m: "lnth E' a_m = (t_a, ta_a)"
unfolding E' by(rule mthr.if.actions_ℰE_aux)
from a have "is_new_action (action_obs E'' (a - n))"
and "(ad, al) ∈ action_loc P E'' (a - n)"
unfolding adal by(auto elim: new_actionsE)
then obtain CTn where "action_obs E'' (a - n) = NormalAction (NewHeapElem ad CTn)"
by cases(fastforce)+
hence New_ta_a: " ⦃ta_a⦄⇘o⇙ ! a_n = NormalAction (NewHeapElem ad CTn)"
using E_a a_n unfolding action_obs_def by simp
let ?E' = "ldropn (Suc a_m) E'"
have E'_unfold: "E' = lappend (ltake (enat a_m) E') (LCons (lnth E' a_m) ?E')"
unfolding ldropn_Suc_conv_ldropn[OF a_m] by simp
hence "mthr.if.mthr.Runs ?start_state (lappend (ltake (enat a_m) E') (LCons (lnth E' a_m) ?E'))"
using τRuns by simp
then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of (ltake (enat a_m) E')) σ'"
and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' a_m) ?E')"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns' obtain σ''
where red_a: "mthr.if.redT σ' (t_a, ta_a) σ''"
and τRuns'': "mthr.if.mthr.Runs σ'' ?E'"
unfolding E'_a_m by cases
from New_ta_a a_n have "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta_a⦄⇘o⇙"
unfolding in_set_conv_nth by blast
with red_a obtain x_a x'_a m'_a
where red'_a: "mthr.init_fin t_a (x_a, shr σ') ta_a (x'_a, m'_a)"
and σ''': "redT_upd σ' t_a ta_a x'_a m'_a σ''"
and ts_t_a: "thr σ' t_a = ⌊(x_a, no_wait_locks)⌋"
by cases auto
from red'_a ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta_a⦄⇘o⇙›
obtain ta'_a X_a X'_a
where x_a: "x_a = (Running, X_a)"
and x'_a: "x'_a = (Running, X'_a)"
and ta_a: "ta_a = convert_TA_initial (convert_obs_initial ta'_a)"
and red''_a: "t_a ⊢ (X_a, shr σ') -ta'_a→ (X'_a, m'_a)"
by cases fastforce+
from ta_a New_ta_a a_n have New_ta'_a: "⦃ta'_a⦄⇘o⇙ ! a_n = NewHeapElem ad CTn"
and a_n': "a_n < length ⦃ta'_a⦄⇘o⇙" by auto
hence "NewHeapElem ad CTn ∈ set ⦃ta'_a⦄⇘o⇙" unfolding in_set_conv_nth by blast
with red''_a have allocated_m'_a_ad: "ad ∈ allocated m'_a"
by(auto dest: red_New_allocatedD)
have "a_m ≤ a'_m"
proof(rule ccontr)
assume "¬ ?thesis"
hence "a'_m < a_m" by simp
hence "(∑i<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = (∑i<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i = a'_m..<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
by(simp add: sum_upto_add_nat)
hence "a' - n < a - n" using ‹a'_m < a_m› a'_n E'_a'_m unfolding a_conv a'_conv
by(subst (asm) sum.atLeast_Suc_lessThan) simp_all
with a_a' show False by simp
qed
have a'_less: "a' - n < (a - n) - a_n + length ⦃ta_a⦄⇘o⇙"
proof(rule ccontr)
assume "¬ ?thesis"
hence a'_greater: "(a - n) - a_n + length ⦃ta_a⦄⇘o⇙ ≤ a' - n" by simp
have "a_m < a'_m"
proof(rule ccontr)
assume "¬ ?thesis"
with ‹a_m ≤ a'_m› have "a_m = a'_m" by simp
with a'_greater a_n a'_n E'_a'_m E'_a_m show False
unfolding a_conv a'_conv by simp
qed
hence a'_m_a_m: "enat (a'_m - Suc a_m) < llength ?E'" using a'_m
by(cases "llength E'") simp_all
from ‹a_m < a'_m› a'_m E'_a'_m
have E'_a'_m': "lnth ?E' (a'_m - Suc a_m) = (t_a', ta_a')" by simp
have E'_unfold': "?E' = lappend (ltake (enat (a'_m - Suc a_m)) ?E') (LCons (lnth ?E' (a'_m - Suc a_m)) (ldropn (Suc (a'_m - Suc a_m)) ?E'))"
unfolding ldropn_Suc_conv_ldropn[OF a'_m_a_m] lappend_ltake_enat_ldropn ..
hence "mthr.if.mthr.Runs σ'' (lappend (ltake (enat (a'_m - Suc a_m)) ?E') (LCons (lnth ?E' (a'_m - Suc a_m)) (ldropn (Suc (a'_m - Suc a_m)) ?E')))"
using τRuns'' by simp
then obtain σ'''
where σ''_σ''': "mthr.if.mthr.Trsys σ'' (list_of (ltake (enat (a'_m - Suc a_m)) ?E')) σ'''"
and τRuns''': "mthr.if.mthr.Runs σ''' (LCons (lnth ?E' (a'_m - Suc a_m)) (ldropn (Suc (a'_m - Suc a_m)) ?E'))"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns''' obtain σ''''
where red_a': "mthr.if.redT σ''' (t_a', ta_a') σ''''"
and τRuns'''': "mthr.if.mthr.Runs σ'''' (ldropn (Suc (a'_m - Suc a_m)) ?E')"
unfolding E'_a'_m' by cases
from New_ta_a' a'_n have "NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙"
unfolding in_set_conv_nth by blast
with red_a' obtain x_a' x'_a' m'_a'
where red'_a': "mthr.init_fin t_a' (x_a', shr σ''') ta_a' (x'_a', m'_a')"
and σ'''''': "redT_upd σ''' t_a' ta_a' x'_a' m'_a' σ''''"
and ts_t_a': "thr σ''' t_a' = ⌊(x_a', no_wait_locks)⌋"
by cases auto
from red'_a' ‹NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙›
obtain ta'_a' X_a' X'_a'
where x_a': "x_a' = (Running, X_a')"
and x'_a': "x'_a' = (Running, X'_a')"
and ta_a': "ta_a' = convert_TA_initial (convert_obs_initial ta'_a')"
and red''_a': "t_a' ⊢ (X_a', shr σ''') -ta'_a'→ (X'_a', m'_a')"
by cases fastforce+
from ta_a' New_ta_a' a'_n have New_ta'_a': "⦃ta'_a'⦄⇘o⇙ ! a'_n = NewHeapElem ad CTn'"
and a'_n': "a'_n < length ⦃ta'_a'⦄⇘o⇙" by auto
hence "NewHeapElem ad CTn' ∈ set ⦃ta'_a'⦄⇘o⇙" unfolding in_set_conv_nth by blast
with red''_a' have allocated_ad': "ad ∉ allocated (shr σ''')"
by(auto dest: red_New_allocatedD)
have "allocated m'_a = allocated (shr σ'')" using σ''' by auto
also have "… ⊆ allocated (shr σ''')"
using σ''_σ''' unfolding mthr.if.RedT_def[symmetric] by(rule init_fin_RedT_allocated_mono)
finally have "ad ∈ allocated (shr σ''')" using allocated_m'_a_ad by blast
with allocated_ad' show False by contradiction
qed
from ‹a_m ≤ a'_m› have [simp]: "a_m = a'_m"
proof(rule le_antisym)
show "a'_m ≤ a_m"
proof(rule ccontr)
assume "¬ ?thesis"
hence "a_m < a'_m" by simp
hence "(∑i<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = (∑i<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i = a_m..<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
by(simp add: sum_upto_add_nat)
with a'_less ‹a_m < a'_m› E'_a_m a_n a'_n show False
unfolding a'_conv a_conv by(subst (asm) sum.atLeast_Suc_lessThan) simp_all
qed
qed
with E'_a_m E'_a'_m have [simp]: "t_a' = t_a" "ta_a' = ta_a" by simp_all
from New_ta_a' a'_n ta_a have a'_n': "a'_n < length ⦃ta'_a⦄⇘o⇙"
and New_ta'_a': "⦃ta'_a⦄⇘o⇙ ! a'_n = NewHeapElem ad CTn'" by auto
with red''_a New_ta'_a a_n' have "a'_n = a_n"
by(auto dest: red_New_same_addr_same)
with ‹a_m = a'_m› have "a - n = a' - n" unfolding a_conv a'_conv by simp
thus ?thesis using ‹n ≤ a› ‹n ≤ a'› by simp
qed
qed
qed
end
text ‹Knowledge of addresses of a multithreaded state›
fun ka_Val :: "'addr val ⇒ 'addr set"
where
"ka_Val (Addr a) = {a}"
| "ka_Val _ = {}"
fun new_obs_addr :: "('addr, 'thread_id) obs_event ⇒ 'addr set"
where
"new_obs_addr (ReadMem ad al (Addr ad')) = {ad'}"
| "new_obs_addr (NewHeapElem ad hT) = {ad}"
| "new_obs_addr _ = {}"
lemma new_obs_addr_cases[consumes 1, case_names ReadMem NewHeapElem, cases set]:
assumes "ad ∈ new_obs_addr ob"
obtains ad' al where "ob = ReadMem ad' al (Addr ad)"
| CTn where "ob = NewHeapElem ad CTn"
using assms
by(cases ob rule: new_obs_addr.cases) auto
definition new_obs_addrs :: "('addr, 'thread_id) obs_event list ⇒ 'addr set"
where
"new_obs_addrs obs = ⋃(new_obs_addr ` set obs)"
fun new_obs_addr_if :: "('addr, 'thread_id) obs_event action ⇒ 'addr set"
where
"new_obs_addr_if (NormalAction a) = new_obs_addr a"
| "new_obs_addr_if _ = {}"
definition new_obs_addrs_if :: "('addr, 'thread_id) obs_event action list ⇒ 'addr set"
where
"new_obs_addrs_if obs = ⋃(new_obs_addr_if ` set obs)"
lemma ka_Val_subset_new_obs_Addr_ReadMem:
"ka_Val v ⊆ new_obs_addr (ReadMem ad al v)"
by(cases v) simp_all
lemma typeof_ka: "typeof v ≠ None ⟹ ka_Val v = {}"
by(cases v) simp_all
lemma ka_Val_undefined_value [simp]:
"ka_Val undefined_value = {}"
apply(cases "undefined_value :: 'a val")
apply(bestsimp simp add: undefined_value_not_Addr dest: subst)+
done
locale known_addrs_base =
fixes known_addrs :: "'t ⇒ 'x ⇒ 'addr set"
begin
definition known_addrs_thr :: "('l, 't, 'x) thread_info ⇒ 'addr set"
where "known_addrs_thr ts = (⋃t ∈ dom ts. known_addrs t (fst (the (ts t))))"
definition known_addrs_state :: "('l,'t,'x,'m,'w) state ⇒ 'addr set"
where "known_addrs_state s = known_addrs_thr (thr s)"
lemma known_addrs_state_simps [simp]:
"known_addrs_state (ls, (ts, m), ws) = known_addrs_thr ts"
by(simp add: known_addrs_state_def)
lemma known_addrs_thr_cases[consumes 1, case_names known_addrs, cases set: known_addrs_thr]:
assumes "ad ∈ known_addrs_thr ts"
and "⋀t x ln. ⟦ ts t = ⌊(x, ln)⌋; ad ∈ known_addrs t x ⟧ ⟹ thesis"
shows thesis
using assms
by(auto simp add: known_addrs_thr_def ran_def)
lemma known_addrs_stateI:
"⋀ln. ⟦ ad ∈ known_addrs t x; thr s t = ⌊(x, ln)⌋ ⟧ ⟹ ad ∈ known_addrs_state s"
by(fastforce simp add: known_addrs_state_def known_addrs_thr_def intro: rev_bexI)
fun known_addrs_if :: "'t ⇒ status × 'x ⇒ 'addr set"
where "known_addrs_if t (s, x) = known_addrs t x"
end
locale if_known_addrs_base =
known_addrs_base known_addrs
+
multithreaded_base final r convert_RA
for known_addrs :: "'t ⇒ 'x ⇒ 'addr set"
and final :: "'x ⇒ bool"
and r :: "('addr, 't, 'x, 'heap, 'addr, 'obs) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
and convert_RA :: "'addr released_locks ⇒ 'obs list"
sublocale if_known_addrs_base < "if": known_addrs_base known_addrs_if .
locale known_addrs =
allocated_multithreaded
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated
final r
P
+
if_known_addrs_base known_addrs final r convert_RA
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
and known_addrs :: "'thread_id ⇒ 'x ⇒ 'addr set"
and final :: "'x ⇒ bool"
and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
and P :: "'md prog"
+
assumes red_known_addrs_new:
"t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩
⟹ known_addrs t x' ⊆ known_addrs t x ∪ new_obs_addrs ⦃ta⦄⇘o⇙"
and red_known_addrs_new_thread:
"⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ known_addrs t' x'' ⊆ known_addrs t x"
and red_read_knows_addr:
"⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ad ∈ known_addrs t x"
and red_write_knows_addr:
"⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; ⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr ad'); n < length ⦃ta⦄⇘o⇙ ⟧
⟹ ad' ∈ known_addrs t x ∨ ad' ∈ new_obs_addrs (take n ⦃ta⦄⇘o⇙)"
begin
notation mthr.redT_syntax1 ("_ -_▹_→ _" [50,0,0,50] 80)
lemma if_red_known_addrs_new:
assumes "t ⊢ (x, m) -ta→i (x', m')"
shows "known_addrs_if t x' ⊆ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
using assms
by cases(auto dest!: red_known_addrs_new simp add: new_obs_addrs_if_def new_obs_addrs_def)
lemma if_red_known_addrs_new_thread:
assumes "t ⊢ (x, m) -ta→i (x', m')" "NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
shows "known_addrs_if t' x'' ⊆ known_addrs_if t x"
using assms
by cases(fastforce dest: red_known_addrs_new_thread)+
lemma if_red_read_knows_addr:
assumes "t ⊢ (x, m) -ta→i (x', m')" "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
shows "ad ∈ known_addrs_if t x"
using assms
by cases(fastforce dest: red_read_knows_addr)+
lemma if_red_write_knows_addr:
assumes "t ⊢ (x, m) -ta→i (x', m')"
and "⦃ta⦄⇘o⇙ ! n = NormalAction (WriteMem ad al (Addr ad'))" "n < length ⦃ta⦄⇘o⇙"
shows "ad' ∈ known_addrs_if t x ∨ ad' ∈ new_obs_addrs_if (take n ⦃ta⦄⇘o⇙)"
using assms
by cases(auto dest: red_write_knows_addr simp add: new_obs_addrs_if_def new_obs_addrs_def take_map)
lemma if_redT_known_addrs_new:
assumes redT: "mthr.if.redT s (t, ta) s'"
shows "if.known_addrs_state s' ⊆ if.known_addrs_state s ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
using redT
proof(cases)
case redT_acquire thus ?thesis
by(cases s)(fastforce simp add: if.known_addrs_thr_def split: if_split_asm intro: rev_bexI)
next
case (redT_normal x x' m)
note red = ‹t ⊢ (x, shr s) -ta→i (x', m)›
show ?thesis
proof
fix ad
assume "ad ∈ if.known_addrs_state s'"
hence "ad ∈ if.known_addrs_thr (thr s')" by(simp add: if.known_addrs_state_def)
then obtain t' x'' ln'' where ts't': "thr s' t' = ⌊(x'', ln'')⌋"
and ad: "ad ∈ known_addrs_if t' x''"
by(rule if.known_addrs_thr_cases)
show "ad ∈ if.known_addrs_state s ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
proof(cases "thr s t'")
case None
with redT_normal ‹thr s' t' = ⌊(x'', ln'')⌋›
obtain m'' where "NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
by(fastforce dest: redT_updTs_new_thread split: if_split_asm)
with red have "known_addrs_if t' x'' ⊆ known_addrs_if t x" by(rule if_red_known_addrs_new_thread)
also have "… ⊆ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙" by simp
finally have "ad ∈ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙" using ad by blast
thus ?thesis using ‹thr s t = ⌊(x, no_wait_locks)⌋› by(blast intro: if.known_addrs_stateI)
next
case (Some xln)
show ?thesis
proof(cases "t = t'")
case True
with redT_normal ts't' if_red_known_addrs_new[OF red] ad
have "ad ∈ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙" by auto
thus ?thesis using ‹thr s t = ⌊(x, no_wait_locks)⌋› by(blast intro: if.known_addrs_stateI)
next
case False
with ts't' redT_normal ad Some show ?thesis
by(fastforce dest: redT_updTs_Some[where ts="thr s" and t=t'] intro: if.known_addrs_stateI)
qed
qed
qed
qed
lemma if_redT_read_knows_addr:
assumes redT: "mthr.if.redT s (t, ta) s'"
and read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
shows "ad ∈ if.known_addrs_state s"
using redT
proof(cases)
case redT_acquire thus ?thesis using read by auto
next
case (redT_normal x x' m')
with if_red_read_knows_addr[OF ‹t ⊢ (x, shr s) -ta→i (x', m')› read]
show ?thesis
by(auto simp add: if.known_addrs_state_def if.known_addrs_thr_def intro: bexI[where x=t])
qed
lemma init_fin_redT_known_addrs_subset:
assumes "mthr.if.redT s (t, ta) s'"
shows "if.known_addrs_state s' ⊆ if.known_addrs_state s ∪ known_addrs_if t (fst (the (thr s' t)))"
using assms
apply(cases)
apply(rule subsetI)
apply(clarsimp simp add: if.known_addrs_thr_def split: if_split_asm)
apply(rename_tac status x status' x' m' a ws' t'' status'' x'' ln'')
apply(case_tac "thr s t''")
apply(drule (2) redT_updTs_new_thread)
apply clarsimp
apply(drule (1) if_red_known_addrs_new_thread)
apply simp
apply(drule (1) subsetD)
apply(rule_tac x="(status, x)" in if.known_addrs_stateI)
apply(simp)
apply simp
apply(frule_tac t="t''" in redT_updTs_Some, assumption)
apply clarsimp
apply(rule_tac x="(status'', x'')" in if.known_addrs_stateI)
apply simp
apply simp
apply(auto simp add: if.known_addrs_state_def if.known_addrs_thr_def split: if_split_asm)
done
lemma w_values_no_write_unchanged:
assumes no_write: "⋀w. ⟦ w ∈ set obs; is_write_action w; adal ∈ action_loc_aux P w ⟧ ⟹ False"
shows "w_values P vs obs adal = vs adal"
using assms
proof(induct obs arbitrary: vs)
case Nil show ?case by simp
next
case (Cons ob obs)
from Cons.prems[of ob]
have "w_value P vs ob adal = vs adal"
by(cases adal)(cases ob rule: w_value_cases, auto simp add: addr_locs_def split: htype.split_asm, blast+)
moreover
have "w_values P (w_value P vs ob) obs adal = w_value P vs ob adal"
proof(rule Cons.hyps)
fix w
assume "w ∈ set obs" "is_write_action w" "adal ∈ action_loc_aux P w"
with Cons.prems[of w] ‹w_value P vs ob adal = vs adal›
show "False" by simp
qed
ultimately show ?case by simp
qed
lemma redT_non_speculative_known_addrs_allocated:
assumes red: "mthr.if.redT s (t, ta) s'"
and tasc: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
and ka: "if.known_addrs_state s ⊆ allocated (shr s)"
and vs: "w_addrs vs ⊆ allocated (shr s)"
shows "if.known_addrs_state s' ⊆ allocated (shr s')" (is "?thesis1")
and "w_addrs (w_values P vs ⦃ta⦄⇘o⇙) ⊆ allocated (shr s')" (is "?thesis2")
proof