Theory BVProgressThreaded
section ‹Progress result for both of the multithreaded JVMs›
theory BVProgressThreaded
imports
"../Framework/FWProgress"
"../Framework/FWLTS"
BVNoTypeError
"../JVM/JVMThreaded"
begin
lemma (in JVM_heap_conf_base') mexec_eq_mexecd:
"⟦ wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t: (xcp, h, frs) √ ⟧ ⟹ mexec P t ((xcp, frs), h) = mexecd P t ((xcp, frs), h)"
apply(auto intro!: ext)
apply(unfold exec_1_iff)
apply(drule no_type_error)
apply(assumption)
apply(clarify)
apply(rule exec_1_d_NormalI)
apply(assumption)
apply(simp add: exec_d_def split: if_split_asm)
apply(erule jvmd_NormalE, auto)
done
context JVM_heap_conf_base begin
abbreviation
correct_state_ts :: "ty⇩P ⇒ ('addr,'thread_id,'addr jvm_thread_state) thread_info ⇒ 'heap ⇒ bool"
where
"correct_state_ts Φ ≡ ts_ok (λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √)"
lemma correct_state_ts_thread_conf:
"correct_state_ts Φ (thr s) (shr s) ⟹ thread_conf P (thr s) (shr s)"
by(erule ts_ok_mono)(auto simp add: correct_state_def)
lemma invoke_new_thread:
assumes "wf_jvm_prog⇘Φ⇙ P"
and "P ⊢ C sees M:Ts→T=⌊(mxs,mxl0,ins,xt)⌋ in C"
and "ins ! pc = Invoke Type.start 0"
and "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
and "Φ ⊢ t: (None, h, (stk, loc, C, M, pc) # frs) √"
and "typeof_addr h (thread_id2addr a) = ⌊Class_type D⌋"
and "P ⊢ D ≼⇧* Thread"
and "P ⊢ D sees run:[]→Void=⌊(mxs', mxl0', ins',xt')⌋ in D'"
shows "Φ ⊢ a: (None, h, [([], Addr (thread_id2addr a) # replicate mxl0' undefined_value, D', run, 0)]) √"
proof -
from ‹Φ ⊢ t: (None, h, (stk, loc, C, M, pc) # frs) √›
have "hconf h" and "preallocated h" by(simp_all add: correct_state_def)
moreover
from ‹P ⊢ D sees run:[]→Void=⌊(mxs', mxl0', ins',xt')⌋ in D'›
have "P ⊢ D' sees run:[]→Void=⌊(mxs', mxl0', ins',xt')⌋ in D'"
by(rule sees_method_idemp)
with ‹wf_jvm_prog⇘Φ⇙ P›
have "wt_start P D' [] mxl0' (Φ D' run)" and "ins' ≠ []"
by(auto dest: wt_jvm_prog_impl_wt_start)
then obtain LT' where LT': "Φ D' run ! 0 = Some ([], LT')"
by (clarsimp simp add: wt_start_def defs1 sup_state_opt_any_Some)
moreover
have "conf_f P h ([], LT') ins' ([], Addr (thread_id2addr a) # replicate mxl0' undefined_value, D', run, 0)"
proof -
let ?LT = "OK (Class D') # (replicate mxl0' Err)"
have "P,h ⊢ replicate mxl0' undefined_value [:≤⇩⊤] replicate mxl0' Err" by simp
also from ‹P ⊢ D sees run:[]→Void=⌊(mxs', mxl0', ins',xt')⌋ in D'›
have "P ⊢ D ≼⇧* D'" by(rule sees_method_decl_above)
with ‹typeof_addr h (thread_id2addr a) = ⌊Class_type D⌋›
have "P,h ⊢ Addr (thread_id2addr a) :≤ Class D'"
by(simp add: conf_def)
ultimately have "P,h ⊢ Addr (thread_id2addr a) # replicate mxl0' undefined_value [:≤⇩⊤] ?LT" by(simp)
also from ‹wt_start P D' [] mxl0' (Φ D' run)› LT'
have "P ⊢ … [≤⇩⊤] LT'" by(simp add: wt_start_def)
finally have "P,h ⊢ Addr (thread_id2addr a) # replicate mxl0' undefined_value [:≤⇩⊤] LT'" .
with ‹ins' ≠ []› show ?thesis by(simp add: conf_f_def)
qed
moreover from ‹typeof_addr h (thread_id2addr a) = ⌊Class_type D⌋› ‹P ⊢ D ≼⇧* Thread›
have "P,h ⊢ a √t" by(rule tconfI)
ultimately show ?thesis using ‹P ⊢ D' sees run:[]→Void=⌊(mxs', mxl0', ins',xt')⌋ in D'›
by(fastforce simp add: correct_state_def)
qed
lemma exec_new_threadE:
assumes "wf_jvm_prog⇘Φ⇙ P"
and "P,t ⊢ Normal σ -ta-jvmd→ Normal σ'"
and "Φ ⊢ t: σ √"
and "⦃ta⦄⇘t⇙ ≠ []"
obtains h frs a stk loc C M pc Ts T mxs mxl0 ins xt M' n Ta ta' va Us Us' U m' D'
where "σ = (None, h, (stk, loc, C, M, pc) # frs)"
and "(ta, σ') ∈ exec P t (None, h, (stk, loc, C, M, pc) # frs)"
and "P ⊢ C sees M: Ts→T = ⌊(mxs, mxl0, ins, xt)⌋ in C"
and "stk ! n = Addr a"
and "ins ! pc = Invoke M' n"
and "n < length stk"
and "typeof_addr h a = ⌊Ta⌋"
and "is_native P Ta M'"
and "ta = extTA2JVM P ta'"
and "σ' = extRet2JVM n m' stk loc C M pc frs va"
and "(ta', va, m') ∈ red_external_aggr P t a M' (rev (take n stk)) h"
and "map typeof⇘h⇙ (rev (take n stk)) = map Some Us"
and "P ⊢ class_type_of Ta sees M':Us'→U = Native in D'"
and "D'∙M'(Us') :: U"
and "P ⊢ Us [≤] Us'"
proof -
from ‹P,t ⊢ Normal σ -ta-jvmd→ Normal σ'› obtain h f Frs xcp
where check: "check P σ"
and exec: "(ta, σ') ∈ exec P t σ"
and [simp]: "σ = (xcp, h, f # Frs)"
by(rule jvmd_NormalE)
obtain stk loc C M pc where [simp]: "f = (stk, loc, C, M, pc)"
by(cases f, blast)
from ‹⦃ta⦄⇘t⇙ ≠ []› exec have [simp]: "xcp = None" by(cases xcp) auto
from ‹Φ ⊢ t: σ √›
obtain Ts T mxs mxl0 ins xt ST LT
where "hconf h" "preallocated h"
and sees: "P ⊢ C sees M: Ts→T = ⌊(mxs, mxl0, ins, xt)⌋ in C"
and "Φ C M ! pc = ⌊(ST, LT)⌋"
and "conf_f P h (ST, LT) ins (stk, loc, C, M, pc)"
and "conf_fs P h Φ M (length Ts) T Frs"
by(fastforce simp add: correct_state_def)
from check ‹Φ C M ! pc = ⌊(ST, LT)⌋› sees
have checkins: "check_instr (ins ! pc) P h stk loc C M pc Frs"
by(clarsimp simp add: check_def)
from sees ‹⦃ta⦄⇘t⇙ ≠ []› exec obtain M' n where [simp]: "ins ! pc = Invoke M' n"
by(cases "ins ! pc", auto split: if_split_asm simp add: split_beta ta_upd_simps)
from ‹wf_jvm_prog⇘Φ⇙ P› obtain wfmd where wfp: "wf_prog wfmd P" by(auto dest: wt_jvm_progD)
from checkins have "n < length stk" "is_Ref (stk ! n)" by auto
moreover from exec sees ‹⦃ta⦄⇘t⇙ ≠ []› have "stk ! n ≠ Null" by auto
with ‹is_Ref (stk ! n)› obtain a where "stk ! n = Addr a"
by(auto simp add: is_Ref_def elim: is_AddrE)
moreover with checkins obtain Ta where Ta: "typeof_addr h a = ⌊Ta⌋" by(fastforce)
moreover with checkins exec sees ‹n < length stk› ‹⦃ta⦄⇘t⇙ ≠ []› ‹stk ! n = Addr a›
obtain Us Us' U D' where "map typeof⇘h⇙ (rev (take n stk)) = map Some Us"
and "P ⊢ class_type_of Ta sees M':Us'→U = Native in D'" and "D'∙M'(Us') :: U"
and "P ⊢ Us [≤] Us'"
by(auto simp add: confs_conv_map min_def split_beta has_method_def external_WT'_iff split: if_split_asm)
moreover with ‹typeof_addr h a = ⌊Ta⌋› ‹n < length stk› exec sees ‹stk ! n = Addr a›
obtain ta' va h' where "ta = extTA2JVM P ta'" "σ' = extRet2JVM n h' stk loc C M pc Frs va"
"(ta', va, h') ∈ red_external_aggr P t a M' (rev (take n stk)) h"
by(fastforce simp add: min_def)
ultimately show thesis using exec sees
by-(rule that, auto intro!: is_native.intros)
qed
end
context JVM_conf_read begin
lemma correct_state_new_thread:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and red: "P,t ⊢ Normal σ -ta-jvmd→ Normal σ'"
and cs: "Φ ⊢ t: σ √"
and nt: "NewThread t'' (xcp, frs) h'' ∈ set ⦃ta⦄⇘t⇙"
shows "Φ ⊢ t'': (xcp, h'', frs) √"
proof -
from wf obtain wt where wfp: "wf_prog wt P" by(blast dest: wt_jvm_progD)
from nt have "⦃ta⦄⇘t⇙ ≠ []" by auto
with wf red cs
obtain h Frs a stk loc C M pc Ts T mxs mxl0 ins xt M' n Ta ta' va h' Us Us' U D'
where [simp]: "σ = (None, h, (stk, loc, C, M, pc) # Frs)"
and exec: "(ta, σ') ∈ exec P t (None, h, (stk, loc, C, M, pc) # Frs)"
and sees: "P ⊢ C sees M: Ts→T = ⌊(mxs, mxl0, ins, xt)⌋ in C"
and [simp]: "stk ! n = Addr a"
and [simp]: "ins ! pc = Invoke M' n"
and n: "n < length stk"
and Ta: "typeof_addr h a = ⌊Ta⌋"
and iec: "is_native P Ta M'"
and ta: "ta = extTA2JVM P ta'"
and σ': "σ' = extRet2JVM n h' stk loc C M pc Frs va"
and rel: "(ta', va, h') ∈ red_external_aggr P t a M' (rev (take n stk)) h"
and Us: "map typeof⇘h⇙ (rev (take n stk)) = map Some Us"
and wtext: "P ⊢ class_type_of Ta sees M':Us'→U = Native in D'" "D'∙M'(Us') :: U"
and sub: "P ⊢ Us [≤] Us'"
by(rule exec_new_threadE)
from cs have hconf: "hconf h" and preh: "preallocated h"
and tconf: "P,h ⊢ t √t" by(auto simp add: correct_state_def)
from Ta Us wtext sub have wtext': "P,h ⊢ a∙M'(rev (take n stk)) : U"
by(auto intro!: external_WT'.intros)
from rel have red: "P,t ⊢ ⟨a∙M'(rev (take n stk)), h⟩ -ta'→ext ⟨va, h'⟩"
by(unfold WT_red_external_list_conv[OF wfp wtext' tconf])
from ta nt obtain D M'' a' where nt': "NewThread t'' (D, M'', a') h'' ∈ set ⦃ta'⦄⇘t⇙"
"(xcp, frs) = extNTA2JVM P (D, M'', a')" by auto
with red have [simp]: "h'' = h'" by-(rule red_ext_new_thread_heap)
from red_external_new_thread_sub_thread[OF red nt'(1)]
have h't'': "typeof_addr h' a' = ⌊Class_type D⌋" "P ⊢ D ≼⇧* Thread" and [simp]: "M'' = run" by auto
from red_external_new_thread_exists_thread_object[OF red nt'(1)]
have tconf': "P,h' ⊢ t'' √t" by(auto intro: tconfI)
from sub_Thread_sees_run[OF wfp ‹P ⊢ D ≼⇧* Thread›] obtain mxs' mxl0' ins' xt' D'
where seesrun: "P ⊢ D sees run: []→Void = ⌊(mxs', mxl0', ins', xt')⌋ in D'" by auto
with nt' ta nt have "xcp = None" "frs = [([],Addr a' # replicate mxl0' undefined_value,D',run,0)]"
by(auto simp add: extNTA2JVM_def split_beta)
moreover
have "Φ ⊢ t'': (None, h', [([], Addr a' # replicate mxl0' undefined_value, D', run, 0)]) √"
proof -
from red wtext' ‹hconf h› have "hconf h'"
by(rule external_call_hconf)
moreover from red have "h ⊴ h'" by(rule red_external_hext)
with preh have "preallocated h'" by(rule preallocated_hext)
moreover from seesrun
have seesrun': "P ⊢ D' sees run: []→Void = ⌊(mxs', mxl0', ins', xt')⌋ in D'"
by(rule sees_method_idemp)
moreover with ‹wf_jvm_prog⇘Φ⇙ P›
obtain "wt_start P D' [] mxl0' (Φ D' run)" "ins' ≠ []"
by (auto dest: wt_jvm_prog_impl_wt_start)
then obtain LT' where "Φ D' run ! 0 = Some ([], LT')"
by (clarsimp simp add: wt_start_def defs1 sup_state_opt_any_Some)
moreover
have "conf_f P h' ([], LT') ins' ([], Addr a' # replicate mxl0' undefined_value, D', run, 0)"
proof -
let ?LT = "OK (Class D') # (replicate mxl0' Err)"
from seesrun have "P ⊢ D ≼⇧* D'" by(rule sees_method_decl_above)
hence "P,h' ⊢ Addr a' # replicate mxl0' undefined_value [:≤⇩⊤] ?LT"
using h't'' by(simp add: conf_def)
also from ‹wt_start P D' [] mxl0' (Φ D' run)› ‹Φ D' run ! 0 = Some ([], LT')›
have "P ⊢ ?LT [≤⇩⊤] LT'" by(simp add: wt_start_def)
finally have "P,h' ⊢ Addr a' # replicate mxl0' undefined_value [:≤⇩⊤] LT'" .
with ‹ins' ≠ []› show ?thesis by(simp add: conf_f_def)
qed
ultimately show ?thesis using tconf' by(fastforce simp add: correct_state_def)
qed
ultimately show ?thesis by(clarsimp)
qed
lemma correct_state_heap_change:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and red: "P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs')"
and cs: "Φ ⊢ t: (xcp, h, frs) √"
and cs'': "Φ ⊢ t'': (xcp'', h, frs'') √"
shows "Φ ⊢ t'': (xcp'', h', frs'') √"
proof(cases xcp)
case None
from cs have "P,h ⊢ t √t" by(simp add: correct_state_def)
with red have "hext h h'" by (auto intro: exec_1_d_hext simp add: tconf_def)
from ‹wf_jvm_prog⇘Φ⇙ P› cs red have "Φ ⊢ t: (xcp', h', frs') √"
by(auto elim!: jvmd_NormalE intro: BV_correct_1 simp add: exec_1_iff)
from cs'' have "P,h ⊢ t'' √t" by(simp add: correct_state_def)
with ‹h ⊴ h'› have tconf': "P,h' ⊢ t'' √t" by-(rule tconf_hext_mono)
from ‹Φ ⊢ t: (xcp', h', frs') √›
have hconf': "hconf h'" "preallocated h'" by(simp_all add: correct_state_def)
show ?thesis
proof(cases frs'')
case Nil thus ?thesis using tconf' hconf' by(simp add: correct_state_def)
next
case (Cons f'' Frs'')
obtain stk'' loc'' C0'' M0'' pc''
where "f'' = (stk'', loc'', C0'', M0'', pc'')"
by(cases f'', blast)
with ‹frs'' = f'' # Frs''› cs''
obtain Ts'' T'' mxs'' mxl⇩0'' ins'' xt'' ST'' LT''
where "hconf h"
and sees'': "P ⊢ C0'' sees M0'': Ts''→T'' = ⌊(mxs'', mxl⇩0'', ins'', xt'')⌋ in C0''"
and "Φ C0'' M0'' ! pc'' = ⌊(ST'', LT'')⌋"
and "conf_f P h (ST'', LT'') ins'' (stk'', loc'', C0'', M0'', pc'')"
and "conf_fs P h Φ M0'' (length Ts'') T'' Frs''"
by(fastforce simp add: correct_state_def)
show ?thesis using Cons ‹Φ ⊢ t'': (xcp'', h, frs'') √› ‹hext h h'› hconf' tconf'
apply(cases xcp'')
apply(auto simp add: correct_state_def)
apply(blast dest: hext_objD intro: conf_fs_hext conf_f_hext)+
done
qed
next
case (Some a)
with ‹P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs')›
have "h = h'" by(auto elim!: jvmd_NormalE)
with ‹Φ ⊢ t'': (xcp'', h, frs'') √› show ?thesis by simp
qed
lemma lifting_wf_correct_state_d:
"wf_jvm_prog⇘Φ⇙ P ⟹ lifting_wf JVM_final (mexecd P) (λt (xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √)"
by(unfold_locales)(auto intro: BV_correct_d_1 correct_state_new_thread correct_state_heap_change)
lemma lifting_wf_correct_state:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
shows "lifting_wf JVM_final (mexec P) (λt (xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √)"
proof(unfold_locales)
fix t x m ta x' m'
assume "mexec P t (x, m) ta (x', m')"
and "(λ(xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √) x m"
with wf show "(λ(xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √) x' m'"
by(cases x)(cases x', simp add: welltyped_commute[symmetric, OF ‹wf_jvm_prog⇘Φ⇙ P›], rule BV_correct_d_1)
next
fix t x m ta x' m' t'' x''
assume "mexec P t (x, m) ta (x', m')"
and "(λ(xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √) x m"
and "NewThread t'' x'' m' ∈ set ⦃ta⦄⇘t⇙"
with wf show "(λ(xcp, frs) h. Φ ⊢ t'': (xcp, h, frs) √) x'' m'"
apply(cases x, cases x', cases x'', clarify, unfold welltyped_commute[symmetric, OF ‹wf_jvm_prog⇘Φ⇙ P›])
by(rule correct_state_new_thread)
next
fix t x m ta x' m' t'' x''
assume "mexec P t (x, m) ta (x', m')"
and "(λ(xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √) x m"
and "(λ(xcp, frs) h. Φ ⊢ t'': (xcp, h, frs) √) x'' m"
with wf show "(λ(xcp, frs) h. Φ ⊢ t'': (xcp, h, frs) √) x'' m'"
by(cases x)(cases x', cases x'', clarify, unfold welltyped_commute[symmetric, OF ‹wf_jvm_prog⇘Φ⇙ P›], rule correct_state_heap_change)
qed
lemmas preserves_correct_state = FWLiftingSem.lifting_wf.RedT_preserves[OF lifting_wf_correct_state]
lemmas preserves_correct_state_d = FWLiftingSem.lifting_wf.RedT_preserves[OF lifting_wf_correct_state_d]
end
context JVM_heap_conf_base begin
definition correct_jvm_state :: "ty⇩P ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state set"
where
"correct_jvm_state Φ
= {s. correct_state_ts Φ (thr s) (shr s) ∧ lock_thread_ok (locks s) (thr s)}"
end
context JVM_heap_conf begin
lemma correct_jvm_state_initial:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and wf_start: "wf_start_state P C M vs"
shows "JVM_start_state P C M vs ∈ correct_jvm_state Φ"
proof -
from wf_start obtain Ts T m D
where "start_heap_ok" and "P ⊢ C sees M:Ts→T = ⌊m⌋ in D"
and "P,start_heap ⊢ vs [:≤] Ts" by cases
with wf BV_correct_initial[OF wf this] show ?thesis
by(cases m)(auto simp add: correct_jvm_state_def start_state_def JVM_start_state'_def intro: lock_thread_okI ts_okI split: if_split_asm)
qed
end
context JVM_conf_read begin
lemma invariant3p_correct_jvm_state_mexecdT:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
shows "invariant3p (mexecdT P) (correct_jvm_state Φ)"
unfolding correct_jvm_state_def
apply(rule invariant3pI)
apply safe
apply(erule (1) lifting_wf.redT_preserves[OF lifting_wf_correct_state_d[OF wf]])
apply(erule (1) execd_mthr.redT_preserves_lock_thread_ok)
done
lemma invariant3p_correct_jvm_state_mexecT:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
shows "invariant3p (mexecT P) (correct_jvm_state Φ)"
unfolding correct_jvm_state_def
apply(rule invariant3pI)
apply safe
apply(erule (1) lifting_wf.redT_preserves[OF lifting_wf_correct_state[OF wf]])
apply(erule (1) exec_mthr.redT_preserves_lock_thread_ok)
done
lemma correct_jvm_state_preserved:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and correct: "s ∈ correct_jvm_state Φ"
and red: "P ⊢ s -▹ttas→⇘jvm⇙* s'"
shows "s' ∈ correct_jvm_state Φ"
using wf red correct unfolding exec_mthr.RedT_def
by(rule invariant3p_rtrancl3p[OF invariant3p_correct_jvm_state_mexecT])
theorem jvm_typesafe:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and start: "wf_start_state P C M vs"
and exec: "P ⊢ JVM_start_state P C M vs -▹ttas→⇘jvm⇙* s'"
shows "s' ∈ correct_jvm_state Φ"
by(rule correct_jvm_state_preserved[OF wf _ exec])(rule correct_jvm_state_initial[OF wf start])
end
declare (in JVM_typesafe) split_paired_Ex [simp del]
context JVM_heap_conf_base' begin
lemma execd_NewThread_Thread_Object:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and conf: "Φ ⊢ t': σ √"
and red: "P,t' ⊢ Normal σ -ta-jvmd→ Normal σ'"
and nt: "NewThread t x m ∈ set ⦃ta⦄⇘t⇙"
shows "∃C. typeof_addr (fst (snd σ')) (thread_id2addr t) = ⌊Class_type C⌋ ∧ P ⊢ Class C ≤ Class Thread"
proof -
from wf obtain wfmd where wfp: "wf_prog wfmd P" by(blast dest: wt_jvm_progD)
from red obtain h f Frs xcp
where check: "check P σ"
and exec: "(ta, σ') ∈ exec P t' σ"
and [simp]: "σ = (xcp, h, f # Frs)"
by(rule jvmd_NormalE)
obtain xcp' h' frs' where [simp]: "σ' = (xcp', h', frs')" by(cases σ', auto)
obtain stk loc C M pc where [simp]: "f = (stk, loc, C, M, pc)" by(cases f, blast)
from exec nt have [simp]: "xcp = None" by(cases xcp, auto)
from ‹Φ ⊢ t': σ √› obtain Ts T mxs mxl0 ins xt ST LT
where "hconf h"
and "P,h ⊢ t' √t"
and sees: "P ⊢ C sees M: Ts→T = ⌊(mxs, mxl0, ins, xt)⌋ in C"
and "Φ C M ! pc = ⌊(ST, LT)⌋"
and "conf_f P h (ST, LT) ins (stk, loc, C, M, pc)"
and "conf_fs P h Φ M (length Ts) T Frs"
by(fastforce simp add: correct_state_def)
from wf red conf nt
obtain h frs a stk loc C M pc M' n ta' va h'
where ha: "typeof_addr h a ≠ None" and ta: "ta = extTA2JVM P ta'"
and σ': "σ' = extRet2JVM n h' stk loc C M pc frs va"
and rel: "(ta', va, h') ∈ red_external_aggr P t' a M' (rev (take n stk)) h"
by -(erule (2) exec_new_threadE, fastforce+)
from nt ta obtain x' where "NewThread t x' m ∈ set ⦃ta'⦄⇘t⇙" by auto
from red_external_aggr_new_thread_exists_thread_object[OF rel ha this] σ'
show ?thesis by(cases va) auto
qed
lemma mexecdT_NewThread_Thread_Object:
"⟦ wf_jvm_prog⇘Φ⇙ P; correct_state_ts Φ (thr s) (shr s); P ⊢ s -t'▹ta→⇘jvmd⇙ s'; NewThread t x m ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ ∃C. typeof_addr (shr s') (thread_id2addr t) = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread"
apply(frule correct_state_ts_thread_conf)
apply(erule execd_mthr.redT.cases)
apply(hypsubst)
apply(frule (2) execd_tconf.redT_updTs_preserves[where ln'="redT_updLns (locks s) t' no_wait_locks ⦃ta⦄⇘l⇙"])
apply clarsimp
apply(clarsimp)
apply(drule execd_NewThread_Thread_Object)
apply(drule (1) ts_okD)
apply(fastforce)
apply(assumption)
apply(fastforce)
apply(clarsimp)
apply(simp)
done
end
context JVM_heap begin
lemma exec_ta_satisfiable:
assumes "P,t ⊢ s -ta-jvm→ s'"
shows "∃s. exec_mthr.actions_ok s t ta"
proof -
obtain xcp h frs where [simp]: "s = (xcp, h, frs)" by(cases s)
from assms obtain stk loc C M pc frs' where [simp]: "frs = (stk, loc, C, M, pc) # frs'"
by(cases frs)(auto simp add: exec_1_iff)
show ?thesis
proof(cases xcp)
case Some with assms show ?thesis by(auto simp add: exec_1_iff lock_ok_las_def finfun_upd_apply split_paired_Ex)
next
case None
with assms show ?thesis
apply(cases "instrs_of P C M ! pc")
apply(auto simp add: exec_1_iff lock_ok_las_def finfun_upd_apply split_beta final_thread.actions_ok_iff split: if_split_asm dest: red_external_aggr_ta_satisfiable[where final=JVM_final])
apply(fastforce simp add: final_thread.actions_ok_iff lock_ok_las_def dest: red_external_aggr_ta_satisfiable[where final=JVM_final])
apply(fastforce simp add: finfun_upd_apply intro: exI[where x="K$ None"] exI[where x="K$ ⌊(t, 0)⌋"] may_lock.intros)+
done
qed
qed
end
context JVM_typesafe begin
lemma execd_wf_progress:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
shows "progress JVM_final (mexecd P) (execd_mthr.wset_Suspend_ok P (correct_jvm_state Φ))"
(is "progress _ _ ?wf_state")
proof
{
fix s t x ta x' m' w
assume mexecd: "mexecd P t (x, shr s) ta (x', m')"
and Suspend: "Suspend w ∈ set ⦃ta⦄⇘w⇙"
from mexecd_Suspend_Invoke[OF mexecd Suspend]
show "¬ JVM_final x'" by auto
}
note Suspend_final = this
{
fix s
assume s: "s ∈ ?wf_state"
hence "lock_thread_ok (locks s) (thr s)"
by(auto dest: execd_mthr.wset_Suspend_okD1 simp add: correct_jvm_state_def)
moreover
have "exec_mthr.wset_final_ok (wset s) (thr s)"
proof(rule exec_mthr.wset_final_okI)
fix t w
assume "wset s t = ⌊w⌋"
from execd_mthr.wset_Suspend_okD2[OF s this]
obtain x0 ta x m1 w' ln'' and s0 :: "('addr, 'thread_id, 'addr option × 'addr frame list, 'heap, 'addr) state"
where mexecd: "mexecd P t (x0, shr s0) ta (x, m1)"
and Suspend: "Suspend w' ∈ set ⦃ta⦄⇘w⇙"
and tst: "thr s t = ⌊(x, ln'')⌋" by blast
from Suspend_final[OF mexecd Suspend] tst
show " ∃x ln. thr s t = ⌊(x, ln)⌋ ∧ ¬ JVM_final x" by blast
qed
ultimately show "lock_thread_ok (locks s) (thr s) ∧ exec_mthr.wset_final_ok (wset s) (thr s)" ..
}
next
fix s t x ta x' m'
assume wfs: "s ∈ ?wf_state"
and "thr s t = ⌊(x, no_wait_locks)⌋"
and "mexecd P t (x, shr s) ta (x', m')"
and wait: "¬ waiting (wset s t)"
moreover obtain ls ts h ws "is" where s [simp]: "s = (ls, (ts, h), ws, is)" by(cases s) fastforce
ultimately have "ts t = ⌊(x, no_wait_locks)⌋" "mexecd P t (x, h) ta (x', m')" by auto
from wfs have "correct_state_ts Φ ts h" by(auto dest: execd_mthr.wset_Suspend_okD1 simp add: correct_jvm_state_def)
from wf obtain wfmd where wfp: "wf_prog wfmd P" by(auto dest: wt_jvm_progD)
from ‹ts t = ⌊(x, no_wait_locks)⌋› ‹mexecd P t (x, h) ta (x', m')›
obtain xcp frs xcp' frs'
where "P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', m', frs')"
and [simp]: "x = (xcp, frs)" "x' = (xcp', frs')"
by(cases x, auto)
then obtain f Frs
where check: "check P (xcp, h, f # Frs)"
and [simp]: "frs = f # Frs"
and exec: "(ta, xcp', m', frs') ∈ exec P t (xcp, h, f # Frs)"
by(auto elim: jvmd_NormalE)
with ‹ts t = ⌊(x, no_wait_locks)⌋› ‹correct_state_ts Φ ts h›
have correct: "Φ ⊢ t: (xcp, h, f # Frs) √" by(auto dest: ts_okD)
obtain stk loc C M pc where f [simp]: "f = (stk, loc, C, M, pc)" by (cases f)
from correct obtain Ts T mxs mxl0 ins xt ST LT
where hconf: "hconf h"
and tconf: "P, h ⊢ t √t"
and sees: "P ⊢ C sees M:Ts→T = ⌊(mxs, mxl0, ins, xt)⌋ in C"
and wt: "Φ C M ! pc = ⌊(ST, LT)⌋"
and conf_f: "conf_f P h (ST, LT) ins (stk, loc, C, M, pc)"
and confs: "conf_fs P h Φ M (length Ts) T Frs"
and confxcp: "conf_xcp P h xcp (ins ! pc)"
and preh: "preallocated h"
by(fastforce simp add: correct_state_def)
have "∃ta' σ'. P,t ⊢ Normal (xcp, h, (stk, loc, C, M, pc) # Frs) -ta'-jvmd→ Normal σ' ∧
(final_thread.actions_ok JVM_final (ls, (ts, h), ws, is) t ta' ∨
final_thread.actions_ok' (ls, (ts, h), ws, is) t ta' ∧ final_thread.actions_subset ta' ta)"
proof(cases "final_thread.actions_ok' (ls, (ts, h), ws, is) t ta")
case True
have "final_thread.actions_subset ta ta" ..
with True ‹P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', m', frs')›
show ?thesis by auto
next
case False
note naok = this
have ws: "wset s t = None ∨
(∃n a T w. ins ! pc = Invoke wait n ∧ stk ! n = Addr a ∧ typeof_addr h a = ⌊T⌋ ∧ is_native P T wait ∧ wset s t = ⌊PostWS w⌋ ∧ xcp = None)"
proof(cases "wset s t")
case None thus ?thesis ..
next
case (Some w)
from execd_mthr.wset_Suspend_okD2[OF wfs this] ‹ts t = ⌊(x, no_wait_locks)⌋›
obtain xcp0 frs0 h0 ta0 w' s1 tta1
where red0: "mexecd P t ((xcp0, frs0), h0) ta0 ((xcp, frs), shr s1)"
and Suspend: "Suspend w' ∈ set ⦃ta0⦄⇘w⇙"
and s1: "P ⊢ s1 -▹tta1→⇘jvmd⇙* s"
by auto
from mexecd_Suspend_Invoke[OF red0 Suspend] sees
obtain n a T where [simp]: "ins ! pc = Invoke wait n" "xcp = None" "stk ! n = Addr a"
and type: "typeof_addr h0 a = ⌊T⌋"
and iec: "is_native P T wait"
by(auto simp add: is_native.simps) blast
from red0 have "h0 ⊴ shr s1" by(auto dest: exec_1_d_hext)
also from s1 have "shr s1 ⊴ shr s" by(rule Execd_hext)
finally have "typeof_addr (shr s) a = ⌊T⌋" using type
by(rule typeof_addr_hext_mono)
moreover from Some wait s obtain w' where "ws t = ⌊PostWS w'⌋"
by(auto simp add: not_waiting_iff)
ultimately show ?thesis using iec s by auto
qed
from ws naok exec sees
show ?thesis
proof(cases "ins ! pc")
case (Invoke M' n)
from ws Invoke check exec sees naok obtain a Ts U Ta Us D D'
where a: "stk ! n = Addr a"
and n: "n < length stk"
and Ta: "typeof_addr h a = ⌊Ta⌋"
and wtext: "P ⊢ class_type_of Ta sees M':Us→U = Native in D'" "D'∙M'(Us)::U"
and sub: "P ⊢ Ts [≤] Us"
and Ts: "map typeof⇘h⇙ (rev (take n stk)) = map Some Ts"
and [simp]: "xcp = None"
apply(cases xcp)
apply(simp add: is_Ref_def has_method_def external_WT'_iff check_def lock_ok_las'_def confs_conv_map split_beta split: if_split_asm option.splits)
apply(auto simp add: lock_ok_las'_def)[2]
apply(fastforce simp add: is_native.simps lock_ok_las'_def dest: sees_method_fun)+
done
from exec Ta n a sees Invoke wtext obtain ta' va m''
where exec': "(ta', va, m'') ∈ red_external_aggr P t a M' (rev (take n stk)) h"
and ta: "ta = extTA2JVM P ta'"
and va: "(xcp', m', frs') = extRet2JVM n m'' stk loc C M pc Frs va"
by(auto)
from va have [simp]: "m'' = m'" by(cases va) simp_all
from Ta Ts wtext sub have wtext': "P,h ⊢ a∙M'(rev (take n stk)) : U"
by(auto intro!: external_WT'.intros simp add: is_native.simps)
with wfp exec' tconf have red: "P,t ⊢ ⟨a∙M'(rev (take n stk)), h⟩ -ta'→ext ⟨va, m'⟩"
by(simp add: WT_red_external_list_conv)
from ws Invoke have "wset s t = None ∨ M' = wait ∧ (∃w. wset s t = ⌊PostWS w⌋)" by auto
with wfp red tconf hconf obtain ta'' va' h''
where red': "P,t ⊢ ⟨a∙M'(rev (take n stk)),h⟩ -ta''→ext ⟨va',h''⟩"
and ok': "final_thread.actions_ok JVM_final s t ta'' ∨ final_thread.actions_ok' s t ta'' ∧ final_thread.actions_subset ta'' ta'"
by(rule red_external_wf_red)
from red' a n Ta Invoke sees wtext
have "(extTA2JVM P ta'', extRet2JVM n h'' stk loc C M pc Frs va') ∈ exec P t (xcp, h, f # Frs)"
by(auto intro: red_external_imp_red_external_aggr)
with check have "P,t ⊢ Normal (xcp, h, (stk, loc, C, M, pc) # Frs) -extTA2JVM P ta''-jvmd→ Normal (extRet2JVM n h'' stk loc C M pc Frs va')"
by -(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def)
moreover from ok' ta
have "final_thread.actions_ok JVM_final (ls, (ts, h), ws, is) t (extTA2JVM P ta'') ∨
final_thread.actions_ok' (ls, (ts, h), ws, is) t (extTA2JVM P ta'') ∧ final_thread.actions_subset (extTA2JVM P ta'') ta"
by(auto simp add: final_thread.actions_ok'_convert_extTA elim: final_thread.actions_subset.cases del: subsetI)
ultimately show ?thesis by blast
next
case MEnter
with exec sees naok ws have False
by(cases xcp)(auto split: if_split_asm simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
thus ?thesis ..
next
case MExit
with exec sees False check ws obtain a where [simp]: "hd stk = Addr a" "xcp = None" "ws t = None"
and ta: "ta = ⦃Unlock→a, SyncUnlock a⦄ ∨ ta = ⦃UnlockFail→a⦄"
by(cases xcp)(fastforce split: if_split_asm simp add: lock_ok_las'_def finfun_upd_apply is_Ref_def check_def)+
from ta show ?thesis
proof(rule disjE)
assume ta: "ta = ⦃Unlock→a, SyncUnlock a⦄"
let ?ta' = "⦃UnlockFail→a⦄"
from ta exec sees MExit obtain σ'
where "(?ta', σ') ∈ exec P t (xcp, h, f # Frs)" by auto
with check have "P,t ⊢ Normal (xcp, h, (stk, loc, C, M, pc) # Frs) -?ta'-jvmd→ Normal σ'"
by -(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def)
moreover from False ta have "has_locks (ls $ a) t = 0"
by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
hence "final_thread.actions_ok' (ls, (ts, h), ws, is) t ?ta'"
by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: final_thread.actions_subset_iff collect_locks'_def finfun_upd_apply ta_upd_simps)
ultimately show ?thesis by(fastforce simp add: ta_upd_simps)
next
assume ta: "ta = ⦃UnlockFail→a⦄"
let ?ta' = "⦃Unlock→a, SyncUnlock a⦄"
from ta exec sees MExit obtain σ'
where "(?ta', σ') ∈ exec P t (xcp, h, f # Frs)" by auto
with check have "P,t ⊢ Normal (xcp, h, (stk, loc, C, M, pc) # Frs) -?ta'-jvmd→ Normal σ'"
by -(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def)
moreover from False ta have "has_lock (ls $ a) t"
by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
hence "final_thread.actions_ok' (ls, (ts, h), ws, is) t ?ta'"
by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
moreover from ta have "final_thread.actions_subset ?ta' ta"
by(auto simp add: final_thread.actions_subset_iff collect_locks'_def finfun_upd_apply ta_upd_simps)
ultimately show ?thesis by(fastforce simp add: ta_upd_simps)
qed
qed(case_tac [!] xcp, auto simp add: split_beta lock_ok_las'_def split: if_split_asm)
qed
thus "∃ta' x' m'. mexecd P t (x, shr s) ta' (x', m') ∧
(final_thread.actions_ok JVM_final s t ta' ∨
final_thread.actions_ok' s t ta' ∧ final_thread.actions_subset ta' ta)"
by fastforce
next
fix s t x
assume wfs: "s ∈ ?wf_state"
and tst: "thr s t = ⌊(x, no_wait_locks)⌋"
and "¬ JVM_final x"
from wfs have correct: "correct_state_ts Φ (thr s) (shr s)"
by(auto dest: execd_mthr.wset_Suspend_okD1 simp add: correct_jvm_state_def)
obtain xcp frs where x: "x = (xcp, frs)" by (cases x, auto)
with ‹¬ JVM_final x› obtain f Frs where "frs = f # Frs"
by(fastforce simp add: neq_Nil_conv)
with tst correct x have "Φ ⊢ t: (xcp, shr s, f # Frs) √" by(auto dest: ts_okD)
with ‹wf_jvm_prog⇘Φ⇙ P›
have "exec_d P t (xcp, shr s, f # Frs) ≠ TypeError" by(auto dest: no_type_error)
then obtain Σ where "exec_d P t (xcp, shr s, f # Frs) = Normal Σ" by(auto)
hence "exec P t (xcp, shr s, f # Frs) = Σ"
by(auto simp add: exec_d_def check_def split: if_split_asm)
with progress[OF wf ‹Φ ⊢ t: (xcp, shr s, f # Frs) √›]
obtain ta σ where "(ta, σ) ∈ Σ" unfolding exec_1_iff by blast
with ‹x = (xcp, frs)› ‹frs = f # Frs› ‹Φ ⊢ t: (xcp, shr s, f # Frs) √›
‹wf_jvm_prog⇘Φ⇙ P› ‹exec_d P t (xcp, shr s, f # Frs) = Normal Σ›
show "∃ta x' m'. mexecd P t (x, shr s) ta (x', m')"
by(cases ta, cases σ)(fastforce simp add: split_paired_Ex intro: exec_1_d_NormalI)
qed(fastforce dest: defensive_imp_aggressive_1 mexec_instr_Wakeup_no_Join exec_ta_satisfiable)+
end
context JVM_conf_read begin
lemma mexecT_eq_mexecdT:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and cs: "correct_state_ts Φ (thr s) (shr s)"
shows "P ⊢ s -t▹ta→⇘jvm⇙ s' = P ⊢ s -t▹ta→⇘jvmd⇙ s'"
proof(rule iffI)
assume "P ⊢ s -t▹ta→⇘jvm⇙ s'"
thus "P ⊢ s -t▹ta→⇘jvmd⇙ s'"
proof(cases rule: exec_mthr.redT_elims[consumes 1, case_names normal acquire])
case (normal x x' m')
obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto)
from ‹thr s t = ⌊(x, no_wait_locks)⌋› cs
have "Φ ⊢ t: (xcp, shr s, frs) √" by(auto dest: ts_okD)
from mexec_eq_mexecd[OF wf ‹Φ ⊢ t: (xcp, shr s, frs) √›] ‹mexec P t (x, shr s) ta (x', m')›
have *: "mexecd P t (x, shr s) ta (x', m')" by simp
with lifting_wf.redT_updTs_preserves[OF lifting_wf_correct_state_d[OF wf] cs, OF this ‹thr s t = ⌊(x, no_wait_locks)⌋›] ‹thread_oks (thr s) ⦃ta⦄⇘t⇙›
have "correct_state_ts Φ ((redT_updTs (thr s) ⦃ta⦄⇘t⇙)(t ↦ (x', redT_updLns (locks s) t no_wait_locks ⦃ta⦄⇘l⇙))) m'" by simp
with * show ?thesis using normal
by(cases s')(erule execd_mthr.redT_normal, auto)
next
case acquire thus ?thesis
apply(cases s', clarify)
apply(rule execd_mthr.redT_acquire, assumption+)
by(auto)
qed
next
assume "P ⊢ s -t▹ta→⇘jvmd⇙ s'"
thus "P ⊢ s -t▹ta→⇘jvm⇙ s'"
proof(cases rule: execd_mthr.redT_elims[consumes 1, case_names normal acquire])
case (normal x x' m')
obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto)
from ‹thr s t = ⌊(x, no_wait_locks)⌋› cs
have "Φ ⊢ t: (xcp, shr s, frs) √" by(auto dest: ts_okD)
from mexec_eq_mexecd[OF wf ‹Φ ⊢ t: (xcp, shr s, frs) √›] ‹mexecd P t (x, shr s) ta (x', m')›
have "mexec P t (x, shr s) ta (x', m')" by simp
moreover from lifting_wf.redT_updTs_preserves[OF lifting_wf_correct_state_d[OF wf] cs, OF ‹mexecd P t (x, shr s) ta (x', m')› ‹thr s t = ⌊(x, no_wait_locks)⌋›] ‹thread_oks (thr s) ⦃ta⦄⇘t⇙›
have "correct_state_ts Φ ((redT_updTs (thr s) ⦃ta⦄⇘t⇙)(t ↦ (x', redT_updLns (locks s) t no_wait_locks ⦃ta⦄⇘l⇙))) m'" by simp
ultimately show ?thesis using normal
by(cases s')(erule exec_mthr.redT_normal, auto)
next
case acquire thus ?thesis
apply(cases s', clarify)
apply(rule exec_mthr.redT_acquire, assumption+)
by(auto)
qed
qed
lemma mExecT_eq_mExecdT:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and ct: "correct_state_ts Φ (thr s) (shr s)"
shows "P ⊢ s -▹ttas→⇘jvm⇙* s' = P ⊢ s -▹ttas→⇘jvmd⇙* s'"
proof
assume Red: "P ⊢ s -▹ttas→⇘jvm⇙* s'"
thus "P ⊢ s -▹ttas→⇘jvmd⇙* s'" using ct
proof(induct rule: exec_mthr.RedT_induct[consumes 1, case_names refl step])
case refl thus ?case by auto
next
case (step s ttas s' t ta s'')
hence "P ⊢ s -▹ttas→⇘jvmd⇙* s'" by blast
moreover from ‹correct_state_ts Φ (thr s) (shr s)› ‹P ⊢ s -▹ttas→⇘jvm⇙* s'›
have "correct_state_ts Φ (thr s') (shr s')"
by(auto dest: preserves_correct_state[OF wf])
with ‹P ⊢ s' -t▹ta→⇘jvm⇙ s''› have "P ⊢ s' -t▹ta→⇘jvmd⇙ s''"
by(unfold mexecT_eq_mexecdT[OF wf])
ultimately show ?case
by(blast intro: execd_mthr.RedTI rtrancl3p_step elim: execd_mthr.RedTE)
qed
next
assume Red: "P ⊢ s -▹ttas→⇘jvmd⇙* s'"
thus "P ⊢ s -▹ttas→⇘jvm⇙* s'" using ct
proof(induct rule: execd_mthr.RedT_induct[consumes 1, case_names refl step])
case refl thus ?case by auto
next
case (step s ttas s' t ta s'')
hence "P ⊢ s -▹ttas→⇘jvm⇙* s'" by blast
moreover from ‹correct_state_ts Φ (thr s) (shr s)› ‹P ⊢ s -▹ttas→⇘jvmd⇙* s'›
have "correct_state_ts Φ (thr s') (shr s')"
by(auto dest: preserves_correct_state_d[OF wf])
with ‹P ⊢ s' -t▹ta→⇘jvmd⇙ s''› have "P ⊢ s' -t▹ta→⇘jvm⇙ s''"
by(unfold mexecT_eq_mexecdT[OF wf])
ultimately show ?case
by(blast intro: exec_mthr.RedTI rtrancl3p_step elim: exec_mthr.RedTE)
qed
qed
lemma mexecT_preserves_thread_conf:
"⟦ wf_jvm_prog⇘Φ⇙ P; correct_state_ts Φ (thr s) (shr s);
P ⊢ s -t'▹ta→⇘jvm⇙ s'; thread_conf P (thr s) (shr s) ⟧
⟹ thread_conf P (thr s') (shr s')"
by(simp only: mexecT_eq_mexecdT)(rule execd_tconf.redT_preserves)
lemma mExecT_preserves_thread_conf:
"⟦ wf_jvm_prog⇘Φ⇙ P; correct_state_ts Φ (thr s) (shr s);
P ⊢ s -▹tta→⇘jvm⇙* s'; thread_conf P (thr s) (shr s) ⟧
⟹ thread_conf P (thr s') (shr s')"
by(simp only: mExecT_eq_mExecdT)(rule execd_tconf.RedT_preserves)
lemma wset_Suspend_ok_mexecd_mexec:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
shows "exec_mthr.wset_Suspend_ok P (correct_jvm_state Φ) = execd_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
apply(safe)
apply(rule execd_mthr.wset_Suspend_okI)
apply(erule exec_mthr.wset_Suspend_okD1)
apply(drule (1) exec_mthr.wset_Suspend_okD2)
apply(subst (asm) (2) split_paired_Ex)
apply(elim bexE exE conjE)
apply(subst (asm) mexec_eq_mexecd[OF wf])
apply(simp add: correct_jvm_state_def)
apply(blast dest: ts_okD)
apply(subst (asm) mexecT_eq_mexecdT[OF wf])
apply(simp add: correct_jvm_state_def)
apply(subst (asm) mExecT_eq_mExecdT[OF wf])
apply(simp add: correct_jvm_state_def)
apply(rule bexI exI|erule conjI|assumption)+
apply(rule exec_mthr.wset_Suspend_okI)
apply(erule execd_mthr.wset_Suspend_okD1)
apply(drule (1) execd_mthr.wset_Suspend_okD2)
apply(subst (asm) (2) split_paired_Ex)
apply(elim bexE exE conjE)
apply(subst (asm) mexec_eq_mexecd[OF wf, symmetric])
apply(simp add: correct_jvm_state_def)
apply(blast dest: ts_okD)
apply(subst (asm) mexecT_eq_mexecdT[OF wf, symmetric])
apply(simp add: correct_jvm_state_def)
apply(subst (asm) mExecT_eq_mExecdT[OF wf, symmetric])
apply(simp add: correct_jvm_state_def)
apply(rule bexI exI|erule conjI|assumption)+
done
end
context JVM_typesafe begin
lemma exec_wf_progress:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
shows "progress JVM_final (mexec P) (exec_mthr.wset_Suspend_ok P (correct_jvm_state Φ))"
(is "progress _ _ ?wf_state")
proof -
interpret progress: progress JVM_final "mexecd P" convert_RA ?wf_state
using assms unfolding wset_Suspend_ok_mexecd_mexec[OF wf] by(rule execd_wf_progress)
show ?thesis
proof(unfold_locales)
fix s
assume "s ∈ ?wf_state"
thus "lock_thread_ok (locks s) (thr s) ∧ exec_mthr.wset_final_ok (wset s) (thr s)"
by(rule progress.wf_stateD)
next
fix s t x ta x' m'
assume wfs: "s ∈ ?wf_state"
and tst: "thr s t = ⌊(x, no_wait_locks)⌋"
and exec: "mexec P t (x, shr s) ta (x', m')"
and wait: "¬ waiting (wset s t)"
from wfs tst have correct: "Φ ⊢ t: (fst x, shr s, snd x) √"
by(auto dest!: exec_mthr.wset_Suspend_okD1 ts_okD simp add: correct_jvm_state_def)
with exec have "mexecd P t (x, shr s) ta (x', m')"
by(cases x)(simp only: mexec_eq_mexecd[OF wf] fst_conv snd_conv)
from progress.wf_red[OF wfs tst this wait] correct
show "∃ta' x' m'. mexec P t (x, shr s) ta' (x', m') ∧
(final_thread.actions_ok JVM_final s t ta' ∨
final_thread.actions_ok' s t ta' ∧ final_thread.actions_subset ta' ta)"
by(cases x)(simp only: fst_conv snd_conv mexec_eq_mexecd[OF wf])
next
fix s t x ta x' m' w
assume wfs: "s ∈ ?wf_state"
and tst: "thr s t = ⌊(x, no_wait_locks)⌋"
and exec: "mexec P t (x, shr s) ta (x', m')"
and wait: "¬ waiting (wset s t)"
and Suspend: "Suspend w ∈ set ⦃ta⦄⇘w⇙"
from wfs tst have correct: "Φ ⊢ t: (fst x, shr s, snd x) √"
by(auto dest!: exec_mthr.wset_Suspend_okD1 ts_okD simp add: correct_jvm_state_def)
with exec have "mexecd P t (x, shr s) ta (x', m')"
by(cases x)(simp only: mexec_eq_mexecd[OF wf] fst_conv snd_conv)
with wfs tst show "¬ JVM_final x'" using wait Suspend by(rule progress.red_wait_set_not_final)
next
fix s t x
assume wfs: "s ∈ ?wf_state"
and tst: "thr s t = ⌊(x, no_wait_locks)⌋"
and "¬ JVM_final x"
from progress.wf_progress[OF this]
show "∃ta x' m'. mexec P t (x, shr s) ta (x', m')"
by(auto dest: defensive_imp_aggressive_1 simp add: split_beta)
qed(fastforce dest: mexec_instr_Wakeup_no_Join exec_ta_satisfiable)+
qed
theorem mexecd_TypeSafety:
fixes ln :: "'addr ⇒f nat"
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and s: "s ∈ execd_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
and Exec: "P ⊢ s -▹ttas→⇘jvmd⇙* s'"
and "¬ (∃t ta s''. P ⊢ s' -t▹ta→⇘jvmd⇙ s'')"
and ts't: "thr s' t = ⌊((xcp, frs), ln)⌋"
shows "frs ≠ [] ∨ ln ≠ no_wait_locks ⟹ t ∈ execd_mthr.deadlocked P s'"
and "Φ ⊢ t: (xcp, shr s', frs) √"
proof -
interpret progress JVM_final "mexecd P" convert_RA "execd_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
by(rule execd_wf_progress) fact+
from Exec s have wfs': "s' ∈ execd_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
unfolding execd_mthr.RedT_def
by(blast intro: invariant3p_rtrancl3p execd_mthr.invariant3p_wset_Suspend_ok invariant3p_correct_jvm_state_mexecdT[OF wf])
with ts't show cst: "Φ ⊢ t: (xcp, shr s', frs) √"
by(auto dest: ts_okD execd_mthr.wset_Suspend_okD1 simp add: correct_jvm_state_def)
assume nfin: "frs ≠ [] ∨ ln ≠ no_wait_locks"
from nfin ‹thr s' t = ⌊((xcp, frs), ln)⌋› have "exec_mthr.not_final_thread s' t"
by(auto simp: exec_mthr.not_final_thread_iff)
from ‹¬ (∃t ta s''. P ⊢ s' -t▹ta→⇘jvmd⇙ s'')›
show "t ∈ execd_mthr.deadlocked P s'"
proof(rule contrapos_np)
assume "t ∉ execd_mthr.deadlocked P s'"
with ‹exec_mthr.not_final_thread s' t› have "¬ execd_mthr.deadlocked' P s'"
by(auto simp add: execd_mthr.deadlocked'_def)
hence "¬ execd_mthr.deadlock P s'" unfolding execd_mthr.deadlock_eq_deadlocked' .
thus "∃t ta s''. P ⊢ s' -t▹ta→⇘jvmd⇙ s''" by(rule redT_progress[OF wfs'])
qed
qed
theorem mexec_TypeSafety:
fixes ln :: "'addr ⇒f nat"
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and s: "s ∈ exec_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
and Exec: "P ⊢ s -▹ttas→⇘jvm⇙* s'"
and "¬ (∃t ta s''. P ⊢ s' -t▹ta→⇘jvm⇙ s'')"
and ts't: "thr s' t = ⌊((xcp, frs), ln)⌋"
shows "frs ≠ [] ∨ ln ≠ no_wait_locks ⟹ t ∈ multithreaded_base.deadlocked JVM_final (mexec P) s'"
and "Φ ⊢ t: (xcp, shr s', frs) √"
proof -
interpret progress JVM_final "mexec P" convert_RA "exec_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
by(rule exec_wf_progress) fact+
from Exec s have wfs': "s' ∈ exec_mthr.wset_Suspend_ok P (correct_jvm_state Φ)"
unfolding exec_mthr.RedT_def
by(blast intro: invariant3p_rtrancl3p exec_mthr.invariant3p_wset_Suspend_ok invariant3p_correct_jvm_state_mexecT[OF wf])
with ts't show cst: "Φ ⊢ t: (xcp, shr s', frs) √"
by(auto dest: ts_okD exec_mthr.wset_Suspend_okD1 simp add: correct_jvm_state_def)
assume nfin: "frs ≠ [] ∨ ln ≠ no_wait_locks"
from nfin ‹thr s' t = ⌊((xcp, frs), ln)⌋› have "exec_mthr.not_final_thread s' t"
by(auto simp: exec_mthr.not_final_thread_iff)
from ‹¬ (∃t ta s''. P ⊢ s' -t▹ta→⇘jvm⇙ s'')›
show "t ∈ exec_mthr.deadlocked P s'"
proof(rule contrapos_np)
assume "t ∉ exec_mthr.deadlocked P s'"
with ‹exec_mthr.not_final_thread s' t› have "¬ exec_mthr.deadlocked' P s'"
by(auto simp add: exec_mthr.deadlocked'_def)
hence "¬ exec_mthr.deadlock P s'" unfolding exec_mthr.deadlock_eq_deadlocked' .
thus "∃t ta s''. P ⊢ s' -t▹ta→⇘jvm⇙ s''" by(rule redT_progress[OF wfs'])
qed
qed
lemma start_mexec_mexecd_commute:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and start: "wf_start_state P C M vs"
shows "P ⊢ JVM_start_state P C M vs -▹ttas→⇘jvmd⇙* s ⟷ P ⊢ JVM_start_state P C M vs -▹ttas→⇘jvm⇙* s"
using correct_jvm_state_initial[OF assms]
by(clarsimp simp add: correct_jvm_state_def)(rule mExecT_eq_mExecdT[symmetric, OF wf])
theorem mRtrancl_eq_mRtrancld:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and ct: "correct_state_ts Φ (thr s) (shr s)"
shows "exec_mthr.mthr.Rtrancl3p P s ttas ⟷ execd_mthr.mthr.Rtrancl3p P s ttas" (is "?lhs ⟷ ?rhs")
proof
show ?lhs if ?rhs using that ct
proof(coinduction arbitrary: s ttas)
case Rtrancl3p
interpret lifting_wf "JVM_final" "mexecd P" convert_RA "λt (xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √"
using wf by(rule lifting_wf_correct_state_d)
from Rtrancl3p(1) show ?case
proof cases
case stop: Rtrancl3p_stop
then show ?thesis using mexecT_eq_mexecdT[OF wf Rtrancl3p(2)] by clarsimp
next
case (Rtrancl3p_into_Rtrancl3p s' ttas' tta)
then show ?thesis using mexecT_eq_mexecdT[OF wf Rtrancl3p(2)] Rtrancl3p(2)
by(cases tta; cases s')(fastforce simp add: split_paired_Ex dest: redT_preserves)
qed
qed
show ?rhs if ?lhs using that ct
proof(coinduction arbitrary: s ttas)
case Rtrancl3p
interpret lifting_wf "JVM_final" "mexec P" convert_RA "λt (xcp, frs) h. Φ ⊢ t: (xcp, h, frs) √"
using wf by(rule lifting_wf_correct_state)
from Rtrancl3p(1) show ?case
proof cases
case stop: Rtrancl3p_stop
then show ?thesis using mexecT_eq_mexecdT[OF wf Rtrancl3p(2)] by clarsimp
next
case (Rtrancl3p_into_Rtrancl3p s' ttas' tta)
then show ?thesis using mexecT_eq_mexecdT[OF wf Rtrancl3p(2)] Rtrancl3p(2)
by(cases tta; cases s')(fastforce simp add: split_paired_Ex dest: redT_preserves)
qed
qed
qed
lemma start_mRtrancl_mRtrancld_commute:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and start: "wf_start_state P C M vs"
shows "exec_mthr.mthr.Rtrancl3p P (JVM_start_state P C M vs) ttas ⟷ execd_mthr.mthr.Rtrancl3p P (JVM_start_state P C M vs) ttas"
using correct_jvm_state_initial[OF assms] by(clarsimp simp add: correct_jvm_state_def mRtrancl_eq_mRtrancld[OF wf])
end
subsection ‹Determinism›
context JVM_heap_conf begin
lemma exec_instr_deterministic:
assumes wf: "wf_prog wf_md P"
and det: "deterministic_heap_ops"
and exec1: "(ta', σ') ∈ exec_instr i P t (shr s) stk loc C M pc frs"
and exec2: "(ta'', σ'') ∈ exec_instr i P t (shr s) stk loc C M pc frs"
and check: "check_instr i P (shr s) stk loc C M pc frs"
and aok1: "final_thread.actions_ok final s t ta'"
and aok2: "final_thread.actions_ok final s t ta''"
and tconf: "P,shr s ⊢ t √t"
shows "ta' = ta'' ∧ σ' = σ''"
using exec1 exec2 aok1 aok2
proof(cases i)
case (Invoke M' n)
{ fix T ta''' ta'''' va' va'' h' h''
assume T: "typeof_addr (shr s) (the_Addr (stk ! n)) = ⌊T⌋"
and "method": "snd (snd (snd (method P (class_type_of T) M'))) = None" "P ⊢ class_type_of T has M'"
and params: "P,shr s ⊢ rev (take n stk) [:≤] fst (snd (method P (class_type_of T) M'))"
and red1: "(ta''', va', h') ∈ red_external_aggr P t (the_Addr (stk ! n)) M' (rev (take n stk)) (shr s)"
and red2: "(ta'''', va'', h'') ∈ red_external_aggr P t (the_Addr (stk ! n)) M' (rev (take n stk)) (shr s)"
and ta': "ta' = extTA2JVM P ta'''"
and ta'': "ta'' = extTA2JVM P ta''''"
from T "method" params obtain T' where "P,shr s ⊢ the_Addr (stk ! n)∙M'(rev (take n stk)) : T'"
by(fastforce simp add: has_method_def confs_conv_map external_WT'_iff)
hence "P,t ⊢ ⟨the_Addr (stk ! n)∙M'(rev (take n stk)), shr s⟩ -ta'''→ext ⟨va', h'⟩"
and "P,t ⊢ ⟨the_Addr (stk ! n)∙M'(rev (take n stk)), shr s⟩ -ta''''→ext ⟨va'', h''⟩"
using red1 red2 tconf
by-(rule WT_red_external_aggr_imp_red_external[OF wf], assumption+)+
moreover from aok1 aok2 ta' ta''
have "final_thread.actions_ok final s t ta'''"
and "final_thread.actions_ok final s t ta''''"
by(auto simp add: final_thread.actions_ok_iff)
ultimately have "ta''' = ta'''' ∧ va' = va'' ∧ h' = h''"
by(rule red_external_deterministic[OF det]) }
with assms Invoke show ?thesis
by(clarsimp simp add: split_beta split: if_split_asm) blast
next
case MExit
{ assume "final_thread.actions_ok final s t ⦃UnlockFail→the_Addr (hd stk)⦄"
and "final_thread.actions_ok final s t ⦃Unlock→the_Addr (hd stk), SyncUnlock (the_Addr (hd stk))⦄"
hence False
by(auto simp add: final_thread.actions_ok_iff lock_ok_las_def finfun_upd_apply elim!: allE[where x="the_Addr (hd stk)"]) }
with assms MExit show ?thesis by(auto split: if_split_asm)
qed(auto simp add: split_beta split: if_split_asm dest: deterministic_heap_ops_readD[OF det] deterministic_heap_ops_writeD[OF det] deterministic_heap_ops_allocateD[OF det])
lemma exec_1_deterministic:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and det: "deterministic_heap_ops"
and exec1: "P,t ⊢ (xcp, shr s, frs) -ta'-jvm→ σ'"
and exec2: "P,t ⊢ (xcp, shr s, frs) -ta''-jvm→ σ''"
and aok1: "final_thread.actions_ok final s t ta'"
and aok2: "final_thread.actions_ok final s t ta''"
and conf: "Φ ⊢ t:(xcp, shr s, frs) √"
shows "ta' = ta'' ∧ σ' = σ''"
proof -
from wf obtain wf_md where wf': "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
from conf have tconf: "P,shr s ⊢ t √t" by(simp add: correct_state_def)
from exec1 conf have "P,t ⊢ Normal (xcp, shr s, frs) -ta'-jvmd→ Normal σ'"
by(simp add: welltyped_commute[OF wf])
hence "check P (xcp, shr s, frs)" by(rule jvmd_NormalE)
with exec1 exec2 aok1 aok2 tconf show ?thesis
by(cases xcp)(case_tac [!] frs, auto elim!: exec_1.cases dest: exec_instr_deterministic[OF wf' det] simp add: check_def split_beta)
qed
end
context JVM_conf_read begin
lemma invariant3p_correct_state_ts:
assumes "wf_jvm_prog⇘Φ⇙ P"
shows "invariant3p (mexecT P) {s. correct_state_ts Φ (thr s) (shr s)}"
using assms by(rule lifting_wf.invariant3p_ts_ok[OF lifting_wf_correct_state])
lemma mexec_deterministic:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and det: "deterministic_heap_ops"
shows "exec_mthr.deterministic P {s. correct_state_ts Φ (thr s) (shr s)}"
proof(rule exec_mthr.determisticI)
fix s t x ta' x' m' ta'' x'' m''
assume tst: "thr s t = ⌊(x, no_wait_locks)⌋"
and red: "mexec P t (x, shr s) ta' (x', m')" "mexec P t (x, shr s) ta'' (x'', m'')"
and aok: "exec_mthr.actions_ok s t ta'" "exec_mthr.actions_ok s t ta''"
and correct [simplified]: "s ∈ {s. correct_state_ts Φ (thr s) (shr s)}"
moreover obtain xcp frs where [simp]: "x = (xcp, frs)" by(cases x)
moreover obtain xcp' frs' where [simp]: "x' = (xcp', frs')" by(cases x')
moreover obtain xcp'' frs'' where [simp]: "x'' = (xcp'', frs'')" by(cases x'')
ultimately have exec1: "P,t ⊢ (xcp, shr s, frs) -ta'-jvm→ (xcp', m', frs')"
and exec1: "P,t ⊢ (xcp, shr s, frs) -ta''-jvm→ (xcp'', m'', frs'')"
by simp_all
moreover note aok
moreover from correct tst have "Φ ⊢ t:(xcp, shr s, frs)√"
by(auto dest: ts_okD)
ultimately have "ta' = ta'' ∧ (xcp', m', frs') = (xcp'', m'', frs'')"
by(rule exec_1_deterministic[OF wf det])
thus "ta' = ta'' ∧ x' = x'' ∧ m' = m''" by simp
qed(rule invariant3p_correct_state_ts[OF wf])
end
end