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 -
have "?thesis1 ∧ ?thesis2" using red
proof(cases)
case (redT_acquire x ln n)
hence "if.known_addrs_state s' = if.known_addrs_state s"
by(auto 4 4 simp add: if.known_addrs_state_def if.known_addrs_thr_def split: if_split_asm dest: bspec)
also note ka
also from redT_acquire have "shr s = shr s'" by simp
finally have "if.known_addrs_state s' ⊆ allocated (shr s')" .
moreover have "w_values P vs ⦃ta⦄⇘o⇙ = vs" using redT_acquire
by(fastforce intro!: w_values_no_write_unchanged del: equalityI dest: convert_RA_not_write)
ultimately show ?thesis using vs by(simp add: ‹shr s = shr s'›)
next
case (redT_normal x x' m')
note red = ‹t ⊢ (x, shr s) -ta→i (x', m')›
and tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
have allocated_subset: "allocated (shr s) ⊆ allocated (shr s')"
using ‹mthr.if.redT s (t, ta) s'› by(rule init_fin_redT_allocated_mono)
with vs have vs': "w_addrs vs ⊆ allocated (shr s')" by blast
{ fix obs obs'
assume "⦃ta⦄⇘o⇙ = obs @ obs'"
moreover with tasc have "non_speculative P vs (llist_of obs)"
by(simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
ultimately have "w_addrs (w_values P vs obs) ∪ new_obs_addrs_if obs ⊆ allocated (shr s')"
(is "?concl obs")
proof(induct obs arbitrary: obs' rule: rev_induct)
case Nil thus ?case using vs' by(simp add: new_obs_addrs_if_def)
next
case (snoc ob obs)
note ta = ‹⦃ta⦄⇘o⇙ = (obs @ [ob]) @ obs'›
note tasc = ‹non_speculative P vs (llist_of (obs @ [ob]))›
from snoc have IH: "?concl obs"
by(simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
hence "?concl (obs @ [ob])"
proof(cases "ob" rule: mrw_value_cases)
case (1 ad' al v)
note ob = ‹ob = NormalAction (WriteMem ad' al v)›
with ta have Write: "⦃ta⦄⇘o⇙ ! length obs = NormalAction (WriteMem ad' al v)" by simp
show ?thesis
proof
fix ad''
assume "ad'' ∈ w_addrs (w_values P vs (obs @ [ob])) ∪ new_obs_addrs_if (obs @ [ob])"
hence "ad'' ∈ w_addrs (w_values P vs obs) ∪ new_obs_addrs_if obs ∨ v = Addr ad''"
by(auto simp add: ob w_addrs_def ran_def new_obs_addrs_if_def split: if_split_asm)
thus "ad'' ∈ allocated (shr s')"
proof
assume "ad'' ∈ w_addrs (w_values P vs obs) ∪ new_obs_addrs_if obs"
also note IH finally show ?thesis .
next
assume v: "v = Addr ad''"
with Write have "⦃ta⦄⇘o⇙ ! length obs = NormalAction (WriteMem ad' al (Addr ad''))" by simp
with red have "ad'' ∈ known_addrs_if t x ∨ ad'' ∈ new_obs_addrs_if (take (length obs) ⦃ta⦄⇘o⇙)"
by(rule if_red_write_knows_addr)(simp add: ta)
thus ?thesis
proof
assume "ad'' ∈ known_addrs_if t x"
hence "ad'' ∈ if.known_addrs_state s" using tst by(rule if.known_addrs_stateI)
with ka allocated_subset show ?thesis by blast
next
assume "ad'' ∈ new_obs_addrs_if (take (length obs) ⦃ta⦄⇘o⇙)"
with ta have "ad'' ∈ new_obs_addrs_if obs" by simp
with IH show ?thesis by blast
qed
qed
qed
next
case (2 ad hT)
hence ob: "ob = NormalAction (NewHeapElem ad hT)" by simp
hence "w_addrs (w_values P vs (obs @ [ob])) ⊆ w_addrs (w_values P vs obs)"
by(cases hT)(auto simp add: w_addrs_def default_val_not_Addr Addr_not_default_val)
moreover from ob ta have "NormalAction (NewHeapElem ad hT) ∈ set ⦃ta⦄⇘o⇙" by simp
from init_fin_red_New_allocatedD[OF red this] have "ad ∈ allocated m'" ..
with redT_normal have "ad ∈ allocated (shr s')" by auto
ultimately show ?thesis using IH ob by(auto simp add: new_obs_addrs_if_def)
next
case (4 ad al v)
note ob = ‹ob = NormalAction (ReadMem ad al v)›
{ fix ad'
assume v: "v = Addr ad'"
with tasc ob have mrw: "Addr ad' ∈ w_values P vs obs (ad, al)"
by(auto simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend simp del: lappend_llist_of_llist_of)
hence "ad' ∈ w_addrs (w_values P vs obs)"
by(auto simp add: w_addrs_def)
with IH have "ad' ∈ allocated (shr s')" by blast }
with ob IH show ?thesis by(cases v)(simp_all add: new_obs_addrs_if_def)
qed(simp_all add: new_obs_addrs_if_def)
thus ?case by simp
qed }
note this[of "⦃ta⦄⇘o⇙" "[]"]
moreover have "if.known_addrs_state s' ⊆ if.known_addrs_state s ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
using ‹mthr.if.redT s (t, ta) s'› by(rule if_redT_known_addrs_new)
ultimately show ?thesis using ka allocated_subset by blast
qed
thus ?thesis1 ?thesis2 by simp_all
qed
lemma RedT_non_speculative_known_addrs_allocated:
assumes red: "mthr.if.RedT s ttas s'"
and tasc: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
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 s'")
and "w_addrs (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) ⊆ allocated (shr s')" (is "?thesis2 s' ttas")
proof -
from red tasc have "?thesis1 s' ∧ ?thesis2 s' ttas"
proof(induct rule: mthr.if.RedT_induct')
case refl thus ?case using ka vs by simp
next
case (step ttas s' t ta s'')
hence "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta⦄⇘o⇙)"
and "?thesis1 s'" "?thesis2 s' ttas"
by(simp_all add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
from redT_non_speculative_known_addrs_allocated[OF ‹mthr.if.redT s' (t, ta) s''› this]
show ?case by simp
qed
thus "?thesis1 s'" "?thesis2 s' ttas" by simp_all
qed
lemma read_ex_NewHeapElem [consumes 5, case_names start Red]:
assumes RedT: "mthr.if.RedT (init_fin_lift_state status (start_state f P C M vs)) ttas s"
and red: "mthr.if.redT s (t, ta) s'"
and read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
and sc: "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and known: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
obtains (start) CTn where "NewHeapElem ad CTn ∈ set start_heap_obs"
| (Red) ttas' s'' t' ta' s''' ttas'' CTn
where "mthr.if.RedT (init_fin_lift_state status (start_state f P C M vs)) ttas' s''"
and "mthr.if.redT s'' (t', ta') s'''"
and "mthr.if.RedT s''' ttas'' s"
and "ttas = ttas' @ (t', ta') # ttas''"
and "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙"
proof -
let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"
let ?obs_prefix = "lift_start_obs start_tid start_heap_obs"
let ?vs_start = "w_values P (λ_. {}) (map snd ?obs_prefix)"
from sc have "non_speculative P (w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs))) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
by(simp add: non_speculative_lappend lappend_llist_of_llist_of[symmetric] del: lappend_llist_of_llist_of)
with RedT have "if.known_addrs_state s ⊆ allocated (shr s)"
proof(rule RedT_non_speculative_known_addrs_allocated)
show "if.known_addrs_state ?start_state ⊆ allocated (shr ?start_state)"
using known
by(auto simp add: if.known_addrs_state_def if.known_addrs_thr_def start_state_def init_fin_lift_state_def split_beta split: if_split_asm)
have "w_addrs ?vs_start ⊆ w_addrs (λ_. {})" by(rule w_addrs_lift_start_heap_obs)
thus "w_addrs ?vs_start ⊆ allocated (shr ?start_state)" by simp
qed
also from red read obtain x_ra x'_ra m'_ra
where red'_ra: "t ⊢ (x_ra, shr s) -ta→i (x'_ra, m'_ra)"
and s': "redT_upd s t ta x'_ra m'_ra s'"
and ts_t: "thr s t = ⌊(x_ra, no_wait_locks)⌋"
by cases auto
from red'_ra read
have "ad ∈ known_addrs_if t x_ra" by(rule if_red_read_knows_addr)
hence "ad ∈ if.known_addrs_state s" using ts_t by(rule if.known_addrs_stateI)
finally have "ad ∈ allocated (shr s)" .
show ?thesis
proof(cases "ad ∈ allocated start_heap")
case True
then obtain CTn where "NewHeapElem ad CTn ∈ set start_heap_obs"
unfolding start_addrs_allocated by(blast dest: start_addrs_NewHeapElem_start_heap_obsD)
thus ?thesis by(rule start)
next
case False
hence "ad ∉ allocated (shr ?start_state)" by(simp add: start_state_def split_beta shr_init_fin_lift_state)
with RedT ‹ad ∈ allocated (shr s)› obtain t' ta' CTn
where tta: "(t', ta') ∈ set ttas"
and new: "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙"
by(blast dest: init_fin_RedT_allocated_NewHeapElemD)
from tta obtain ttas' ttas'' where ttas: "ttas = ttas' @ (t', ta') # ttas''" by(auto dest: split_list)
with RedT obtain s'' s'''
where "mthr.if.RedT ?start_state ttas' s''"
and "mthr.if.redT s'' (t', ta') s'''"
and "mthr.if.RedT s''' ttas'' s"
unfolding mthr.if.RedT_def by(auto elim!: rtrancl3p_appendE dest!: converse_rtrancl3p_step)
thus thesis using ttas new by(rule Red)
qed
qed
end
locale known_addrs_typing =
known_addrs
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated known_addrs
final r P
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 wfx :: "'thread_id ⇒ 'x ⇒ 'heap ⇒ bool"
and P :: "'md prog"
+
assumes wfs_non_speculative_invar:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙)) ⟧
⟹ wfx t x' m'"
and wfs_non_speculative_spawn:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙));
NewThread t'' x'' m'' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ wfx t'' x'' m''"
and wfs_non_speculative_other:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙));
wfx t'' x'' m ⟧
⟹ wfx t'' x'' m'"
and wfs_non_speculative_vs_conf:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
vs_conf P m vs; non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙))) ⟧
⟹ vs_conf P m' (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
and red_read_typeable:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ∃T. P,m ⊢ ad@al : T"
and red_NewHeapElemD:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m; NewHeapElem ad hT ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ typeof_addr m' ad = ⌊hT⌋"
and red_hext_incr:
"⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙)) ⟧
⟹ m ⊴ m'"
begin
lemma redT_wfs_non_speculative_invar:
assumes redT: "mthr.redT s (t, ta) s'"
and wfx: "ts_ok wfx (thr s) (shr s)"
and vs: "vs_conf P (shr s) vs"
and ns: "non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙))"
shows "ts_ok wfx (thr s') (shr s')"
using redT
proof(cases)
case (redT_normal x x' m')
with vs wfx ns show ?thesis
apply(clarsimp intro!: ts_okI split: if_split_asm)
apply(erule wfs_non_speculative_invar, auto dest: ts_okD)
apply(rename_tac t' x' ln ws')
apply(case_tac "thr s t'")
apply(frule (2) redT_updTs_new_thread, clarify)
apply(frule (1) mthr.new_thread_memory)
apply(auto intro: wfs_non_speculative_other wfs_non_speculative_spawn dest: ts_okD simp add: redT_updTs_Some)
done
next
case (redT_acquire x ln n)
thus ?thesis using wfx by(auto intro!: ts_okI dest: ts_okD split: if_split_asm)
qed
lemma redT_wfs_non_speculative_vs_conf:
assumes redT: "mthr.redT s (t, ta) s'"
and wfx: "ts_ok wfx (thr s) (shr s)"
and conf: "vs_conf P (shr s) vs"
and ns: "non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
shows "vs_conf P (shr s') (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
using redT
proof(cases)
case (redT_normal x x' m')
thus ?thesis using ns conf wfx by(auto dest: wfs_non_speculative_vs_conf ts_okD)
next
case (redT_acquire x l ln)
have "w_values P vs (take n (map NormalAction (convert_RA ln :: ('addr, 'thread_id) obs_event list))) = vs"
by(fastforce dest: in_set_takeD simp add: convert_RA_not_write intro!: w_values_no_write_unchanged del: equalityI)
thus ?thesis using conf redT_acquire by(auto)
qed
lemma if_redT_non_speculative_invar:
assumes red: "mthr.if.redT s (t, ta) s'"
and ts_ok: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and sc: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
and vs: "vs_conf P (shr s) vs"
shows "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
proof -
let ?s = "λs. (locks s, (λt. map_option (λ((status, x), ln). (x, ln)) (thr s t), shr s), wset s, interrupts s)"
from ts_ok have ts_ok': "ts_ok wfx (thr (?s s)) (shr (?s s))" by(auto intro!: ts_okI dest: ts_okD)
from vs have vs': "vs_conf P (shr (?s s)) vs" by simp
from red show ?thesis
proof(cases)
case (redT_normal x x' m)
note tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
from ‹t ⊢ (x, shr s) -ta→i (x', m)›
show ?thesis
proof(cases)
case (NormalAction X TA X')
from ‹ta = convert_TA_initial (convert_obs_initial TA)› ‹mthr.if.actions_ok s t ta›
have "mthr.actions_ok (?s s) t TA"
by(auto elim: rev_iffD1[OF _ thread_oks_ts_change] cond_action_oks_final_change)
with tst NormalAction ‹redT_upd s t ta x' m s'› have "mthr.redT (?s s) (t, TA) (?s s')"
using map_redT_updTs[of snd "thr s" "⦃ta⦄⇘t⇙"]
by(auto intro!: mthr.redT.intros simp add: split_def map_prod_def o_def fun_eq_iff)
moreover note ts_ok' vs'
moreover from ‹ta = convert_TA_initial (convert_obs_initial TA)› have "⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙" by(auto)
with sc have "non_speculative P vs (llist_of (map NormalAction ⦃TA⦄⇘o⇙))" by simp
ultimately have "ts_ok wfx (thr (?s s')) (shr (?s s'))"
by(auto dest: redT_wfs_non_speculative_invar)
thus ?thesis using ‹⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙› by(auto intro!: ts_okI dest: ts_okD)
next
case InitialThreadAction
with redT_normal ts_ok' vs show ?thesis
by(auto 4 3 intro!: ts_okI dest: ts_okD split: if_split_asm)
next
case ThreadFinishAction
with redT_normal ts_ok' vs show ?thesis
by(auto 4 3 intro!: ts_okI dest: ts_okD split: if_split_asm)
qed
next
case (redT_acquire x ln l)
thus ?thesis using vs ts_ok by(auto 4 3 intro!: ts_okI dest: ts_okD split: if_split_asm)
qed
qed
lemma if_redT_non_speculative_vs_conf:
assumes red: "mthr.if.redT s (t, ta) s'"
and ts_ok: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and sc: "non_speculative P vs (llist_of (take n ⦃ta⦄⇘o⇙))"
and vs: "vs_conf P (shr s) vs"
shows "vs_conf P (shr s') (w_values P vs (take n ⦃ta⦄⇘o⇙))"
proof -
let ?s = "λs. (locks s, (λt. map_option (λ((status, x), ln). (x, ln)) (thr s t), shr s), wset s, interrupts s)"
from ts_ok have ts_ok': "ts_ok wfx (thr (?s s)) (shr (?s s))" by(auto intro!: ts_okI dest: ts_okD)
from vs have vs': "vs_conf P (shr (?s s)) vs" by simp
from red show ?thesis
proof(cases)
case (redT_normal x x' m)
note tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
from ‹t ⊢ (x, shr s) -ta→i (x', m)›
show ?thesis
proof(cases)
case (NormalAction X TA X')
from ‹ta = convert_TA_initial (convert_obs_initial TA)› ‹mthr.if.actions_ok s t ta›
have "mthr.actions_ok (?s s) t TA"
by(auto elim: rev_iffD1[OF _ thread_oks_ts_change] cond_action_oks_final_change)
with tst NormalAction ‹redT_upd s t ta x' m s'› have "mthr.redT (?s s) (t, TA) (?s s')"
using map_redT_updTs[of snd "thr s" "⦃ta⦄⇘t⇙"]
by(auto intro!: mthr.redT.intros simp add: split_def map_prod_def o_def fun_eq_iff)
moreover note ts_ok' vs'
moreover from ‹ta = convert_TA_initial (convert_obs_initial TA)› have "⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙" by(auto)
with sc have "non_speculative P vs (llist_of (take n (map NormalAction ⦃TA⦄⇘o⇙)))" by simp
ultimately have "vs_conf P (shr (?s s')) (w_values P vs (take n (map NormalAction ⦃TA⦄⇘o⇙)))"
by(auto dest: redT_wfs_non_speculative_vs_conf)
thus ?thesis using ‹⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙› by(auto)
next
case InitialThreadAction
with redT_normal vs show ?thesis by(auto simp add: take_Cons')
next
case ThreadFinishAction
with redT_normal vs show ?thesis by(auto simp add: take_Cons')
qed
next
case (redT_acquire x l ln)
have "w_values P vs (take n (map NormalAction (convert_RA ln :: ('addr, 'thread_id) obs_event list))) = vs"
by(fastforce simp add: convert_RA_not_write take_Cons' dest: in_set_takeD intro!: w_values_no_write_unchanged del: equalityI)
thus ?thesis using vs redT_acquire by auto
qed
qed
lemma if_RedT_non_speculative_invar:
assumes red: "mthr.if.RedT s ttas s'"
and tsok: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and sc: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and vs: "vs_conf P (shr s) vs"
shows "ts_ok (init_fin_lift wfx) (thr s') (shr s')" (is ?thesis1)
and "vs_conf P (shr s') (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))" (is ?thesis2)
using red tsok sc vs unfolding mthr.if.RedT_def
proof(induct arbitrary: vs rule: rtrancl3p_converse_induct')
case refl
case 1 thus ?case by -
case 2 thus ?case by simp
next
case (step s tta s' ttas)
obtain t ta where tta: "tta = (t, ta)" by(cases tta)
case 1
hence sc1: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
and sc2: "non_speculative P (w_values P vs ⦃ta⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
unfolding lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def llist_of.simps llist.map(2) lconcat_LCons tta
by(simp_all add: non_speculative_lappend list_of_lconcat o_def)
from if_redT_non_speculative_invar[OF step(2)[unfolded tta] _ sc1] if_redT_non_speculative_vs_conf[OF step(2)[unfolded tta], where vs = vs and n="length ⦃ta⦄⇘o⇙"] 1 step.hyps(3)[of "w_values P vs ⦃ta⦄⇘o⇙"] sc2 sc1
show ?case by simp
case 2
hence sc1: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
and sc2: "non_speculative P (w_values P vs ⦃ta⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
unfolding lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def llist_of.simps llist.map(2) lconcat_LCons tta
by(simp_all add: non_speculative_lappend list_of_lconcat o_def)
from if_redT_non_speculative_invar[OF step(2)[unfolded tta] _ sc1] if_redT_non_speculative_vs_conf[OF step(2)[unfolded tta], where vs = vs and n="length ⦃ta⦄⇘o⇙"] 2 step.hyps(4)[of "w_values P vs ⦃ta⦄⇘o⇙"] sc2 sc1
show ?case by(simp add: tta o_def)
qed
lemma init_fin_hext_incr:
assumes "t ⊢ (x, m) -ta→i (x', m')"
and "init_fin_lift wfx t x m"
and "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
and "vs_conf P m vs"
shows "m ⊴ m'"
using assms
by(cases)(auto intro: red_hext_incr)
lemma init_fin_redT_hext_incr:
assumes "mthr.if.redT s (t, ta) s'"
and "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
and "vs_conf P (shr s) vs"
shows "shr s ⊴ shr s'"
using assms
by(cases)(auto dest: init_fin_hext_incr ts_okD)
lemma init_fin_RedT_hext_incr:
assumes "mthr.if.RedT s ttas s'"
and "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and sc: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and vs: "vs_conf P (shr s) vs"
shows "shr s ⊴ shr s'"
using assms
proof(induction rule: mthr.if.RedT_induct')
case refl thus ?case by simp
next
case (step ttas s' t ta s'')
note ts_ok = ‹ts_ok (init_fin_lift wfx) (thr s) (shr s)›
from ‹non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas @ [(t, ta)]))))›
have ns: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and ns': "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta⦄⇘o⇙)"
by(simp_all add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
from ts_ok ns have "shr s ⊴ shr s'"
using ‹vs_conf P (shr s) vs› by(rule step.IH)
also have "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
using ‹mthr.if.RedT s ttas s'› ts_ok ns ‹vs_conf P (shr s) vs›
by(rule if_RedT_non_speculative_invar)
with ‹mthr.if.redT s' (t, ta) s''›
have "… ⊴ shr s''" using ns'
proof(rule init_fin_redT_hext_incr)
from ‹mthr.if.RedT s ttas s'› ts_ok ns ‹vs_conf P (shr s) vs›
show "vs_conf P (shr s') (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
by(rule if_RedT_non_speculative_invar)
qed
finally show ?case .
qed
lemma init_fin_red_read_typeable:
assumes "t ⊢ (x, m) -ta→i (x', m')"
and "init_fin_lift wfx t x m" "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
shows "∃T. P,m ⊢ ad@al : T"
using assms
by cases(auto dest: red_read_typeable)
lemma Ex_new_action_for:
assumes wf: "wf_syscls P"
and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
and E: "E ∈ ℰ_start f P C M vs status"
and read: "ra ∈ read_actions E"
and aloc: "adal ∈ action_loc P E ra"
and sc: "non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E))"
shows "∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra"
proof -
let ?obs_prefix = "lift_start_obs start_tid start_heap_obs"
let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"
from start_state_vs_conf[OF wf]
have vs_conf_start: "vs_conf P start_heap (w_values P (λ_. {}) (map NormalAction start_heap_obs))"
by(simp add: lift_start_obs_def o_def)
obtain ad al where adal: "adal = (ad, al)" by(cases adal)
with read aloc obtain v where ra: "action_obs E ra = NormalAction (ReadMem ad al v)"
and ra_len: "enat ra < llength E"
by(cases "lnth E ra")(auto elim!: read_actions.cases actionsE)
from E obtain E'' where E: "E = lappend (llist_of ?obs_prefix) 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)
have ra_len': "length ?obs_prefix ≤ ra"
proof(rule ccontr)
assume "¬ ?thesis"
hence "ra < length ?obs_prefix" by simp
moreover with ra ra_len E obtain ra' ad al v
where "start_heap_obs ! ra' = ReadMem ad al v" "ra' < length start_heap_obs"
by(cases ra)(auto simp add: lnth_LCons lnth_lappend1 action_obs_def lift_start_obs_def)
ultimately have "ReadMem ad al v ∈ set start_heap_obs" unfolding in_set_conv_nth by blast
thus False by(simp add: start_heap_obs_not_Read)
qed
let ?n = "length ?obs_prefix"
from ra ra_len ra_len' E have "enat (ra - ?n) < llength E''"
and ra_obs: "action_obs E'' (ra - ?n) = NormalAction (ReadMem ad al v)"
by(cases "llength E''", auto simp add: action_obs_def lnth_lappend2)
from τRuns ‹enat (ra - ?n) < llength E''› obtain ra_m ra_n t_ra ta_ra
where E_ra: "lnth E'' (ra - ?n) = (t_ra, ⦃ta_ra⦄⇘o⇙ ! ra_n)"
and ra_n: "ra_n < length ⦃ta_ra⦄⇘o⇙" and ra_m: "enat ra_m < llength E'"
and ra_conv: "ra - ?n = (∑i<ra_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + ra_n"
and E'_ra_m: "lnth E' ra_m = (t_ra, ta_ra)"
unfolding E' by(rule mthr.if.actions_ℰE_aux)
let ?E' = "ldropn (Suc ra_m) E'"
have E'_unfold: "E' = lappend (ltake (enat ra_m) E') (LCons (lnth E' ra_m) ?E')"
unfolding ldropn_Suc_conv_ldropn[OF ra_m] by simp
hence "mthr.if.mthr.Runs ?start_state (lappend (ltake (enat ra_m) E') (LCons (lnth E' ra_m) ?E'))"
using τRuns by simp
then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of (ltake (enat ra_m) E')) σ'"
and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' ra_m) ?E')"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns' obtain σ'' where red_ra: "mthr.if.redT σ' (t_ra, ta_ra) σ''"
and τRuns'': "mthr.if.mthr.Runs σ'' ?E'"
unfolding E'_ra_m by cases
from E_ra ra_n ra_obs have "NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙"
by(auto simp add: action_obs_def in_set_conv_nth)
with red_ra obtain x_ra x'_ra m'_ra
where red'_ra: "mthr.init_fin t_ra (x_ra, shr σ') ta_ra (x'_ra, m'_ra)"
and σ'': "redT_upd σ' t_ra ta_ra x'_ra m'_ra σ''"
and ts_t_a: "thr σ' t_ra = ⌊(x_ra, no_wait_locks)⌋"
by cases auto
from red'_ra ‹NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙›
obtain ta'_ra X_ra X'_ra
where x_ra: "x_ra = (Running, X_ra)"
and x'_ra: "x'_ra = (Running, X'_ra)"
and ta_ra: "ta_ra = convert_TA_initial (convert_obs_initial ta'_ra)"
and red''_ra: "t_ra ⊢ (X_ra, shr σ') -ta'_ra→ (X'_ra, m'_ra)"
by cases fastforce+
from ‹NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙› ta_ra
have "ReadMem ad al v ∈ set ⦃ta'_ra⦄⇘o⇙" by auto
from wfx_start have wfx_start: "ts_ok (init_fin_lift wfx) (thr ?start_state) (shr ?start_state)"
by(simp add: start_state_def split_beta)
from sc ra_len'
have "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix))
(lmap snd (ltake (enat (ra - ?n)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E'))))"
unfolding E E' by(simp add: ltake_lappend2 lmap_lappend_distrib non_speculative_lappend)
also note ra_conv also note plus_enat_simps(1)[symmetric]
also have "enat (∑i<ra_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = (∑i<ra_m. enat (length ⦃snd (lnth E' i)⦄⇘o⇙))"
by(subst sum_comp_morphism[symmetric])(simp_all add: zero_enat_def)
also have "… = (∑i<ra_m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i))"
using ra_m by-(rule sum.cong[OF refl], simp add: le_less_trans[where y="enat ra_m"] split_beta)
also note ltake_plus_conv_lappend also note lconcat_ltake[symmetric]
also note lmap_lappend_distrib
also note non_speculative_lappend
finally have "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix)) (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of (list_of (ltake (enat ra_m) E'))))))"
by(simp add: split_def)
hence sc': "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat ra_m) E')))))"
unfolding lmap_lconcat llist.map_comp o_def lconcat_llist_of[symmetric] lmap_llist_of[symmetric]
by(simp add: split_beta o_def)
from vs_conf_start have vs_conf_start: "vs_conf P (shr ?start_state) (w_values P (λ_. {}) (map snd ?obs_prefix))"
by(simp add:init_fin_lift_state_conv_simps start_state_def split_beta lift_start_obs_def o_def)
with σ_σ' wfx_start sc' have "ts_ok (init_fin_lift wfx) (thr σ') (shr σ')"
unfolding mthr.if.RedT_def[symmetric] by(rule if_RedT_non_speculative_invar)
with ts_t_a have "wfx t_ra X_ra (shr σ')" unfolding x_ra by(auto dest: ts_okD)
with red''_ra ‹ReadMem ad al v ∈ set ⦃ta'_ra⦄⇘o⇙›
obtain T' where type_adal: "P,shr σ' ⊢ ad@al : T'" by(auto dest: red_read_typeable)
from sc ra_len' have "non_speculative P (λ_. {}) (llist_of (map snd ?obs_prefix))"
unfolding E by(simp add: ltake_lappend2 lmap_lappend_distrib non_speculative_lappend)
with sc' have sc'': "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat ra_m) E')))))"
by(simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
from σ_σ' red_ra ‹NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙› sc'' ka
show "∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra"
unfolding mthr.if.RedT_def[symmetric]
proof(cases rule: read_ex_NewHeapElem)
case (start CTn)
then obtain n where n: "start_heap_obs ! n = NewHeapElem ad CTn"
and len: "n < length start_heap_obs"
unfolding in_set_conv_nth by blast
from len have "Suc n ∈ actions E" unfolding E by(simp add: actions_def enat_less_enat_plusI)
moreover
from σ_σ' have hext: "start_heap ⊴ shr σ'" unfolding mthr.if.RedT_def[symmetric]
using wfx_start sc' vs_conf_start
by(auto dest!: init_fin_RedT_hext_incr simp add: start_state_def split_beta init_fin_lift_state_conv_simps)
from start have "typeof_addr start_heap ad = ⌊CTn⌋"
by(auto dest: NewHeapElem_start_heap_obsD[OF wf])
with hext have "typeof_addr (shr σ') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
with type_adal have "adal ∈ action_loc P E (Suc n)" using n len unfolding E adal
by cases(auto simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
moreover have "is_new_action (action_obs E (Suc n))" using n len unfolding E
by(simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
ultimately have "Suc n ∈ new_actions_for P E adal" by(rule new_actionsI)
moreover have "Suc n < ra" using ra_len' len by(simp)
ultimately show ?thesis by blast
next
case (Red ttas' s'' t' ta' s''' ttas'' CTn)
from ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
obtain obs obs' where obs: "⦃ta'⦄⇘o⇙ = obs @ NormalAction (NewHeapElem ad CTn) # obs'"
by(auto dest: split_list)
let ?wa = "?n + length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs"
have "enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) < enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas' @ [(t', ta')]))))"
using obs by simp
also have "… = llength (lconcat (lmap llist_of (lmap (λ(t, ta). ⦃ta⦄⇘o⇙) (llist_of (ttas' @ [(t', ta')])))))"
by(simp del: map_map map_append add: lconcat_llist_of)
also have "… ≤ llength (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (llist_of (ttas' @ (t', ta') # ttas''))))"
by(auto simp add: o_def split_def intro: lprefix_llist_ofI intro!: lprefix_lconcatI lprefix_llength_le)
also note len_less = calculation
have "… ≤ (∑i<ra_m. llength (lnth (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) E') i))"
unfolding ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›[symmetric]
by(simp add: ltake_lmap[symmetric] lconcat_ltake del: ltake_lmap)
also have "… = enat (∑i<ra_m. length ⦃snd (lnth E' i)⦄⇘o⇙)" using ra_m
by(subst sum_comp_morphism[symmetric, where h="enat"])(auto intro: sum.cong simp add: zero_enat_def less_trans[where y="enat ra_m"] split_beta)
also have "… ≤ enat (ra - ?n)" unfolding ra_conv by simp
finally have enat_length: "enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) < enat (ra - length (lift_start_obs start_tid start_heap_obs))" .
then have wa_ra: "?wa < ra" by simp
with ra_len have "?wa ∈ actions E" by(cases "llength E")(simp_all add: actions_def)
moreover
from ‹mthr.if.redT s'' (t', ta') s'''› ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
obtain x_wa x_wa' where ts''t': "thr s'' t' = ⌊(x_wa, no_wait_locks)⌋"
and red_wa: "mthr.init_fin t' (x_wa, shr s'') ta' (x_wa', shr s''')"
by(cases) fastforce+
from sc'
have ns: "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
and ns': "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) (llist_of ⦃ta'⦄⇘o⇙)"
and ns'': "non_speculative P (w_values P (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'')))"
unfolding ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›
by(simp_all add: lappend_llist_of_llist_of[symmetric] lmap_lappend_distrib non_speculative_lappend del: lappend_llist_of_llist_of)
from ‹mthr.if.RedT ?start_state ttas' s''› wfx_start ns
have ts_ok'': "ts_ok (init_fin_lift wfx) (thr s'') (shr s'')"
using vs_conf_start by(rule if_RedT_non_speculative_invar)
with ts''t' have wfxt': "wfx t' (snd x_wa) (shr s'')" by(cases x_wa)(auto dest: ts_okD)
{
have "action_obs E ?wa =
snd (lnth (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')) (length (concat (map (λ(t, y). ⦃y⦄⇘o⇙) ttas')) + length obs))"
unfolding E E' by(simp add: action_obs_def lnth_lappend2)
also from enat_length ‹enat (ra - ?n) < llength E''›
have "… = lnth (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) E')) (length (concat (map (λ(t, y). ⦃y⦄⇘o⇙) ttas')) + length obs)"
unfolding E'
by(subst lnth_lmap[symmetric, where f=snd])(erule (1) less_trans, simp add: lmap_lconcat llist.map_comp split_def o_def)
also from len_less
have "enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) < llength (lconcat (ltake (enat ra_m) (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) E')))"
unfolding ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›[symmetric]
by(simp add: ltake_lmap[symmetric] del: ltake_lmap)
note lnth_lconcat_ltake[OF this, symmetric]
also note ltake_lmap
also have "ltake (enat ra_m) E' = llist_of (list_of (ltake (enat ra_m) E'))" by(simp)
also note ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›
also note lmap_llist_of also have "(λ(t, ta). llist_of ⦃ta⦄⇘o⇙) = llist_of ∘ (λ(t, ta). ⦃ta⦄⇘o⇙)"
by(simp add: o_def split_def)
also note map_map[symmetric] also note lconcat_llist_of
also note lnth_llist_of
also have "concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas' @ (t', ta') # ttas'')) ! (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) = NormalAction (NewHeapElem ad CTn)"
by(simp add: nth_append obs)
finally have "action_obs E ?wa = NormalAction (NewHeapElem ad CTn)" .
}
note wa_obs = this
from ‹mthr.if.RedT ?start_state ttas' s''› wfx_start ns vs_conf_start
have vs'': "vs_conf P (shr s'') (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
by(rule if_RedT_non_speculative_invar)
from if_redT_non_speculative_vs_conf[OF ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' _ vs'', of "length ⦃ta'⦄⇘o⇙"] ns'
have vs''': "vs_conf P (shr s''') (w_values P (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙)"
by simp
from ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' ns' vs''
have "ts_ok (init_fin_lift wfx) (thr s''') (shr s''')"
by(rule if_redT_non_speculative_invar)
with ‹mthr.if.RedT s''' ttas'' σ'›
have hext: "shr s''' ⊴ shr σ'" using ns'' vs'''
by(rule init_fin_RedT_hext_incr)
from red_wa have "typeof_addr (shr s''') ad = ⌊CTn⌋"
using wfxt' ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙› by cases(auto dest: red_NewHeapElemD)
with hext have "typeof_addr (shr σ') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
with type_adal have "adal ∈ action_loc P E ?wa" using wa_obs unfolding E adal
by cases (auto simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
moreover have "is_new_action (action_obs E ?wa)" using wa_obs by simp
ultimately have "?wa ∈ new_actions_for P E adal" by(rule new_actionsI)
thus ?thesis using wa_ra by blast
qed
qed
lemma executions_sc_hb:
assumes "wf_syscls P"
and "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
and "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
shows
"executions_sc_hb (ℰ_start f P C M vs status) P"
(is "executions_sc_hb ?E P")
proof
fix E a adal a'
assume "E ∈ ?E" "a ∈ new_actions_for P E adal" "a' ∈ new_actions_for P E adal"
thus "a = a'" by(rule ℰ_new_actions_for_unique)
next
fix E ra adal
assume "E ∈ ?E" "ra ∈ read_actions E" "adal ∈ action_loc P E ra"
and "non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E))"
with assms show "∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra"
by(rule Ex_new_action_for)
qed
lemma executions_aux:
assumes wf: "wf_syscls P"
and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap" (is "ts_ok wfx (thr ?start_state) _")
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
shows "executions_aux (ℰ_start f P C M vs status) P"
(is "executions_aux ?ℰ P")
proof
fix E a adal a'
assume "E ∈ ?ℰ" "a ∈ new_actions_for P E adal" "a' ∈ new_actions_for P E adal"
thus "a = a'" by(rule ℰ_new_actions_for_unique)
next
fix E ws r adal
assume E: "E ∈ ?ℰ"
and wf_exec: "P ⊢ (E, ws) √"
and read: "r ∈ read_actions E" "adal ∈ action_loc P E r"
and sc: "⋀a. ⟦a < r; a ∈ read_actions E⟧ ⟹ P,E ⊢ a ↝mrw ws a"
interpret jmm: executions_sc_hb ?ℰ P
using wf wfx_start ka by(rule executions_sc_hb)
from E wf_exec sc
have "ta_seq_consist P Map.empty (ltake (enat r) (lmap snd E))"
unfolding ltake_lmap by(rule jmm.ta_seq_consist_mrwI) simp
hence "non_speculative P (λ_. {}) (ltake (enat r) (lmap snd E))"
by(rule ta_seq_consist_into_non_speculative) simp
with wf wfx_start ka E read
have "∃i. i ∈ new_actions_for P E adal ∧ i < r"
by(rule Ex_new_action_for)
thus "∃i<r. i ∈ new_actions_for P E adal" by blast
qed
lemma drf:
assumes cut_and_update:
"if.cut_and_update
(init_fin_lift_state status (start_state f P C M vs))
(mrw_values P Map.empty (map snd (lift_start_obs start_tid start_heap_obs)))"
(is "if.cut_and_update ?start_state (mrw_values _ _ (map _ ?start_heap_obs))")
and wf: "wf_syscls P"
and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
shows "drf (ℰ_start f P C M vs status) P" (is "drf ?ℰ _")
proof -
interpret jmm: executions_sc_hb "?ℰ" P
using wf wfx_start ka by(rule executions_sc_hb)
let ?n = "length ?start_heap_obs"
let ?ℰ' = "lappend (llist_of ?start_heap_obs) ` mthr.if.ℰ ?start_state"
show ?thesis
proof
fix E ws r
assume E: "E ∈ ?ℰ'"
and wf: "P ⊢ (E, ws) √"
and mrw: "⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
show "∃E'∈?ℰ'. ∃ws'. P ⊢ (E', ws') √ ∧ ltake (enat r) E = ltake (enat r) E' ∧
sequentially_consistent P (E', ws') ∧
action_tid E r = action_tid E' r ∧ action_obs E r ≈ action_obs E' r ∧
(r ∈ actions E ⟶ r ∈ actions E')"
proof(cases "∃r'. r' ∈ read_actions E ∧ r ≤ r'")
case False
have "sequentially_consistent P (E, ws)"
proof(rule sequentially_consistentI)
fix a
assume "a ∈ read_actions E"
with False have "a < r" by auto
thus "P,E ⊢ a ↝mrw ws a" using ‹a ∈ read_actions E› by(rule mrw)
qed
moreover have "action_obs E r ≈ action_obs E r" by(rule sim_action_refl)
ultimately show ?thesis using wf E by blast
next
case True
let ?P = "λr'. r' ∈ read_actions E ∧ r ≤ r'"
let ?r = "Least ?P"
from True obtain r' where r': "?P r'" by blast
hence r: "?P ?r" by(rule LeastI)
{
fix a
assume "a < ?r" "a ∈ read_actions E"
have "P,E ⊢ a ↝mrw ws a"
proof(cases "a < r")
case True
thus ?thesis using ‹a ∈ read_actions E› by(rule mrw)
next
case False
with ‹a ∈ read_actions E› have "?P a" by simp
hence "?r ≤ a" by(rule Least_le)
with ‹a < ?r› have False by simp
thus ?thesis ..
qed }
note mrw' = this
from E obtain E'' where E: "E = lappend (llist_of ?start_heap_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)
have r_len: "length ?start_heap_obs ≤ ?r"
proof(rule ccontr)
assume "¬ ?thesis"
hence "?r < length ?start_heap_obs" by simp
moreover with r E obtain t ad al v where "?start_heap_obs ! ?r = (t, NormalAction (ReadMem ad al v))"
by(cases "?start_heap_obs ! ?r")(fastforce elim!: read_actions.cases simp add: actions_def action_obs_def lnth_lappend1)
ultimately have "(t, NormalAction (ReadMem ad al v)) ∈ set ?start_heap_obs" unfolding in_set_conv_nth by blast
thus False by(auto simp add: start_heap_obs_not_Read)
qed
let ?n = "length ?start_heap_obs"
from r r_len E have r: "?r - ?n ∈ read_actions E''"
by(fastforce elim!: read_actions.cases simp add: actions_lappend action_obs_def lnth_lappend2 elim: actionsE intro: read_actions.intros)
from r have "?r - ?n ∈ actions E''" by(auto)
hence "enat (?r - ?n) < llength E''" by(rule actionsE)
with τRuns obtain r_m r_n t_r ta_r
where E_r: "lnth E'' (?r - ?n) = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)"
and r_n: "r_n < length ⦃ta_r⦄⇘o⇙" and r_m: "enat r_m < llength E'"
and r_conv: "?r - ?n = (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + r_n"
and E'_r_m: "lnth E' r_m = (t_r, ta_r)"
unfolding E' by(rule mthr.if.actions_ℰE_aux)
let ?E' = "ldropn (Suc r_m) E'"
let ?r_m_E' = "ltake (enat r_m) E'"
have E'_unfold: "E' = lappend (ltake (enat r_m) E') (LCons (lnth E' r_m) ?E')"
unfolding ldropn_Suc_conv_ldropn[OF r_m] by simp
hence "mthr.if.mthr.Runs ?start_state (lappend ?r_m_E' (LCons (lnth E' r_m) ?E'))"
using τRuns by simp
then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of ?r_m_E') σ'"
and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' r_m) ?E')"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns' obtain σ''' where red_ra: "mthr.if.redT σ' (t_r, ta_r) σ'''"
and τRuns'': "mthr.if.mthr.Runs σ''' ?E'"
unfolding E'_r_m by cases
let ?vs = "mrw_values P Map.empty (map snd ?start_heap_obs)"
{ fix a
assume "enat a < enat ?r"
and "a ∈ read_actions E"
have "a < r"
proof(rule ccontr)
assume "¬ a < r"
with ‹a ∈ read_actions E› have "?P a" by simp
hence "?r ≤ a" by(rule Least_le)
with ‹enat a < enat ?r› show False by simp
qed
hence "P,E ⊢ a ↝mrw ws a" using ‹a ∈ read_actions E› by(rule mrw) }
with ‹E ∈ ?ℰ'› wf have "ta_seq_consist P Map.empty (lmap snd (ltake (enat ?r) E))"
by(rule jmm.ta_seq_consist_mrwI)
hence start_sc: "ta_seq_consist P Map.empty (llist_of (map snd ?start_heap_obs))"
and "ta_seq_consist P ?vs (lmap snd (ltake (enat (?r - ?n)) E''))"
using ‹?n ≤ ?r› unfolding E ltake_lappend lmap_lappend_distrib
by(simp_all add: ta_seq_consist_lappend o_def)
note this(2) also from r_m
have r_m_sum_len_eq: "(∑i<r_m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) = enat (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
by(subst sum_comp_morphism[symmetric, where h=enat])(auto simp add: zero_enat_def split_def less_trans[where y="enat r_m"] intro: sum.cong)
hence "ltake (enat (?r - ?n)) E'' =
lappend (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))
(ltake (enat r_n) (ldrop (enat (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) E''))"
unfolding ltake_lmap[symmetric] lconcat_ltake r_conv plus_enat_simps(1)[symmetric] ltake_plus_conv_lappend
unfolding E' by simp
finally have "ta_seq_consist P ?vs (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E')))"
and sc_ta_r: "ta_seq_consist P (mrw_values P ?vs (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))))) (lmap snd (ltake (enat r_n) (ldropn (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) E'')))"
unfolding lmap_lappend_distrib by(simp_all add: ta_seq_consist_lappend split_def ldrop_enat)
note this(1) also
have "lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ltake (enat r_m) E')))
= llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of ?r_m_E')))"
unfolding lmap_lconcat llist.map_comp o_def split_def lconcat_llist_of[symmetric] map_map lmap_llist_of[symmetric]
by simp
finally have "ta_seq_consist P ?vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of ?r_m_E'))))" .
from if.sequential_completion[OF cut_and_update ta_seq_consist_convert_RA σ_σ'[folded mthr.if.RedT_def] this red_ra]
obtain ta' ttas'
where "mthr.if.mthr.Runs σ' (LCons (t_r, ta') ttas')"
and sc: "ta_seq_consist P (mrw_values P Map.empty (map snd ?start_heap_obs))
(lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of (list_of ?r_m_E')) (LCons (t_r, ta') ttas'))))"
and eq_ta: "eq_upto_seq_inconsist P ⦃ta_r⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P ?vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of ?r_m_E'))))"
by blast
let ?E_sc' = "lappend (llist_of (list_of ?r_m_E')) (LCons (t_r, ta') ttas')"
let ?E_sc'' = "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?E_sc')"
let ?E_sc = "lappend (llist_of ?start_heap_obs) ?E_sc''"
from σ_σ' ‹mthr.if.mthr.Runs σ' (LCons (t_r, ta') ttas')›
have "mthr.if.mthr.Runs ?start_state ?E_sc'" by(rule mthr.if.mthr.Trsys_into_Runs)
hence "?E_sc'' ∈ mthr.if.ℰ ?start_state" by(rule mthr.if.ℰ.intros)
hence "?E_sc ∈ ?ℰ" by(rule imageI)
moreover from ‹?E_sc'' ∈ mthr.if.ℰ ?start_state›
have tsa_ok: "thread_start_actions_ok ?E_sc" by(rule thread_start_actions_ok_init_fin)
from sc have "ta_seq_consist P Map.empty (lmap snd ?E_sc)"
by(simp add: lmap_lappend_distrib o_def lmap_lconcat llist.map_comp split_def ta_seq_consist_lappend start_sc)
from ta_seq_consist_imp_sequentially_consistent[OF tsa_ok jmm.ℰ_new_actions_for_fun[OF ‹?E_sc ∈ ?ℰ›] this]
obtain ws_sc where "sequentially_consistent P (?E_sc, ws_sc)"
and "P ⊢ (?E_sc, ws_sc) √" unfolding start_heap_obs_def[symmetric] by iprover
moreover {
have enat_sum_r_m_eq: "enat (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))"
by(auto intro: sum.cong simp add: less_trans[OF _ r_m] lnth_ltake llength_lconcat_lfinite_conv_sum sum_comp_morphism[symmetric, where h=enat] zero_enat_def[symmetric] split_beta)
also have "… ≤ llength E''" unfolding E'
by(blast intro: lprefix_llength_le lprefix_lconcatI lmap_lprefix)
finally have r_m_E: "ltake (enat (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙))) E = ltake (enat (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙))) ?E_sc"
by(simp add: ltake_lappend lappend_eq_lappend_conv lmap_lappend_distrib r_m_sum_len_eq ltake_lmap[symmetric] min_def zero_enat_def[symmetric] E E' lconcat_ltake ltake_all del: ltake_lmap)
have drop_r_m_E: "ldropn (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) E = lappend (llist_of (map (Pair t_r) ⦃ta_r⦄⇘o⇙)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ldropn (Suc r_m) E')))"
(is "_ = ?drop_r_m_E") using E'_r_m unfolding E E'
by(subst (2) E'_unfold)(simp add: ldropn_lappend2 lmap_lappend_distrib enat_sum_r_m_eq[symmetric])
have drop_r_m_E_sc: "ldropn (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) ?E_sc =
lappend (llist_of (map (Pair t_r) ⦃ta'⦄⇘o⇙)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas'))"
by(simp add: ldropn_lappend2 lmap_lappend_distrib enat_sum_r_m_eq[symmetric])
let ?vs_r_m = "mrw_values P ?vs (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))))"
note sc_ta_r also
from drop_r_m_E have "ldropn (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) E'' = ?drop_r_m_E"
unfolding E by(simp add: ldropn_lappend2)
also have "lmap snd (ltake (enat r_n) …) = llist_of (take r_n ⦃ta_r⦄⇘o⇙)" using r_n
by(simp add: ltake_lappend lmap_lappend_distrib ltake_lmap[symmetric] take_map o_def zero_enat_def[symmetric] del: ltake_lmap)
finally have sc_ta_r: "ta_seq_consist P ?vs_r_m (llist_of (take r_n ⦃ta_r⦄⇘o⇙))" .
note eq_ta
also have "⦃ta_r⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙ @ drop r_n ⦃ta_r⦄⇘o⇙" by simp
finally have "eq_upto_seq_inconsist P (take r_n ⦃ta_r⦄⇘o⇙ @ drop r_n ⦃ta_r⦄⇘o⇙) ⦃ta'⦄⇘o⇙ ?vs_r_m"
by(simp add: list_of_lconcat split_def o_def map_concat)
from eq_upto_seq_inconsist_appendD[OF this sc_ta_r]
have r_n': "r_n ≤ length ⦃ta'⦄⇘o⇙"
and take_r_n_eq: "take r_n ⦃ta'⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙"
and eq_r_n: "eq_upto_seq_inconsist P (drop r_n ⦃ta_r⦄⇘o⇙) (drop r_n ⦃ta'⦄⇘o⇙) (mrw_values P ?vs_r_m (take r_n ⦃ta_r⦄⇘o⇙))"
using r_n by(simp_all add: min_def)
from r_conv ‹?n ≤ ?r› have r_conv': "?r = (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) + r_n" by simp
from r_n' r_n take_r_n_eq r_m_E drop_r_m_E drop_r_m_E_sc
have take_r'_eq: "ltake (enat ?r) E = ltake (enat ?r) ?E_sc" unfolding r_conv'
apply(subst (1 2) plus_enat_simps(1)[symmetric])
apply(subst (1 2) ltake_plus_conv_lappend)
apply(simp add: lappend_eq_lappend_conv ltake_lappend1 ldrop_enat take_map)
done
hence take_r_eq: "ltake (enat r) E = ltake (enat r) ?E_sc"
by(rule ltake_eq_ltake_antimono)(simp add: ‹?P ?r›)
from eq_r_n Cons_nth_drop_Suc[OF r_n, symmetric]
have "drop r_n ⦃ta'⦄⇘o⇙ ≠ []" by(auto simp add: eq_upto_seq_inconsist_simps)
hence r_n': "r_n < length ⦃ta'⦄⇘o⇙" by simp
hence eq_r_n: "⦃ta_r⦄⇘o⇙ ! r_n ≈ ⦃ta'⦄⇘o⇙ ! r_n"
using eq_r_n Cons_nth_drop_Suc[OF r_n, symmetric] Cons_nth_drop_Suc[OF r_n', symmetric]
by(simp add: eq_upto_seq_inconsist_simps split: action.split_asm obs_event.split_asm if_split_asm)
obtain tid_eq: "action_tid E r = action_tid ?E_sc r"
and obs_eq: "action_obs E r ≈ action_obs ?E_sc r"
proof(cases "r < ?r")
case True
{ from True have "action_tid E r = action_tid (ltake (enat ?r) E) r"
by(simp add: action_tid_def lnth_ltake)
also note take_r'_eq
also have "action_tid (ltake (enat ?r) ?E_sc) r = action_tid ?E_sc r"
using True by(simp add: action_tid_def lnth_ltake)
finally have "action_tid E r = action_tid ?E_sc r" . }
moreover
{ from True have "action_obs E r = action_obs (ltake (enat ?r) E) r"
by(simp add: action_obs_def lnth_ltake)
also note take_r'_eq
also have "action_obs (ltake (enat ?r) ?E_sc) r = action_obs ?E_sc r"
using True by(simp add: action_obs_def lnth_ltake)
finally have "action_obs E r ≈ action_obs ?E_sc r" by simp }
ultimately show thesis by(rule that)
next
case False
with ‹?P ?r› have r_eq: "r = ?r" by simp
hence "lnth E r = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)" using E_r r_conv' E by(simp add: lnth_lappend2)
moreover have "lnth ?E_sc r = (t_r, ⦃ta'⦄⇘o⇙ ! r_n)" using ‹?n ≤ ?r› r_n'
by(subst r_eq)(simp add: r_conv lnth_lappend2 lmap_lappend_distrib enat_sum_r_m_eq[symmetric] lnth_lappend1 del: length_lift_start_obs)
ultimately have "action_tid E r = action_tid ?E_sc r" "action_obs E r ≈ action_obs ?E_sc r"
using eq_r_n by(simp_all add: action_tid_def action_obs_def)
thus thesis by(rule that)
qed
have "enat r < enat ?n + llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend ?r_m_E' (LCons (t_r, ta') LNil))))"
using ‹?P ?r› r_n' unfolding lmap_lappend_distrib
by(simp add: enat_sum_r_m_eq[symmetric] r_conv')
also have "llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend ?r_m_E' (LCons (t_r, ta') LNil)))) ≤ llength ?E_sc''"
by(rule lprefix_llength_le[OF lprefix_lconcatI])(simp add: lmap_lprefix)
finally have "r ∈ actions ?E_sc" by(simp add: actions_def add_left_mono)
note this tid_eq obs_eq take_r_eq }
ultimately show ?thesis by blast
qed
qed(rule ℰ_new_actions_for_unique)
qed
lemma sc_legal:
assumes hb_completion:
"if.hb_completion (init_fin_lift_state status (start_state f P C M vs)) (lift_start_obs start_tid start_heap_obs)"
(is "if.hb_completion ?start_state ?start_heap_obs")
and wf: "wf_syscls P"
and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
shows "sc_legal (ℰ_start f P C M vs status) P"
(is "sc_legal ?ℰ P")
proof -
interpret jmm: executions_sc_hb ?ℰ P
using wf wfx_start ka by(rule executions_sc_hb)
interpret jmm: executions_aux ?ℰ P
using wf wfx_start ka by(rule executions_aux)
show ?thesis
proof
fix E ws r
assume E: "E ∈ ?ℰ" and wf_exec: "P ⊢ (E, ws) √"
and mrw: "⋀a. ⟦a < r; a ∈ read_actions E⟧ ⟹ P,E ⊢ a ↝mrw ws a"
from E obtain E'' where E: "E = lappend (llist_of ?start_heap_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)
show "∃E'∈?ℰ. ∃ws'. P ⊢ (E', ws') √ ∧ ltake (enat r) E = ltake (enat r) E' ∧
(∀a∈read_actions E'. if a < r then ws' a = ws a else P,E' ⊢ ws' a ≤hb a) ∧
action_tid E' r = action_tid E r ∧
(if r ∈ read_actions E then sim_action else (=)) (action_obs E' r) (action_obs E r) ∧
(r ∈ actions E ⟶ r ∈ actions E')"
(is "∃E'∈?ℰ. ∃ws'. _ ∧ ?same E' ∧ ?read E' ws' ∧ ?tid E' ∧ ?obs E' ∧ ?actions E'")
proof(cases "r < length ?start_heap_obs")
case True
from if.hb_completion_Runs[OF hb_completion ta_hb_consistent_convert_RA]
obtain ttas where Runs: "mthr.if.mthr.Runs ?start_state ttas"
and hb: "ta_hb_consistent P ?start_heap_obs (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
by blast
from Runs have ℰ: "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas) ∈ mthr.if.ℰ ?start_state"
by(rule mthr.if.ℰ.intros)
let ?E = "lappend (llist_of ?start_heap_obs) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
from ℰ have E': "?E ∈ ?ℰ" by blast
from ℰ have tsa: "thread_start_actions_ok ?E" by(rule thread_start_actions_ok_init_fin)
from start_heap_obs_not_Read
have ws: "is_write_seen P (llist_of (lift_start_obs start_tid start_heap_obs)) ws"
by(unfold in_set_conv_nth)(rule is_write_seenI, auto simp add: action_obs_def actions_def lift_start_obs_def lnth_LCons elim!: read_actions.cases split: nat.split_asm)
with hb tsa
have "∃ws'. P ⊢ (?E, ws') √ ∧
(∀n. n ∈ read_actions ?E ⟶ length ?start_heap_obs ≤ n ⟶ P,?E ⊢ ws' n ≤hb n) ∧
(∀n<length ?start_heap_obs. ws' n = ws n)"
by(rule ta_hb_consistent_Read_hb)(rule jmm.ℰ_new_actions_for_fun[OF E'])
then obtain ws' where wf_exec': "P ⊢ (?E, ws') √"
and read_hb: "⋀n. ⟦ n ∈ read_actions ?E; length ?start_heap_obs ≤ n ⟧ ⟹ P,?E ⊢ ws' n ≤hb n"
and same: "⋀n. n<length ?start_heap_obs ⟹ ws' n = ws n" by blast
from True have "?same ?E" unfolding E by(simp add: ltake_lappend1)
moreover {
fix a
assume a: "a ∈ read_actions ?E"
have "if a < r then ws' a = ws a else P,?E ⊢ ws' a ≤hb a"
proof(cases "a < length ?start_heap_obs")
case True
with a have False using start_heap_obs_not_Read
by cases(auto simp add: action_obs_def actions_def lnth_lappend1 lift_start_obs_def lnth_LCons in_set_conv_nth split: nat.split_asm)
thus ?thesis ..
next
case False
with read_hb[of a] True a show ?thesis by auto
qed }
hence "?read ?E ws'" by blast
moreover from True E have "?tid ?E" by(simp add: action_tid_def lnth_lappend1)
moreover from True E have "?obs ?E" by(simp add: action_obs_def lnth_lappend1)
moreover from True have "?actions ?E" by(simp add: actions_def enat_less_enat_plusI)
ultimately show ?thesis using E' wf_exec' by blast
next
case False
hence r: "length ?start_heap_obs ≤ r" by simp
show ?thesis
proof(cases "enat r < llength E")
case False
then obtain "?same E" "?read E ws" "?tid E" "?obs E" "?actions E"
by(cases "llength E")(fastforce elim!: read_actions.cases simp add: actions_def split: if_split_asm)+
with wf_exec ‹E ∈ ?ℰ› show ?thesis by blast
next
case True
note r' = this
let ?r = "r - length ?start_heap_obs"
from E r r' have "enat ?r < llength E''" by(cases "llength E''")(auto)
with τRuns obtain r_m r_n t_r ta_r
where E_r: "lnth E'' ?r = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)"
and r_n: "r_n < length ⦃ta_r⦄⇘o⇙" and r_m: "enat r_m < llength E'"
and r_conv: "?r = (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + r_n"
and E'_r_m: "lnth E' r_m = (t_r, ta_r)"
unfolding E' by(rule mthr.if.actions_ℰE_aux)
let ?E' = "ldropn (Suc r_m) E'"
let ?r_m_E' = "ltake (enat r_m) E'"
have E'_unfold: "E' = lappend (ltake (enat r_m) E') (LCons (lnth E' r_m) ?E')"
unfolding ldropn_Suc_conv_ldropn[OF r_m] by simp
hence "mthr.if.mthr.Runs ?start_state (lappend ?r_m_E' (LCons (lnth E' r_m) ?E'))"
using τRuns by simp
then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of ?r_m_E') σ'"
and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' r_m) ?E')"
by(rule mthr.if.mthr.Runs_lappendE) simp
from τRuns' obtain σ''' where red_ra: "mthr.if.redT σ' (t_r, ta_r) σ'''"
and τRuns'': "mthr.if.mthr.Runs σ''' ?E'"
unfolding E'_r_m by cases
let ?vs = "mrw_values P Map.empty (map snd ?start_heap_obs)"
from ‹E ∈ ?ℰ› wf_exec have "ta_seq_consist P Map.empty (lmap snd (ltake (enat r) E))"
by(rule jmm.ta_seq_consist_mrwI)(simp add: mrw)
hence ns: "non_speculative P (λ_. {}) (lmap snd (ltake (enat r) E))"
by(rule ta_seq_consist_into_non_speculative) simp
also note E also note ltake_lappend2 also note E'
also note E'_unfold also note lmap_lappend_distrib also note lmap_lappend_distrib
also note lconcat_lappend also note llist.map(2) also note E'_r_m also note prod.simps(2)
also note ltake_lappend2 also note lconcat_LCons also note ltake_lappend1
also note non_speculative_lappend also note lmap_lappend_distrib also note non_speculative_lappend
also have "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ltake (enat r_m) E')) =
llist_of (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))))"
by(simp add: lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def split_def del: lmap_llist_of)
ultimately
have "non_speculative P (λ_. {}) (lmap snd (llist_of ?start_heap_obs))"
and "non_speculative P (w_values P (λ_. {}) (map snd ?start_heap_obs))
(lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ltake (enat r_m) E'))))"
and ns': "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?start_heap_obs)) (map snd (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))))))
(lmap snd (ltake (enat r_n) (llist_of (map (Pair t_r) ⦃ta_r⦄⇘o⇙))))"
using r r_conv r_m r_n
by(simp_all add: length_concat o_def split_def sum_list_sum_nth length_list_of_conv_the_enat less_min_eq1 atLeast0LessThan lnth_ltake split: if_split_asm cong: sum.cong_simp)
hence ns: "non_speculative P (w_values P (λ_. {}) (map snd ?start_heap_obs))
(llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E')))))"
unfolding lconcat_llist_of[symmetric] lmap_lconcat lmap_llist_of[symmetric] llist.map_comp o_def split_def
by(simp)
from ns'
have ns': "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?start_heap_obs)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))))) (llist_of (take r_n ⦃ta_r⦄⇘o⇙))"
unfolding map_concat map_map by(simp add: take_map[symmetric] o_def split_def)
let ?hb = "λta'_r :: ('addr, 'thread_id, status × 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event action) thread_action.
ta_hb_consistent P (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙)))"
let ?sim = "λta'_r. (if ∃ad al v. ⦃ta_r⦄⇘o⇙ ! r_n = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta_r⦄⇘o⇙ ! r_n) (⦃ta'_r⦄⇘o⇙ ! r_n)"
from red_ra obtain ta'_r σ''''
where red_ra': "mthr.if.redT σ' (t_r, ta'_r) σ''''"
and eq: "take r_n ⦃ta'_r⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙"
and hb: "?hb ta'_r"
and r_n': "r_n < length ⦃ta'_r⦄⇘o⇙"
and sim: "?sim ta'_r"
proof(cases)
case (redT_normal x x' m')
note tst = ‹thr σ' t_r = ⌊(x, no_wait_locks)⌋›
and red = ‹t_r ⊢ (x, shr σ') -ta_r→i (x', m')›
and aok = ‹mthr.if.actions_ok σ' t_r ta_r›
and σ''' = ‹redT_upd σ' t_r ta_r x' m' σ'''›
from if.hb_completionD[OF hb_completion σ_σ'[folded mthr.if.RedT_def] ns tst red aok ns'] r_n
obtain ta'_r x'' m''
where red': "t_r ⊢ (x, shr σ') -ta'_r→i (x'', m'')"
and aok': "mthr.if.actions_ok σ' t_r ta'_r"
and eq': "take r_n ⦃ta'_r⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙"
and hb: "?hb ta'_r"
and r_n': "r_n < length ⦃ta'_r⦄⇘o⇙"
and sim: "?sim ta'_r" by blast
from redT_updWs_total[of t_r "wset σ'" "⦃ta'_r⦄⇘w⇙"]
obtain σ'''' where "redT_upd σ' t_r ta'_r x'' m'' σ''''" by fastforce
with red' tst aok' have "mthr.if.redT σ' (t_r, ta'_r) σ''''" ..
thus thesis using eq' hb r_n' sim by(rule that)
next
case (redT_acquire x n ln)
hence "?hb ta_r" using set_convert_RA_not_Read[where ln=ln]
by -(rule ta_hb_consistent_not_ReadI, fastforce simp del: set_convert_RA_not_Read dest!: in_set_dropD)
with red_ra r_n show ?thesis by(auto intro: that)
qed
from hb
have "non_speculative P (w_values P (λ_. {}) (map snd (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)))) (lmap snd (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙))))"
by(rule ta_hb_consistent_into_non_speculative)
with ns' eq[symmetric] have "non_speculative P (w_values P (λ_. {}) (map snd (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E')))))) (llist_of (map snd (map (Pair t_r) ⦃ta'_r⦄⇘o⇙)))"
by(subst append_take_drop_id[where xs="⦃ta'_r⦄⇘o⇙" and n=r_n, symmetric])(simp add: o_def map_concat split_def lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: append_take_drop_id lappend_llist_of_llist_of)
with ns have ns'': "non_speculative P (w_values P (λ_. {}) (map snd ?start_heap_obs)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E') @ [(t_r, ta'_r)]))))"
unfolding lconcat_llist_of[symmetric] map_append lappend_llist_of_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp
by(simp add: o_def split_def non_speculative_lappend list_of_lconcat map_concat)
from σ_σ' red_ra' have "mthr.if.RedT ?start_state (list_of ?r_m_E' @ [(t_r, ta'_r)]) σ''''"
unfolding mthr.if.RedT_def ..
with hb_completion
have hb_completion': "if.hb_completion σ'''' (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E') @ [(t_r, ta'_r)])))"
using ns'' by(rule if.hb_completion_shift)
from if.hb_completion_Runs[OF hb_completion' ta_hb_consistent_convert_RA]
obtain ttas' where Runs': "mthr.if.mthr.Runs σ'''' ttas'"
and hb': "ta_hb_consistent P (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E') @ [(t_r, ta'_r)]))) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas'))"
by blast
let ?E = "lappend (llist_of ?start_heap_obs) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend (ltake (enat r_m) E') (LCons (t_r, ta'_r) ttas'))))"
have ℰ: "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend (ltake (enat r_m) E') (LCons (t_r, ta'_r) ttas'))) ∈ mthr.if.ℰ ?start_state"
by(subst (4) llist_of_list_of[symmetric])(simp, blast intro: mthr.if.ℰ.intros mthr.if.mthr.Trsys_into_Runs σ_σ' mthr.if.mthr.Runs.Step red_ra' Runs')
hence ℰ': "?E ∈ ?ℰ" by blast
from ℰ have tsa: "thread_start_actions_ok ?E" by(rule thread_start_actions_ok_init_fin)
also let ?E' = "lappend (llist_of (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙))) (lappend (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙))) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas')))"
have "?E = ?E'"
using eq[symmetric]
by(simp add: lmap_lappend_distrib lappend_assoc lappend_llist_of_llist_of[symmetric] lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def split_def del: lmap_llist_of)(simp add: lappend_assoc[symmetric] lmap_lappend_distrib[symmetric] map_append[symmetric] lappend_llist_of_llist_of del: map_append)
finally have tsa': "thread_start_actions_ok ?E'" .
from hb hb' eq[symmetric]
have HB: "ta_hb_consistent P (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) (lappend (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙))) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas')))"
by -(rule ta_hb_consistent_lappendI, simp_all add: take_map[symmetric] drop_map[symmetric])
define EE where "EE = llist_of (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙))"
from r r_conv have r_conv': "r = (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + r_n + length ?start_heap_obs" by auto
hence len_EE: "llength EE = enat r" using r_m r_n
by(auto simp add: EE_def length_concat sum_list_sum_nth atLeast0LessThan lnth_ltake less_min_eq1 split_def min_def length_list_of_conv_the_enat cong: sum.cong_simp)
from r_conv r_m
have r_conv3: "llength (lconcat (lmap (λx. llist_of (map (Pair (fst x)) ⦃snd x⦄⇘o⇙)) (ltake (enat r_m) E'))) = enat (r - Suc (length start_heap_obs) - r_n)"
apply(simp add: llength_lconcat_lfinite_conv_sum lnth_ltake cong: sum.cong_simp conj_cong)
apply(auto simp add: sum_comp_morphism[where h=enat, symmetric] zero_enat_def less_trans[where y="enat r_m"] intro: sum.cong)
done
have is_ws: "is_write_seen P EE ws"
proof(rule is_write_seenI)
fix a ad al v
assume a: "a ∈ read_actions EE"
and a_obs: "action_obs EE a = NormalAction (ReadMem ad al v)"
from a have a_r: "a < r" by cases(simp add: len_EE actions_def)
from r E'_r_m r_m r_n r_conv3
have eq: "ltake (enat r) EE = ltake (enat r) E"
unfolding E E' EE_def
apply(subst (2) E'_unfold)
apply(simp add: ltake_lappend2 lappend_llist_of_llist_of[symmetric] lappend_eq_lappend_conv lmap_lappend_distrib lconcat_llist_of[symmetric] o_def split_def lmap_llist_of[symmetric] del: lappend_llist_of_llist_of lmap_llist_of)
apply(subst ltake_lappend1)
defer
apply(simp add: ltake_lmap[symmetric] take_map[symmetric] ltake_llist_of[symmetric] del: ltake_lmap ltake_llist_of)
apply(auto simp add: min_def)
done
hence sim: "ltake (enat r) EE [≈] ltake (enat r) E" by(rule eq_into_sim_actions)
from a sim have a': "a ∈ read_actions E"
by(rule read_actions_change_prefix)(simp add: a_r)
from action_obs_change_prefix_eq[OF eq, of a] a_r a_obs
have a_obs': "action_obs E a = NormalAction (ReadMem ad al v)" by simp
have a_mrw: "P,E ⊢ a ↝mrw ws a" using a_r a' by(rule mrw)
with ‹E ∈ ?ℰ› wf_exec have ws_a_a: "ws a < a"
by(rule jmm.mrw_before)(auto intro: a_r less_trans mrw)
hence [simp]: "ws a < r" using a_r by simp
from wf_exec have ws: "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
from is_write_seenD[OF this a' a_obs']
have "ws a ∈ write_actions E"
and "(ad, al) ∈ action_loc P E (ws a)"
and "value_written P E (ws a) (ad, al) = v"
and "¬ P,E ⊢ a ≤hb ws a"
and "is_volatile P al ⟹ ¬ P,E ⊢ a ≤so ws a"
and between: "⋀a'. ⟦ a' ∈ write_actions E; (ad, al) ∈ action_loc P E a';
P,E ⊢ ws a ≤hb a' ∧ P,E ⊢ a' ≤hb a ∨ is_volatile P al ∧ P,E ⊢ ws a ≤so a' ∧ P,E ⊢ a' ≤so a ⟧
⟹ a' = ws a" by simp_all
from ‹ws a ∈ write_actions E› sim[symmetric]
show "ws a ∈ write_actions EE" by(rule write_actions_change_prefix) simp
from action_loc_change_prefix[OF sim, of "ws a" P] ‹(ad, al) ∈ action_loc P E (ws a)›
show "(ad, al) ∈ action_loc P EE (ws a)" by(simp)
from value_written_change_prefix[OF eq, of "ws a" P] ‹value_written P E (ws a) (ad, al) = v›
show "value_written P EE (ws a) (ad, al) = v" by simp
from wf_exec have tsa_E: "thread_start_actions_ok E"
by(rule wf_exec_thread_start_actions_okD)
from ‹¬ P,E ⊢ a ≤hb ws a› show "¬ P,EE ⊢ a ≤hb ws a"
proof(rule contrapos_nn)
assume "P,EE ⊢ a ≤hb ws a"
thus "P,E ⊢ a ≤hb ws a" using tsa_E sim
by(rule happens_before_change_prefix)(simp_all add: a_r)
qed
{ assume "is_volatile P al"
hence "¬ P,E ⊢ a ≤so ws a" by fact
thus "¬ P,EE ⊢ a ≤so ws a"
by(rule contrapos_nn)(rule sync_order_change_prefix[OF _ sim], simp_all add: a_r) }
fix a'
assume "a' ∈ write_actions EE" "(ad, al) ∈ action_loc P EE a'"
moreover
hence [simp]: "a' < r" by cases(simp add: actions_def len_EE)
ultimately have a': "a' ∈ write_actions E" "(ad, al) ∈ action_loc P E a'"
using sim action_loc_change_prefix[OF sim, of a' P]
by(auto intro: write_actions_change_prefix)
{ assume "P,EE ⊢ ws a ≤hb a'" "P,EE ⊢ a' ≤hb a"
hence "P,E ⊢ ws a ≤hb a'" "P,E ⊢ a' ≤hb a"
using tsa_E sim a_r by(auto elim!: happens_before_change_prefix)
with between[OF a'] show "a' = ws a" by simp }
{ assume "is_volatile P al " "P,EE ⊢ ws a ≤so a'" "P,EE ⊢ a' ≤so a"
with sim a_r between[OF a'] show "a' = ws a"
by(fastforce elim: sync_order_change_prefix intro!: disjI2 del: disjCI) }
qed
with HB tsa'
have "∃ws'. P ⊢ (?E', ws') √ ∧
(∀n. n ∈ read_actions ?E' ⟶ length (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) ≤ n ⟶ P,?E' ⊢ ws' n ≤hb n) ∧
(∀n<length (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)). ws' n = ws n)"
unfolding EE_def
by(rule ta_hb_consistent_Read_hb)(rule jmm.ℰ_new_actions_for_fun[OF ℰ'[unfolded ‹?E = ?E'›]])
also have r_conv'': "length (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) = r"
using r_n r_m unfolding r_conv'
by(auto simp add: length_concat sum_list_sum_nth atLeast0LessThan lnth_ltake split_def o_def less_min_eq1 min_def length_list_of_conv_the_enat cong: sum.cong_simp)
finally obtain ws' where wf_exec': "P ⊢ (?E', ws') √"
and read_hb: "⋀n. ⟦ n ∈ read_actions ?E'; r ≤ n ⟧ ⟹ P,?E' ⊢ ws' n ≤hb n"
and read_same: "⋀n. n < r ⟹ ws' n = ws n" by blast
have "?same ?E'"
apply(subst ltake_lappend1, simp add: r_conv''[symmetric] length_list_of_conv_the_enat)
unfolding E E' lappend_llist_of_llist_of[symmetric]
apply(subst (1 2) ltake_lappend2, simp add: r[simplified])
apply(subst lappend_eq_lappend_conv, simp)
apply safe
apply(subst E'_unfold)
unfolding lmap_lappend_distrib
apply(subst lconcat_lappend, simp)
apply(subst lconcat_llist_of[symmetric])
apply(subst (3) lmap_llist_of[symmetric])
apply(subst (3) lmap_llist_of[symmetric])
apply(subst llist.map_comp)
apply(simp only: split_def o_def)
apply(subst llist_of_list_of, simp)
apply(subst (1 2) ltake_lappend2, simp add: r_conv3)
apply(subst lappend_eq_lappend_conv, simp)
apply safe
unfolding llist.map(2) lconcat_LCons E'_r_m snd_conv fst_conv take_map
apply(subst ltake_lappend1)
defer
apply(subst append_take_drop_id[where xs="⦃ta_r⦄⇘o⇙" and n=r_n, symmetric])
unfolding map_append lappend_llist_of_llist_of[symmetric]
apply(subst ltake_lappend1)
using r_n
apply(simp add: min_def r_conv3)
apply(rule refl)
apply(simp add: r_conv3)
using r_n by arith
moreover {
fix a
assume "a ∈ read_actions ?E'"
with read_hb[of a] read_same[of a]
have "if a < r then ws' a = ws a else P,?E' ⊢ ws' a ≤hb a" by simp }
hence "?read ?E' ws'" by blast
moreover from r_m r_n r_n'
have E'_r: "lnth ?E' r = (t_r, ⦃ta'_r⦄⇘o⇙ ! r_n)" unfolding r_conv'
by(auto simp add: lnth_lappend nth_append length_concat sum_list_sum_nth atLeast0LessThan split_beta lnth_ltake less_min_eq1 length_list_of_conv_the_enat cong: sum.cong_simp)
from E_r r have E_r: "lnth E r = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)"
unfolding E by(simp add: lnth_lappend)
have "r ∈ read_actions E ⟷ (∃ad al v. ⦃ta_r⦄⇘o⇙ ! r_n = NormalAction (ReadMem ad al v))" using True
by(auto elim!: read_actions.cases simp add: action_obs_def E_r actions_def intro!: read_actions.intros)
with sim E'_r E_r have "?tid ?E'" "?obs ?E'"
by(auto simp add: action_tid_def action_obs_def)
moreover have "?actions ?E'" using r_n r_m r_n' unfolding r_conv'
by(cases "llength ?E'")(auto simp add: actions_def less_min_eq2 length_concat sum_list_sum_nth atLeast0LessThan split_beta lnth_ltake less_min_eq1 length_list_of_conv_the_enat enat_plus_eq_enat_conv cong: sum.cong_simp)
ultimately show ?thesis using wf_exec' ℰ'
unfolding ‹?E = ?E'› by blast
qed
qed
qed
qed
end
lemma w_value_mrw_value_conf:
assumes "set_option (vs' adal) ⊆ vs adal × UNIV"
shows "set_option (mrw_value P vs' ob adal) ⊆ w_value P vs ob adal × UNIV"
using assms by(cases adal)(cases ob rule: w_value_cases, auto)
lemma w_values_mrw_values_conf:
assumes "set_option (vs' adal) ⊆ vs adal × UNIV"
shows "set_option (mrw_values P vs' obs adal) ⊆ w_values P vs obs adal × UNIV"
using assms
by(induct obs arbitrary: vs' vs)(auto del: subsetI intro: w_value_mrw_value_conf)
lemma w_value_mrw_value_dom_eq_preserve:
assumes "dom vs' = {adal. vs adal ≠ {}}"
shows "dom (mrw_value P vs' ob) = {adal. w_value P vs ob adal ≠ {}}"
using assms
apply(cases ob rule: w_value_cases)
apply(simp_all add: dom_def split_beta del: not_None_eq)
apply(blast elim: equalityE dest: subsetD)+
done
lemma w_values_mrw_values_dom_eq_preserve:
assumes "dom vs' = {adal. vs adal ≠ {}}"
shows "dom (mrw_values P vs' obs) = {adal. w_values P vs obs adal ≠ {}}"
using assms
by(induct obs arbitrary: vs vs')(auto del: equalityI intro: w_value_mrw_value_dom_eq_preserve)
context jmm_multithreaded begin
definition non_speculative_read ::
"nat ⇒ ('l, 'thread_id, 'x, 'm, 'w) state ⇒ ('addr × addr_loc ⇒ 'addr val set) ⇒ bool"
where
"non_speculative_read n s vs ⟷
(∀ttas s' t x ta x' m' i ad al v v'.
s -▹ttas→* s' ⟶ non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) ⟶
thr s' t = ⌊(x, no_wait_locks)⌋ ⟶ t ⊢ (x, shr s') -ta→ (x', m') ⟶ actions_ok s' t ta ⟶
i < length ⦃ta⦄⇘o⇙ ⟶
non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙)) ⟶
⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) ⟶
v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al) ⟶
(∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ ⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)))"
lemma non_speculative_readI [intro?]:
"(⋀ttas s' t x ta x' m' i ad al v v'.
⟦ s -▹ttas→* s'; non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)));
thr s' t = ⌊(x, no_wait_locks)⌋; t ⊢ (x, shr s') -ta→ (x', m'); actions_ok s' t ta;
i < length ⦃ta⦄⇘o⇙; non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙));
⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v);
v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al) ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ ⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙))
⟹ non_speculative_read n s vs"
unfolding non_speculative_read_def by blast
lemma non_speculative_readD:
"⟦ non_speculative_read n s vs; s -▹ttas→* s'; non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)));
thr s' t = ⌊(x, no_wait_locks)⌋; t ⊢ (x, shr s') -ta→ (x', m'); actions_ok s' t ta;
i < length ⦃ta⦄⇘o⇙; non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙));
⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v);
v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al) ⟧
⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ ⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)"
unfolding non_speculative_read_def by blast
end
subsection ‹@{term "non_speculative"} generalises @{term "cut_and_update"} and @{term "ta_hb_consistent"}›
context known_addrs_typing begin
lemma read_non_speculative_new_actions_for:
fixes status f C M params E
defines "E ≡ lift_start_obs start_tid start_heap_obs"
and "vs ≡ w_values P (λ_. {}) (map snd E)"
and "s ≡ init_fin_lift_state status (start_state f P C M params)"
assumes wf: "wf_syscls P"
and RedT: "mthr.if.RedT s ttas s'"
and redT: "mthr.if.redT s' (t, ta') s''"
and read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta'⦄⇘o⇙"
and ns: "non_speculative P (λ_. {}) (llist_of (map snd E @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) params) ⊆ allocated start_heap"
and wt: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and type_adal: "P,shr s' ⊢ ad@al : T"
shows "∃w. w ∈ new_actions_for P (llist_of (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))) (ad, al)"
(is "∃w. ?new_w w")
using RedT redT read ns[unfolded E_def] ka unfolding s_def
proof(cases rule: read_ex_NewHeapElem)
case (start CTn)
then obtain n where n: "start_heap_obs ! n = NewHeapElem ad CTn"
and len: "n < length start_heap_obs"
unfolding in_set_conv_nth by blast
from ns have "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
unfolding lappend_llist_of_llist_of[symmetric]
by(simp add: non_speculative_lappend del: lappend_llist_of_llist_of)
with RedT wt have hext: "start_heap ⊴ shr s'"
unfolding s_def E_def using start_state_vs_conf[OF wf]
by(auto dest!: init_fin_RedT_hext_incr simp add: start_state_def split_beta init_fin_lift_state_conv_simps)
from start have "typeof_addr start_heap ad = ⌊CTn⌋"
by(auto dest: NewHeapElem_start_heap_obsD[OF wf])
with hext have "typeof_addr (shr s') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
with type_adal have "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad CTn))" using n len
by cases (auto simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
with n len have "?new_w (Suc n)"
by(simp add: new_actions_for_def actions_def E_def action_obs_def lift_start_obs_def nth_append)
thus ?thesis ..
next
case (Red ttas' s'' t' ta' s''' ttas'' CTn)
note ttas = ‹ttas = ttas' @ (t', ta') # ttas''›
from ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
obtain obs obs' where obs: "⦃ta'⦄⇘o⇙ = obs @ NormalAction (NewHeapElem ad CTn) # obs'"
by(auto dest: split_list)
let ?n = "length (lift_start_obs start_tid start_heap_obs)"
let ?wa = "?n + length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs"
have "?wa = ?n + length (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas')) + length obs"
by(simp add: length_concat o_def split_def)
also have "… < length (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))"
using obs ttas by(simp add: E_def)
also
from ttas obs
have "(E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas)) ! ?wa = (t', NormalAction (NewHeapElem ad CTn))"
by(auto simp add: E_def lift_start_obs_def nth_append o_def split_def length_concat)
moreover
from ‹mthr.if.redT s'' (t', ta') s'''› ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
obtain x_wa x_wa' where ts''t': "thr s'' t' = ⌊(x_wa, no_wait_locks)⌋"
and red_wa: "mthr.init_fin t' (x_wa, shr s'') ta' (x_wa', shr s''')"
by(cases) fastforce+
from start_state_vs_conf[OF wf]
have vs: "vs_conf P (shr s) vs" unfolding vs_def E_def s_def
by(simp add: init_fin_lift_state_conv_simps start_state_def split_def)
from ns
have ns: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
and ns': "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) (llist_of ⦃ta'⦄⇘o⇙)"
and ns'': "non_speculative P (w_values P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'')))"
unfolding ttas vs_def
by(simp_all add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
from ‹mthr.if.RedT (init_fin_lift_state status (start_state f P C M params)) ttas' s''› wt ns
have ts_ok'': "ts_ok (init_fin_lift wfx) (thr s'') (shr s'')" using vs unfolding vs_def s_def
by(rule if_RedT_non_speculative_invar)
with ts''t' have wfxt': "wfx t' (snd x_wa) (shr s'')" by(cases x_wa)(auto dest: ts_okD)
from ‹mthr.if.RedT (init_fin_lift_state status (start_state f P C M params)) ttas' s''› wt ns
have vs'': "vs_conf P (shr s'') (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
unfolding s_def E_def vs_def
by(rule if_RedT_non_speculative_invar)(simp add: start_state_def split_beta init_fin_lift_state_conv_simps start_state_vs_conf[OF wf])
from if_redT_non_speculative_vs_conf[OF ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' _ vs'', of "length ⦃ta'⦄⇘o⇙"] ns'
have vs''': "vs_conf P (shr s''') (w_values P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙)"
by(simp add: vs_def)
from ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' ns' vs''
have "ts_ok (init_fin_lift wfx) (thr s''') (shr s''')"
unfolding vs_def by(rule if_redT_non_speculative_invar)
with ‹mthr.if.RedT s''' ttas'' s'›
have hext: "shr s''' ⊴ shr s'" using ns'' vs'''
by(rule init_fin_RedT_hext_incr)
from red_wa have "typeof_addr (shr s''') ad = ⌊CTn⌋"
using wfxt' ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙› by cases(auto dest: red_NewHeapElemD)
with hext have "typeof_addr (shr s') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
with type_adal have "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad CTn))" by cases auto
ultimately have "?new_w ?wa"
by(simp add: new_actions_for_def actions_def action_obs_def)
thus ?thesis ..
qed
lemma non_speculative_read_into_cut_and_update:
fixes status f C M params E
defines "E ≡ lift_start_obs start_tid start_heap_obs"
and "vs ≡ w_values P (λ_. {}) (map snd E)"
and "s ≡ init_fin_lift_state status (start_state f P C M params)"
and "vs' ≡ mrw_values P Map.empty (map snd E)"
assumes wf: "wf_syscls P"
and nsr: "if.non_speculative_read n s vs"
and wt: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) params) ⊆ allocated start_heap"
shows "if.cut_and_update s vs'"
proof(rule if.cut_and_updateI)
fix ttas s' t x ta x' m'
assume Red: "mthr.if.RedT s ttas s'"
and sc: "ta_seq_consist P vs' (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and tst: "thr s' t = ⌊(x, no_wait_locks)⌋"
and red: "t ⊢ (x, shr s') -ta→i (x', m')"
and aok: "mthr.if.actions_ok s' t ta"
let ?vs = "w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))"
let ?vs' = "mrw_values P vs' (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))"
from start_state_vs_conf[OF wf]
have vs: "vs_conf P (shr s) vs" unfolding vs_def E_def s_def
by(simp add: init_fin_lift_state_conv_simps start_state_def split_def)
from sc have ns: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
by(rule ta_seq_consist_into_non_speculative)(auto simp add: vs'_def vs_def del: subsetI intro: w_values_mrw_values_conf)
from ns have ns': "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
unfolding lappend_llist_of_llist_of[symmetric] vs_def
by(simp add: non_speculative_lappend E_def non_speculative_start_heap_obs del: lappend_llist_of_llist_of)
have vs_vs'': "⋀adal. set_option (?vs' adal) ⊆ ?vs adal × UNIV"
by(rule w_values_mrw_values_conf)(auto simp add: vs'_def vs_def del: subsetI intro: w_values_mrw_values_conf)
from Red wt ns vs
have wt': "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
by(rule if_RedT_non_speculative_invar)
hence wtt: "init_fin_lift wfx t x (shr s')" using tst by(rule ts_okD)
{ fix i
have "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧
length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙) ∧
ta_seq_consist P ?vs' (llist_of (take i ⦃ta'⦄⇘o⇙)) ∧
eq_upto_seq_inconsist P (take i ⦃ta⦄⇘o⇙) (take i ⦃ta'⦄⇘o⇙) ?vs' ∧
(ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙)) ⟶ ta' = ta)"
proof(induct i)
case 0
show ?case using red aok
by(auto simp del: split_paired_Ex simp add: eq_upto_seq_inconsist_simps)
next
case (Suc i)
then obtain ta' x'' m''
where red': "t ⊢ (x, shr s') -ta'→i (x'', m'')"
and aok': "mthr.if.actions_ok s' t ta'"
and len: "length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)"
and sc': "ta_seq_consist P ?vs' (llist_of (take i ⦃ta'⦄⇘o⇙))"
and eusi: "eq_upto_seq_inconsist P (take i ⦃ta⦄⇘o⇙) (take i ⦃ta'⦄⇘o⇙) ?vs'"
and ta'_ta: "ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙)) ⟹ ta' = ta"
by blast
let ?vs'' = "mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙)"
show ?case
proof(cases "i < length ⦃ta'⦄⇘o⇙ ∧ ¬ ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta'⦄⇘o⇙)) ∧ ¬ ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta⦄⇘o⇙))")
case True
hence i: "i < length ⦃ta'⦄⇘o⇙" and "¬ ta_seq_consist P ?vs'' (LCons (⦃ta'⦄⇘o⇙ ! i) LNil)" using sc'
by(auto simp add: take_Suc_conv_app_nth lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend simp del: lappend_llist_of_llist_of)
then obtain ad al v where ta'_i: "⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v)"
by(auto split: action.split_asm obs_event.split_asm)
from ta'_i True have read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta'⦄⇘o⇙" by(auto simp add: in_set_conv_nth)
with red' have "ad ∈ known_addrs_if t x" by(rule if_red_read_knows_addr)
hence "ad ∈ if.known_addrs_state s'" using tst by(rule if.known_addrs_stateI)
moreover from init_fin_red_read_typeable[OF red' wtt read]
obtain T where type_adal: "P,shr s' ⊢ ad@al : T" ..
from redT_updWs_total[of t "wset s'" "⦃ta'⦄⇘w⇙"] red' tst aok'
obtain s'' where redT': "mthr.if.redT s' (t, ta') s''" by(auto dest!: mthr.if.redT.redT_normal)
with wf Red
have "∃w. w ∈ new_actions_for P (llist_of (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))) (ad, al)"
(is "∃w. ?new_w w")
using read ns' ka wt type_adal unfolding s_def E_def by(rule read_non_speculative_new_actions_for)
then obtain w where w: "?new_w w" ..
have "(ad, al) ∈ dom ?vs'"
proof(cases "w < length E")
case True
with w have "(ad, al) ∈ dom vs'" unfolding vs'_def new_actions_for_def
by(clarsimp)(erule mrw_values_new_actionD[rotated 1], auto simp del: split_paired_Ex simp add: set_conv_nth action_obs_def nth_append intro!: exI[where x=w])
also have "dom vs' ⊆ dom ?vs'" by(rule mrw_values_dom_mono)
finally show ?thesis .
next
case False
with w show ?thesis unfolding new_actions_for_def
apply(clarsimp)
apply(erule mrw_values_new_actionD[rotated 1])
apply(simp_all add: set_conv_nth action_obs_def nth_append actions_def)
apply(rule exI[where x="w - length E"])
apply(subst nth_map[where f=snd, symmetric])
apply(simp_all add: length_concat o_def split_def map_concat)
done
qed
hence "(ad, al) ∈ dom (mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙))"
by(rule subsetD[OF mrw_values_dom_mono])
then obtain v' b where v': "mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙) (ad, al) = ⌊(v', b)⌋" by auto
moreover from vs_vs''[of "(ad, al)"]
have "set_option (mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙) (ad, al)) ⊆ w_values P ?vs (take i ⦃ta'⦄⇘o⇙) (ad, al) × UNIV"
by(rule w_values_mrw_values_conf)
ultimately have "v' ∈ w_values P ?vs (take i ⦃ta'⦄⇘o⇙) (ad, al)" by simp
moreover from sc'
have "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta'⦄⇘o⇙))"
by(blast intro: ta_seq_consist_into_non_speculative vs_vs'' del: subsetI)
ultimately obtain ta'' x'' m''
where red'': "t ⊢ (x, shr s') -ta''→i (x'', m'')"
and aok'': "mthr.if.actions_ok s' t ta''"
and i': "i < length ⦃ta''⦄⇘o⇙"
and eq: "take i ⦃ta''⦄⇘o⇙ = take i ⦃ta'⦄⇘o⇙"
and ta''_i: "⦃ta''⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v')"
and len': "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta'⦄⇘o⇙)"
using if.non_speculative_readD[OF nsr Red ns tst red' aok' i _ ta'_i, of v'] by auto
from len' len have "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)" by simp
moreover have "ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta''⦄⇘o⇙))"
using eq sc' i' ta''_i v'
by(simp add: take_Suc_conv_app_nth lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend del: lappend_llist_of_llist_of)
moreover
have eusi': "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta''⦄⇘o⇙) ?vs'"
proof(cases "i < length ⦃ta⦄⇘o⇙")
case True
with i' i len eq eusi ta'_i ta''_i v' show ?thesis
by(auto simp add: take_Suc_conv_app_nth ta'_ta eq_upto_seq_inconsist_simps intro: eq_upto_seq_inconsist_appendI)
next
case False
with i ta'_ta have "¬ ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙))" by auto
then show ?thesis using False i' eq eusi
by(simp add: take_Suc_conv_app_nth eq_upto_seq_inconsist_append2)
qed
moreover {
assume "ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta⦄⇘o⇙))"
with True have "ta'' = ta" by simp }
ultimately show ?thesis using red'' aok'' True by blast
next
case False
hence "ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta⦄⇘o⇙)) ∨
length ⦃ta'⦄⇘o⇙ ≤ i ∨
ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta'⦄⇘o⇙))"
(is "?case1 ∨ ?case2 ∨ ?case3") by auto
thus ?thesis
proof(elim disjCE)
assume "?case1"
moreover
hence "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta⦄⇘o⇙) ?vs'"
by(rule ta_seq_consist_imp_eq_upto_seq_inconsist_refl)
ultimately show ?thesis using red aok by fastforce
next
assume "?case2" and "¬ ?case1"
have "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta'⦄⇘o⇙) ?vs'"
proof(cases "i < length ⦃ta⦄⇘o⇙")
case True
from ‹?case2› ‹¬ ?case1› have "¬ ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙))" by(auto simp add: ta'_ta)
hence "eq_upto_seq_inconsist P (take i ⦃ta⦄⇘o⇙ @ [⦃ta⦄⇘o⇙ ! i]) (take i ⦃ta'⦄⇘o⇙ @ []) ?vs'"
by(blast intro: eq_upto_seq_inconsist_appendI[OF eusi])
thus ?thesis using True ‹?case2› by(simp add: take_Suc_conv_app_nth)
next
case False with eusi ‹?case2› show ?thesis by simp
qed
with red' aok' len sc' eusi ‹?case2› ‹¬ ?case1›show ?thesis
by (fastforce simp add: take_all simp del: split_paired_Ex)
next
assume "?case3" and "¬ ?case1" and "¬ ?case2"
with len eusi ta'_ta
have "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta'⦄⇘o⇙) ?vs'"
by(cases "i < length ⦃ta⦄⇘o⇙")(auto simp add: take_Suc_conv_app_nth lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend intro: eq_upto_seq_inconsist_appendI eq_upto_seq_inconsist_append2 cong: action.case_cong obs_event.case_cong)
with red' aok' ‹?case3› len ‹¬ ?case1› show ?thesis by blast
qed
qed
qed }
from this[of "max n (length ⦃ta⦄⇘o⇙)"]
show "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧ ta_seq_consist P ?vs' (llist_of ⦃ta'⦄⇘o⇙) ∧ eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ ?vs'"
by(auto simp del: split_paired_Ex cong: conj_cong)
qed
lemma non_speculative_read_into_hb_completion:
fixes status f C M params E
defines "E ≡ lift_start_obs start_tid start_heap_obs"
and "vs ≡ w_values P (λ_. {}) (map snd E)"
and "s ≡ init_fin_lift_state status (start_state f P C M params)"
assumes wf: "wf_syscls P"
and nsr: "if.non_speculative_read n s vs"
and wt: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) params) ⊆ allocated start_heap"
shows "if.hb_completion s E"
proof
fix ttas s' t x ta x' m' i
assume Red: "mthr.if.RedT s ttas s'"
and ns: "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and tst: "thr s' t = ⌊(x, no_wait_locks)⌋"
and red: "t ⊢ (x, shr s') -ta→i (x', m')"
and aok: "mthr.if.actions_ok s' t ta"
and nsi: "non_speculative P (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙))"
let ?E = "E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas) @ map (Pair t) (take i ⦃ta⦄⇘o⇙)"
let ?vs = "w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))"
from ns have ns': "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
unfolding lappend_llist_of_llist_of[symmetric]
by(simp add: non_speculative_lappend E_def non_speculative_start_heap_obs del: lappend_llist_of_llist_of)
from start_state_vs_conf[OF wf]
have vs: "vs_conf P (shr s) vs" unfolding vs_def E_def s_def
by(simp add: init_fin_lift_state_conv_simps start_state_def split_def)
from Red wt ns vs
have wt': "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
unfolding vs_def by(rule if_RedT_non_speculative_invar)
hence wtt: "init_fin_lift wfx t x (shr s')" using tst by(rule ts_okD)
{ fix j
have "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧ length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙) ∧
take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
ta_hb_consistent P ?E (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙)))) ∧
(i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
proof(induct j)
case 0 from red aok show ?case by(fastforce simp del: split_paired_Ex)
next
case (Suc j)
then obtain ta' x'' m''
where red': "t ⊢ (x, shr s') -ta'→i (x'', m'')"
and aok': "mthr.if.actions_ok s' t ta'"
and len: "length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)"
and eq: "take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙"
and hb: "ta_hb_consistent P ?E (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙))))"
and len_i: "i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙"
and sim_i: "(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
by blast
show ?case
proof(cases "i + j < length ⦃ta'⦄⇘o⇙")
case False
with red' aok' len eq hb len_i sim_i show ?thesis by(fastforce simp del: split_paired_Ex)
next
case True
note j = this
show ?thesis
proof(cases "∃ad al v. ⦃ta'⦄⇘o⇙ ! (i + j) = NormalAction (ReadMem ad al v)")
case True
then obtain ad al v where ta'_j: "⦃ta'⦄⇘o⇙ ! (i + j) = NormalAction (ReadMem ad al v)" by blast
hence read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta'⦄⇘o⇙" using j by(auto simp add: in_set_conv_nth)
with red' have "ad ∈ known_addrs_if t x" by(rule if_red_read_knows_addr)
hence "ad ∈ if.known_addrs_state s'" using tst by(rule if.known_addrs_stateI)
from init_fin_red_read_typeable[OF red' wtt read] obtain T
where type_adal: "P,shr s' ⊢ ad@al : T" ..
from redT_updWs_total[of t "wset s'" "⦃ta'⦄⇘w⇙"] red' tst aok'
obtain s'' where redT': "mthr.if.redT s' (t, ta') s''" by(auto dest!: mthr.if.redT.redT_normal)
with wf Red
have "∃w. w ∈ new_actions_for P (llist_of (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))) (ad, al)"
(is "∃w. ?new_w w")
using read ns' ka wt type_adal unfolding s_def E_def
by(rule read_non_speculative_new_actions_for)
then obtain w where w: "?new_w w" ..
define E'' where "E'' = ?E @ map (Pair t) (take (Suc j) (drop i ⦃ta'⦄⇘o⇙))"
from Red redT' have "mthr.if.RedT s (ttas @ [(t, ta')]) s''" unfolding mthr.if.RedT_def ..
hence tsa: "thread_start_actions_ok (llist_of (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (ttas @ [(t, ta')]))))"
unfolding s_def by(rule thread_start_actions_ok_init_fin_RedT)
hence "thread_start_actions_ok (llist_of E'')" unfolding E_def[symmetric] E''_def
by(rule thread_start_actions_ok_prefix)(rule lprefix_llist_ofI, simp, metis append_take_drop_id eq map_append)
moreover from w have "w ∈ actions (llist_of E'')"
unfolding E''_def by(auto simp add: new_actions_for_def actions_def)
moreover have "length ?E + j ∈ actions (llist_of E'')" using j by(auto simp add: E''_def actions_def)
moreover from w have "is_new_action (action_obs (llist_of E'') w)"
by(auto simp add: new_actions_for_def action_obs_def actions_def nth_append E''_def)
moreover have "¬ is_new_action (action_obs (llist_of E'') (length ?E + j))"
using j ta'_j by(auto simp add: action_obs_def nth_append min_def E''_def)(subst (asm) nth_map, simp_all)
ultimately have hb_w: "P,llist_of E'' ⊢ w ≤hb length ?E + j"
by(rule happens_before_new_not_new)
define writes where
"writes = {w. P,llist_of E'' ⊢ w ≤hb length ?E + j ∧ w ∈ write_actions (llist_of E'') ∧
(ad, al) ∈ action_loc P (llist_of E'') w}"
define w' where "w' = Max_torder (action_order (llist_of E'')) writes"
have writes_actions: "writes ⊆ actions (llist_of E'')" unfolding writes_def actions_def
by(auto dest!: happens_before_into_action_order elim!: action_orderE simp add: actions_def)
also have "finite …" by(simp add: actions_def)
finally (finite_subset) have "finite writes" .
moreover from hb_w w have w_writes: "w ∈ writes"
by(auto 4 3 simp add: writes_def new_actions_for_def action_obs_def actions_def nth_append E''_def intro!: write_actions.intros elim!: is_new_action.cases)
hence "writes ≠ {}" by auto
with torder_action_order ‹finite writes›
have w'_writes: "w' ∈ writes" using writes_actions unfolding w'_def by(rule Max_torder_in_set)
moreover
{ fix w''
assume "w'' ∈ writes"
with torder_action_order ‹finite writes›
have "llist_of E'' ⊢ w'' ≤a w'" using writes_actions unfolding w'_def by(rule Max_torder_above) }
note w'_maximal = this
define v' where "v' = value_written P (llist_of E'') w' (ad, al)"
from nsi ta_hb_consistent_into_non_speculative[OF hb]
have nsi': "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take (i + j) ⦃ta'⦄⇘o⇙))"
unfolding take_add lappend_llist_of_llist_of[symmetric] non_speculative_lappend vs_def eq
by(simp add: non_speculative_lappend o_def map_concat split_def del: lappend_llist_of_llist_of)
from w'_writes have adal_w': "(ad, al) ∈ action_loc P (llist_of E'') w'" by(simp add: writes_def)
from w'_writes have "w' ∈ write_actions (llist_of E'')"
unfolding writes_def by blast
then obtain "is_write_action (action_obs (llist_of E'') w')"
and w'_actions: "w' ∈ actions (llist_of E'')" by cases
hence "v' ∈ w_values P (λ_. {}) (map snd E'') (ad, al)"
proof cases
case (NewHeapElem ad' CTn)
hence "NormalAction (NewHeapElem ad' CTn) ∈ set (map snd E'')"
using w'_actions unfolding in_set_conv_nth
by(auto simp add: actions_def action_obs_def cong: conj_cong)
moreover have "ad' = ad"
and "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad CTn))"
using adal_w' NewHeapElem by auto
ultimately show ?thesis using NewHeapElem unfolding v'_def
by(simp add: value_written.simps w_values_new_actionD)
next
case (WriteMem ad' al' v'')
hence "NormalAction (WriteMem ad' al' v'') ∈ set (map snd E'')"
using w'_actions unfolding in_set_conv_nth
by(auto simp add: actions_def action_obs_def cong: conj_cong)
moreover have "ad' = ad" "al' = al" using adal_w' WriteMem by auto
ultimately show ?thesis using WriteMem unfolding v'_def
by(simp add: value_written.simps w_values_WriteMemD)
qed
hence "v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take (i + j) ⦃ta'⦄⇘o⇙) (ad, al)"
using j ta'_j eq unfolding E''_def vs_def
by(simp add: o_def split_def map_concat take_add take_Suc_conv_app_nth)
from if.non_speculative_readD[OF nsr Red ns[folded vs_def] tst red' aok' j nsi' ta'_j this]
obtain ta'' x'' m''
where red'': "t ⊢ (x, shr s') -ta''→i (x'', m'')"
and aok'': "mthr.if.actions_ok s' t ta''"
and j': "i + j < length ⦃ta''⦄⇘o⇙"
and eq': "take (i + j) ⦃ta''⦄⇘o⇙ = take (i + j) ⦃ta'⦄⇘o⇙"
and ta''_j: "⦃ta''⦄⇘o⇙ ! (i + j) = NormalAction (ReadMem ad al v')"
and len': "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta'⦄⇘o⇙)" by blast
define EE where "EE = ?E @ map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙))"
define E' where "E' = ?E @ map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙)) @ [(t, NormalAction (ReadMem ad al v'))]"
from len' len have "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)" by simp
moreover from eq' eq j j' have "take i ⦃ta''⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙"
by(auto simp add: take_add min_def)
moreover {
note hb
also have eq'': "take j (drop i ⦃ta'⦄⇘o⇙) = take j (drop i ⦃ta''⦄⇘o⇙)"
using eq' j j' by(simp add: take_add min_def)
also have "ta_hb_consistent P (?E @ list_of (llist_of (map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙))))) (llist_of [(t, ⦃ta''⦄⇘o⇙ ! (i + j))])"
unfolding llist_of.simps ta_hb_consistent_LCons ta_hb_consistent_LNil ta''_j prod.simps action.simps obs_event.simps list_of_llist_of append_assoc E'_def[symmetric, unfolded append_assoc]
unfolding EE_def[symmetric, unfolded append_assoc]
proof(intro conjI TrueI exI[where x=w'] strip)
have "llist_of E'' [≈] llist_of E'" using j len eq'' ta'_j unfolding E''_def E'_def
by(auto simp add: sim_actions_def list_all2_append List.list_all2_refl split_beta take_Suc_conv_app_nth take_map[symmetric])
moreover have "length E'' = length E'" using j j' by(simp add: E''_def E'_def)
ultimately have sim: "ltake (enat (length E')) (llist_of E'') [≈] ltake (enat (length E')) (llist_of E')" by simp
from w'_actions ‹length E'' = length E'›
have w'_len: "w' < length E'" by(simp add: actions_def)
from ‹w' ∈ write_actions (llist_of E'')› sim
show "w' ∈ write_actions (llist_of E')" by(rule write_actions_change_prefix)(simp add: w'_len)
from adal_w' action_loc_change_prefix[OF sim, of w' P]
show "(ad, al) ∈ action_loc P (llist_of E') w'" by(simp add: w'_len)
from ta'_j j have "length ?E + j ∈ read_actions (llist_of E'')"
by(auto intro!: read_actions.intros simp add: action_obs_def actions_def E''_def min_def nth_append)(auto)
hence "w' ≠ length ?E + j" using ‹w' ∈ write_actions (llist_of E'')›
by(auto dest: read_actions_not_write_actions)
with w'_len have "w' < length ?E + j" by(simp add: E'_def)
from j j' len' eq''
have "ltake (enat (length ?E + j)) (llist_of E'') = ltake (enat (length ?E + j)) (llist_of E')"
by(auto simp add: E''_def E'_def min_def take_Suc_conv_app_nth)
from value_written_change_prefix[OF this, of w' P] ‹w' < length ?E + j›
show "value_written P (llist_of E') w' (ad, al) = v'" unfolding v'_def by simp
from ‹thread_start_actions_ok (llist_of E'')› ‹llist_of E'' [≈] llist_of E'›
have tsa'': "thread_start_actions_ok (llist_of E')"
by(rule thread_start_actions_ok_change)
from w'_writes j j' len len' have "P,llist_of E'' ⊢ w' ≤hb length EE"
by(auto simp add: EE_def writes_def min_def ac_simps)
thus "P,llist_of E' ⊢ w' ≤hb length EE" using tsa'' sim
by(rule happens_before_change_prefix)(simp add: w'_len, simp add: EE_def E'_def)
fix w''
assume w'': "w'' ∈ write_actions (llist_of E')"
and adal_w'': "(ad, al) ∈ action_loc P (llist_of E') w''"
from w'' have w''_len: "w'' < length E'" by(cases)(simp add: actions_def)
from w'' sim[symmetric] have w'': "w'' ∈ write_actions (llist_of E'')"
by(rule write_actions_change_prefix)(simp add: w''_len)
from adal_w'' action_loc_change_prefix[OF sim[symmetric], of w'' P] w''_len
have adal_w'': "(ad, al) ∈ action_loc P (llist_of E'') w''" by simp
{
presume w'_w'': "llist_of E' ⊢ w' ≤a w''"
and w''_hb: "P,llist_of E' ⊢ w'' ≤hb length EE"
from w''_hb ‹thread_start_actions_ok (llist_of E'')› sim[symmetric]
have "P,llist_of E'' ⊢ w'' ≤hb length EE"
by(rule happens_before_change_prefix)(simp add: w''_len, simp add: E'_def EE_def)
with w'' adal_w'' j j' len len' have "w'' ∈ writes"
by(auto simp add: writes_def EE_def min_def ac_simps split: if_split_asm)
hence "llist_of E'' ⊢ w'' ≤a w'" by(rule w'_maximal)
hence "llist_of E' ⊢ w'' ≤a w'" using sim
by(rule action_order_change_prefix)(simp_all add: w'_len w''_len)
thus "w'' = w'" "w'' = w'" using w'_w'' by(rule antisymPD[OF antisym_action_order])+
}
{ assume "P,llist_of E' ⊢ w' ≤hb w'' ∧ P,llist_of E' ⊢ w'' ≤hb length EE"
thus "llist_of E' ⊢ w' ≤a w''" "P,llist_of E' ⊢ w'' ≤hb length EE"
by(blast dest: happens_before_into_action_order)+ }
{ assume "is_volatile P al ∧ P,llist_of E' ⊢ w' ≤so w'' ∧ P,llist_of E' ⊢ w'' ≤so length EE"
then obtain vol: "is_volatile P al"
and so: "P,llist_of E' ⊢ w' ≤so w''"
and so': "P,llist_of E' ⊢ w'' ≤so length EE" by blast
from so show "llist_of E' ⊢ w' ≤a w''" by(blast elim: sync_orderE)
show "P,llist_of E' ⊢ w'' ≤hb length EE"
proof(cases "is_new_action (action_obs (llist_of E') w'')")
case True
with ‹w'' ∈ write_actions (llist_of E')› ta''_j show ?thesis
by cases(rule happens_before_new_not_new[OF tsa''], auto simp add: actions_def EE_def E'_def action_obs_def min_def nth_append)
next
case False
with ‹w'' ∈ write_actions (llist_of E')› ‹(ad, al) ∈ action_loc P (llist_of E') w''›
obtain v'' where "action_obs (llist_of E') w'' = NormalAction (WriteMem ad al v'')"
by cases(auto elim: is_write_action.cases)
with ta''_j w'' j j' len len'
have "P ⊢ (action_tid (llist_of E') w'', action_obs (llist_of E') w'') ↝sw (action_tid (llist_of E') (length EE), action_obs (llist_of E') (length EE))"
by(auto simp add: E'_def EE_def action_obs_def min_def nth_append Volatile)
with so' have "P,llist_of E' ⊢ w'' ≤sw length EE" by(rule sync_withI)
thus ?thesis unfolding po_sw_def [abs_def] by(blast intro: tranclp.r_into_trancl)
qed }
qed
ultimately have "ta_hb_consistent P ?E (lappend (llist_of (map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙)))) (llist_of ([(t, ⦃ta''⦄⇘o⇙ ! (i + j))])))"
by(rule ta_hb_consistent_lappendI) simp
hence "ta_hb_consistent P ?E (llist_of (map (Pair t) (take (Suc j) (drop i ⦃ta''⦄⇘o⇙))))"
using j' unfolding lappend_llist_of_llist_of by(simp add: take_Suc_conv_app_nth) }
moreover from len_i have "i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta''⦄⇘o⇙" using eq' j' by auto
moreover from sim_i eq' ta''_j ta'_j
have "(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta''⦄⇘o⇙ ! i)"
by(cases "j = 0")(auto split: if_split_asm, (metis add_strict_left_mono add_0_right nth_take)+)
ultimately show ?thesis using red'' aok'' by blast
next
case False
hence "ta_hb_consistent P (?E @ list_of (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙))))) (llist_of [(t, ⦃ta'⦄⇘o⇙ ! (i + j))])"
by(simp add: ta_hb_consistent_LCons split: action.split obs_event.split)
with hb
have "ta_hb_consistent P ?E (lappend (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙)))) (llist_of ([(t, ⦃ta'⦄⇘o⇙ ! (i + j))])))"
by(rule ta_hb_consistent_lappendI) simp
hence "ta_hb_consistent P ?E (llist_of (map (Pair t) (take (Suc j) (drop i ⦃ta'⦄⇘o⇙))))"
using j unfolding lappend_llist_of_llist_of by(simp add: take_Suc_conv_app_nth)
with red' aok' len eq len_i sim_i show ?thesis by blast
qed
qed
qed }
from this[of "max n (length ⦃ta⦄⇘o⇙)"]
show "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧
take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
ta_hb_consistent P ?E (llist_of (map (Pair t) (drop i ⦃ta'⦄⇘o⇙))) ∧
(i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
by(simp del: split_paired_Ex cong: conj_cong split del: if_split) blast
qed
end
end