Theory Correctness2
section ‹Correctness of Stage 2: The multithreaded setting›
theory Correctness2
imports
J1JVM
JVMJ1
"../BV/BVProgressThreaded"
begin
declare Listn.lesub_list_impl_same_size[simp del]
context J1_JVM_heap_conf_base begin
lemma bisim1_list1_has_methodD: "bisim1_list1 t h ex exs xcp ((stk, loc, C, M, pc) # frs) ⟹ P ⊢ C has M"
by(fastforce elim!: bisim1_list1.cases intro: has_methodI)
end
declare compP_has_method [simp]
sublocale J1_JVM_heap_conf_base < Red1_exec:
delay_bisimulation_base "mred1 P t" "mexec (compP2 P) t" "wbisim1 t" "ta_bisim wbisim1" "τMOVE1 P" "τMOVE2 (compP2 P)"
for t
.
sublocale J1_JVM_heap_conf_base < Red1_execd: delay_bisimulation_base
"mred1 P t"
"mexecd (compP2 P) t"
"wbisim1 t"
"ta_bisim wbisim1"
"τMOVE1 P"
"τMOVE2 (compP2 P)"
for t
.
context JVM_heap_base begin
lemma τexec_1_d_silent_move:
"τexec_1_d P t (xcp, h, frs) (xcp', h', frs')
⟹ τtrsys.silent_move (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
apply(rule τtrsys.silent_move.intros)
apply auto
apply(rule exec_1_d_NormalI)
apply(auto simp add: exec_1_iff exec_d_def)
done
lemma silent_move_τexec_1_d:
"τtrsys.silent_move (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')
⟹ τexec_1_d P t (xcp, h, frs) (xcp', h', frs')"
apply(erule τtrsys.silent_move.cases)
apply clarsimp
apply(erule jvmd_NormalE)
apply(auto simp add: exec_1_iff)
done
lemma τExec_1_dr_rtranclpD:
"τExec_1_dr P t (xcp, h, frs) (xcp', h', frs')
⟹ τtrsys.silent_moves (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
by(induct rule: rtranclp_induct3)(blast intro: rtranclp.rtrancl_into_rtrancl τexec_1_d_silent_move)+
lemma τExec_1_dt_tranclpD:
"τExec_1_dt P t (xcp, h, frs) (xcp', h', frs')
⟹ τtrsys.silent_movet (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
by(induct rule: tranclp_induct3)(blast intro: tranclp.trancl_into_trancl τexec_1_d_silent_move)+
lemma rtranclp_τExec_1_dr:
"τtrsys.silent_moves (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')
⟹ τExec_1_dr P t (xcp, h, frs) (xcp', h', frs')"
by(induct rule: rtranclp_induct[of _ "((ax, ay), az)" "((bx, by), bz)", split_rule, consumes 1])(blast intro: rtranclp.rtrancl_into_rtrancl silent_move_τexec_1_d)+
lemma tranclp_τExec_1_dt:
"τtrsys.silent_movet (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')
⟹ τExec_1_dt P t (xcp, h, frs) (xcp', h', frs')"
by(induct rule: tranclp_induct[of _ "((ax, ay), az)" "((bx, by), bz)", split_rule, consumes 1])(blast intro: tranclp.trancl_into_trancl silent_move_τexec_1_d)+
lemma τExec_1_dr_conv_rtranclp:
"τExec_1_dr P t (xcp, h, frs) (xcp', h', frs') =
τtrsys.silent_moves (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
by(blast intro: τExec_1_dr_rtranclpD rtranclp_τExec_1_dr)
lemma τExec_1_dt_conv_tranclp:
"τExec_1_dt P t (xcp, h, frs) (xcp', h', frs') =
τtrsys.silent_movet (mexecd P t) (τMOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
by(blast intro: τExec_1_dt_tranclpD tranclp_τExec_1_dt)
end
context J1_JVM_conf_read begin
lemma Red1_execd_weak_bisim:
assumes wf: "wf_J1_prog P"
shows "delay_bisimulation_measure (mred1 P t) (mexecd (compP2 P) t) (wbisim1 t) (ta_bisim wbisim1) (τMOVE1 P) (τMOVE2 (compP2 P)) (λ(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') (λ(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')"
proof
fix s1 s2 s1'
assume "wbisim1 t s1 s2" and "τtrsys.silent_move (mred1 P t) (τMOVE1 P) s1 s1'"
moreover obtain e xs exs h where s1: "s1 = (((e, xs), exs), h)" by(cases s1) auto
moreover obtain e' xs' exs' h1' where s1': "s1' = (((e', xs'), exs'), h1')" by(cases s1') auto
moreover obtain xcp frs h2 where s2: "s2 = ((xcp, frs), h2)" by(cases s2) auto
ultimately have [simp]: "h2 = h" and red: "True,P,t ⊢1 ⟨(e, xs)/exs,h⟩ -ε→ ⟨(e', xs')/exs',h1'⟩"
and τ: "τMove1 P h ((e, xs), exs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs" by(auto)
from red τ bisim have h1' [simp]: "h1' = h" by(auto dest: τmove1_heap_unchanged elim!: Red1.cases bisim1_list1.cases)
from exec_1_simulates_Red1_τ[OF wf red[unfolded h1'] bisim τ] obtain xcp' frs'
where exec: "(if sim12_size e' < sim12_size e then τExec_1_dr else τExec_1_dt) (compP2 P) t (xcp, h, frs) (xcp', h, frs')"
and bisim': "bisim1_list1 t h (e', xs') exs' xcp' frs'" by blast
from exec have "(if (λ(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') (((e', xs'), exs'), h) (((e, xs), exs), h) then τtrsys.silent_moves (mexecd (compP2 P) t) (τMOVE2 (compP2 P)) else τtrsys.silent_movet (mexecd (compP2 P) t) (τMOVE2 (compP2 P))) ((xcp, frs), h) ((xcp', frs'), h)"
by(auto simp add: τExec_1_dr_conv_rtranclp τExec_1_dt_conv_tranclp)
thus "wbisim1 t s1' s2 ∧ (λ(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')⇧+⇧+ s1' s1 ∨
(∃s2'. (τtrsys.silent_movet (mexecd (compP2 P) t) (τMOVE2 (compP2 P))) s2 s2' ∧ wbisim1 t s1' s2')"
using bisim' s1 s1' s2
by -(rule delay_bisimulation_base.simulation_silent1I', auto split del: if_split)
next
fix s1 s2 s2'
assume "wbisim1 t s1 s2" and "τtrsys.silent_move (mexecd (compP2 P) t) (τMOVE2 (compP2 P)) s2 s2'"
moreover obtain e xs exs h1 where s1: "s1 = (((e, xs), exs), h1)" by(cases s1) auto
moreover obtain xcp frs h where s2: "s2 = ((xcp, frs), h)" by(cases s2) auto
moreover obtain xcp' frs' h2' where s2': "s2' = ((xcp', frs'), h2')" by(cases s2') auto
ultimately have [simp]: "h1 = h" and exec: "exec_1_d (compP2 P) t (Normal (xcp, h, frs)) ε (Normal (xcp', h2', frs'))"
and τ: "τMove2 (compP2 P) (xcp, h, frs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs" by(auto)
from τRed1_simulates_exec_1_τ[OF wf exec bisim τ]
obtain e' xs' exs' where [simp]: "h2' = h"
and red: "(if sim21_size (compP2 P) (xcp', frs') (xcp, frs) then τRed1r else τRed1t) P t h ((e, xs), exs) ((e', xs'), exs')"
and bisim': "bisim1_list1 t h (e', xs') exs' xcp' frs'" by blast
from red have "(if ((λ(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') ((xcp', frs'), h2') ((xcp, frs), h)) then τtrsys.silent_moves (mred1 P t) (τMOVE1 P) else τtrsys.silent_movet (mred1 P t) (τMOVE1 P)) (((e, xs), exs), h) (((e', xs'), exs'), h)"
by(auto dest: τRed1r_rtranclpD τRed1t_tranclpD)
thus "wbisim1 t s1 s2' ∧ (λ(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')⇧+⇧+ s2' s2 ∨
(∃s1'. τtrsys.silent_movet (mred1 P t) (τMOVE1 P) s1 s1' ∧ wbisim1 t s1' s2')"
using bisim' s1 s2 s2'
by -(rule delay_bisimulation_base.simulation_silent2I', auto split del: if_split)
next
fix s1 s2 tl1 s1'
assume "wbisim1 t s1 s2" and "mred1 P t s1 tl1 s1'" and "¬ τMOVE1 P s1 tl1 s1'"
moreover obtain e xs exs h where s1: "s1 = (((e, xs), exs), h)" by(cases s1) auto
moreover obtain e' xs' exs' h1' where s1': "s1' = (((e', xs'), exs'), h1')" by(cases s1') auto
moreover obtain xcp frs h2 where s2: "s2 = ((xcp, frs), h2)" by(cases s2) auto
ultimately have [simp]: "h2 = h" and red: "True,P,t ⊢1 ⟨(e, xs)/exs,h⟩ -tl1→ ⟨(e', xs')/exs',h1'⟩"
and τ: "¬ τMove1 P h ((e, xs), exs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs"
by(fastforce elim!: Red1.cases dest: red1_τ_taD)+
from exec_1_simulates_Red1_not_τ[OF wf red bisim τ] obtain ta' xcp' frs' xcp'' frs''
where exec1: "τExec_1_dr (compP2 P) t (xcp, h, frs) (xcp', h, frs')"
and exec2: "exec_1_d (compP2 P) t (Normal (xcp', h, frs')) ta' (Normal (xcp'', h1', frs''))"
and τ': "¬ τMove2 (compP2 P) (xcp', h, frs')"
and bisim': "bisim1_list1 t h1' (e', xs') exs' xcp'' frs''"
and ta': "ta_bisim wbisim1 tl1 ta'" by blast
from exec1 have "τtrsys.silent_moves (mexecd (compP2 P) t) (τMOVE2 (compP2 P)) ((xcp, frs), h) ((xcp', frs'), h)"
by(rule τExec_1_dr_rtranclpD)
thus "∃s2' s2'' tl2. τtrsys.silent_moves (mexecd (compP2 P) t) (τMOVE2 (compP2 P)) s2 s2' ∧
mexecd (compP2 P) t s2' tl2 s2'' ∧ ¬ τMOVE2 (compP2 P) s2' tl2 s2'' ∧
wbisim1 t s1' s2'' ∧ ta_bisim wbisim1 tl1 tl2"
using bisim' exec2 τ' s1 s1' s2 ta' unfolding ‹h2 = h›
apply(subst (1 2) split_paired_Ex)
apply(subst (1 2) split_paired_Ex)
by clarify ((rule exI conjI|assumption)+, auto)
next
fix s1 s2 tl2 s2'
assume "wbisim1 t s1 s2" and "mexecd (compP2 P) t s2 tl2 s2'" and "¬ τMOVE2 (compP2 P) s2 tl2 s2'"
moreover obtain e xs exs h1 where s1: "s1 = (((e, xs), exs), h1)" by(cases s1) auto
moreover obtain xcp frs h where s2: "s2 = ((xcp, frs), h)" by(cases s2) auto
moreover obtain xcp' frs' h2' where s2': "s2' = ((xcp', frs'), h2')" by(cases s2') auto
ultimately have [simp]: "h1 = h" and exec: "exec_1_d (compP2 P) t (Normal (xcp, h, frs)) tl2 (Normal (xcp', h2', frs'))"
and τ: "¬ τMove2 (compP2 P) (xcp, h, frs)" and bisim: "bisim1_list1 t h (e, xs) exs xcp frs"
apply auto
apply(erule jvmd_NormalE)
apply(cases xcp)
apply auto
apply(rename_tac stk loc C M pc frs)
apply(case_tac "instrs_of (compP2 P) C M ! pc")
apply(simp_all split: if_split_asm)
apply(auto dest!: τexternal_red_external_aggr_TA_empty simp add: check_def has_method_def τexternal_def τexternal'_def)
done
from τRed1_simulates_exec_1_not_τ[OF wf exec bisim τ] obtain e' xs' exs' ta' e'' xs'' exs''
where red1: "τRed1r P t h ((e, xs), exs) ((e', xs'), exs')"
and red2: "True,P,t ⊢1 ⟨(e', xs')/exs',h⟩ -ta'→ ⟨(e'', xs'')/exs'',h2'⟩"
and τ': "¬ τMove1 P h ((e', xs'), exs')" and ta': "ta_bisim wbisim1 ta' tl2"
and bisim': "bisim1_list1 t h2' (e'', xs'') exs'' xcp' frs'" by blast
from red1 have "τtrsys.silent_moves (mred1 P t) (τMOVE1 P) (((e, xs), exs), h) (((e', xs'), exs'), h)"
by(rule τRed1r_rtranclpD)
thus "∃s1' s1'' tl1. τtrsys.silent_moves (mred1 P t) (τMOVE1 P) s1 s1' ∧ mred1 P t s1' tl1 s1'' ∧
¬ τMOVE1 P s1' tl1 s1'' ∧ wbisim1 t s1'' s2' ∧ ta_bisim wbisim1 tl1 tl2"
using bisim' red2 τ' s1 s2 s2' ‹h1 = h› ta'
apply -
apply(rule exI[where x="(((e', xs'), exs'), h)"])
apply(rule exI[where x="(((e'', xs''), exs''), h2')"])
apply(rule exI[where x="ta'"])
apply auto
done
next
have "wf (inv_image {(x, y). x < y} (λ(((e, xs), exs), h). sim12_size e))"
by(rule wf_inv_image)(rule wf_less)
also have "inv_image {(x, y). x < y} (λ(((e, xs), exs), h). sim12_size e) =
{(x, y). (λ(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e') x y}" by auto
finally show "wfP (λ(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e')"
unfolding wfp_def .
next
from wfP_sim21_size
have "wf {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'}" by(unfold wfp_def)
hence "wf (inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst)" by(rule wf_inv_image)
also have "inv_image {(xcpfrs, xcpfrs'). sim21_size (compP2 P) xcpfrs xcpfrs'} fst =
{((xcpfrs, h), (xcpfrs', h)). sim21_size (compP2 P) xcpfrs xcpfrs'}" by auto
also have "… = {(x, y). (λ(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs') x y}" by(auto)
finally show "wfP (λ(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs')"
unfolding wfp_def .
qed
lemma Red1_execd_delay_bisim:
assumes wf: "wf_J1_prog P"
shows "delay_bisimulation_diverge (mred1 P t) (mexecd (compP2 P) t) (wbisim1 t) (ta_bisim wbisim1) (τMOVE1 P) (τMOVE2 (compP2 P))"
proof -
interpret delay_bisimulation_measure
"mred1 P t" "mexecd (compP2 P) t" "wbisim1 t" "ta_bisim wbisim1" "τMOVE1 P" "τMOVE2 (compP2 P)"
"λ(((e, xs), exs), h) (((e', xs'), exs'), h'). sim12_size e < sim12_size e'"
"λ(xcpfrs, h) (xcpfrs', h). sim21_size (compP2 P) xcpfrs xcpfrs'"
using wf by(rule Red1_execd_weak_bisim)
show ?thesis by(unfold_locales)
qed
end
definition bisim_wait1JVM ::
"'addr jvm_prog ⇒ ('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list ⇒ 'addr jvm_thread_state ⇒ bool"
where
"bisim_wait1JVM P ≡
λ((e1, xs1), exs1) (xcp, frs). call1 e1 ≠ None ∧
(case frs of Nil ⇒ False | (stk, loc, C, M, pc) # frs' ⇒ ∃M' n. instrs_of P C M ! pc = Invoke M' n)"
sublocale J1_JVM_heap_conf_base < Red1_execd:
FWbisimulation_base
final_expr1
"mred1 P"
JVM_final
"mexecd (compP2 P)"
convert_RA
wbisim1
"bisim_wait1JVM (compP2 P)"
.
sublocale JVM_heap_base < execd_mthr:
τmultithreaded
JVM_final
"mexecd P"
convert_RA
"τMOVE2 P"
for P
by(unfold_locales)
sublocale J1_JVM_heap_conf_base < Red1_execd:
FWdelay_bisimulation_base
final_expr1
"mred1 P"
JVM_final
"mexecd (compP2 P)"
convert_RA
"wbisim1"
"bisim_wait1JVM (compP2 P)"
"τMOVE1 P"
"τMOVE2 (compP2 P)"
by(unfold_locales)
context J1_JVM_conf_read begin
theorem Red1_exec1_FWwbisim:
assumes wf: "wf_J1_prog P"
shows "FWdelay_bisimulation_diverge final_expr1 (mred1 P) JVM_final (mexecd (compP2 P)) wbisim1 (bisim_wait1JVM (compP2 P)) (τMOVE1 P) (τMOVE2 (compP2 P))"
proof -
let ?exec = "mexecd (compP2 P)"
let ?τexec = "λt. τtrsys.silent_moves (mexecd (compP2 P) t) (τMOVE2 (compP2 P))"
let ?τred = "λt. τtrsys.silent_moves (mred1 P t) (τMOVE1 P)"
interpret delay_bisimulation_diverge
"mred1 P t" "?exec t" "wbisim1 t" "ta_bisim wbisim1" "τMOVE1 P" "τMOVE2 (compP2 P)"
for t
using wf by(rule Red1_execd_delay_bisim)
show ?thesis
proof
fix t s1 s2
assume "wbisim1 t s1 s2" "(λ(x1, m). final_expr1 x1) s1"
moreover obtain e xs exs m1 where [simp]: "s1 = (((e, xs), exs), m1)" by(cases s1) auto
moreover obtain xcp frs m2 where [simp]: "s2 = ((xcp, frs), m2)" by(cases s2) auto
ultimately have [simp]: "m2 = m1" "exs = []"
and "bisim1_list1 t m1 (e, xs) [] xcp frs"
and "final e" by auto
from ‹bisim1_list1 t m1 (e, xs) [] xcp frs› ‹final e›
show "∃s2'. ?τexec t s2 s2' ∧ wbisim1 t s1 s2' ∧ (λ(x2, m). JVM_final x2) s2'"
proof cases
case (bl1_Normal stk loc C M pc frs' Ts T body D)
hence [simp]: "frs = [(stk, loc, C, M, pc)]"
and conf: "compTP P ⊢ t:(xcp, m1, frs) √"
and sees: "P ⊢ C sees M: Ts→T = ⌊body⌋ in D"
and bisim: "P,blocks1 0 (Class D # Ts) body,m1 ⊢ (e, xs) ↔ (stk, loc, pc, xcp)"
and var: "max_vars e ≤ length xs" by auto
from ‹final e› show ?thesis
proof cases
fix v
assume [simp]: "e = Val v"
with bisim have [simp]: "xcp = None" "xs = loc"
and exec: "τExec_mover_a P t (blocks1 0 (Class D # Ts) body) m1 (stk, loc, pc, xcp) ([v], loc, length (compE2 body), None)"
by(auto dest!: bisim1Val2D1)
from exec have "τExec_mover_a P t body m1 (stk, loc, pc, xcp) ([v], loc, length (compE2 body), None)"
unfolding τExec_mover_blocks1 .
with sees have "τExec_1r (compP2 P) t (xcp, m1, frs) (None, m1, [([v], loc, C, M, length (compE2 body))])"
by(auto intro: τExec_mover_τExec_1r)
with wt_compTP_compP2[OF wf]
have execd: "τExec_1_dr (compP2 P) t (xcp, m1, frs) (None, m1, [([v], loc, C, M, length (compE2 body))])"
using conf by(rule τExec_1r_τExec_1_dr)
also from sees_method_compP[OF sees, of "λC M Ts T. compMb2"] sees max_stack1[of body]
have "τexec_1_d (compP2 P) t (None, m1, [([v], loc, C, M, length (compE2 body))]) (None, m1, [])"
by(auto simp add: τexec_1_d_def compP2_def compMb2_def check_def has_methodI intro: exec_1I)
finally have "?τexec t s2 ((None, []), m1)"
unfolding τExec_1_dr_conv_rtranclp by simp
moreover have "JVM_final (None, [])" by simp
moreover from conf have "hconf m1" "preallocated m1" unfolding correct_state_def by(simp_all)
hence "wbisim1 t s1 ((None, []), m1)" by(auto intro: bisim1_list1.intros)
ultimately show ?thesis by blast
next
fix a
assume [simp]: "e = throw (addr a)"
hence "∃stk' loc' pc'. τExec_mover_a P t body m1 (stk, loc, pc, xcp) (stk', loc', pc', ⌊a⌋) ∧ P,blocks1 0 (Class D # Ts) body,m1 ⊢ (Throw a, xs) ↔ (stk', loc', pc', ⌊a⌋)"
proof(cases xcp)
case None
with bisim show ?thesis
by(fastforce dest!: bisim1_Throw_τExec_movet simp del: blocks1.simps intro: tranclp_into_rtranclp)
next
case (Some a')
with bisim have "a = a'" by(auto dest: bisim1_ThrowD)
with Some bisim show ?thesis by(auto)
qed
then obtain stk' loc' pc'
where exec: "τExec_mover_a P t body m1 (stk, loc, pc, xcp) (stk', loc', pc', ⌊a⌋)"
and bisim': "P,blocks1 0 (Class D # Ts) body,m1 ⊢ (throw (addr a), xs) ↔ (stk', loc', pc', ⌊a⌋)" by blast
with sees have "τExec_1r (compP2 P) t (xcp, m1, frs) (⌊a⌋, m1, [(stk', loc', C, M, pc')])"
by(auto intro: τExec_mover_τExec_1r)
with wt_compTP_compP2[OF wf]
have execd: "τExec_1_dr (compP2 P) t (xcp, m1, frs) (⌊a⌋, m1, [(stk', loc', C, M, pc')])"
using conf by(rule τExec_1r_τExec_1_dr)
also {
from bisim1_xcp_Some_not_caught[OF bisim', of "λC M Ts T. compMb2" 0 0]
have "match_ex_table (compP2 P) (cname_of m1 a) pc' (compxE2 body 0 0) = None" by(simp add: compP2_def)
moreover from bisim' have "pc' < length (compE2 body)" by(auto dest: bisim1_ThrowD)
ultimately have "τexec_1 (compP2 P) t (⌊a⌋, m1, [(stk', loc', C, M, pc')]) (⌊a⌋, m1, [])"
using sees_method_compP[OF sees, of "λC M Ts T. compMb2"] sees
by(auto simp add: τexec_1_def compP2_def compMb2_def has_methodI intro: exec_1I)
moreover from wt_compTP_compP2[OF wf] execd conf
have "compTP P ⊢ t:(⌊a⌋, m1, [(stk', loc', C, M, pc')]) √" by(rule τExec_1_dr_preserves_correct_state)
ultimately have "τexec_1_d (compP2 P) t (⌊a⌋, m1, [(stk', loc', C, M, pc')]) (⌊a⌋, m1, [])"
using wt_compTP_compP2[OF wf]
by(auto simp add: τexec_1_def τexec_1_d_def welltyped_commute[symmetric] elim: jvmd_NormalE) }
finally have "?τexec t s2 ((⌊a⌋, []), m1)"
unfolding τExec_1_dr_conv_rtranclp by simp
moreover have "JVM_final (⌊a⌋, [])" by simp
moreover from conf have "hconf m1" "preallocated m1" by(simp_all add: correct_state_def)
hence "wbisim1 t s1 ((⌊a⌋, []), m1)" by(auto intro: bisim1_list1.intros)
ultimately show ?thesis by blast
qed
qed(auto intro!: exI bisim1_list1.intros)
next
fix t s1 s2
assume "wbisim1 t s1 s2" "(λ(x2, m). JVM_final x2) s2"
moreover obtain e xs exs m1 where [simp]: "s1 = (((e, xs), exs), m1)" by(cases s1) auto
moreover obtain xcp frs m2 where [simp]: "s2 = ((xcp, frs), m2)" by(cases s2) auto
ultimately have [simp]: "m2 = m1" "exs = []" "frs = []"
and bisim: "bisim1_list1 t m1 (e, xs) [] xcp []" by(auto elim: bisim1_list1.cases)
hence "final e" by(auto elim: bisim1_list1.cases)
thus "∃s1'. ?τred t s1 s1' ∧ wbisim1 t s1' s2 ∧ (λ(x1, m). final_expr1 x1) s1'" using bisim by auto
next
fix t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'
assume b: "wbisim1 t' (x, m1) (xx, m2)" and b': "wbisim1 t (x1, m1) (x2, m2)"
and τred: "?τred t (x1, m1) (x1', m1)"
and red: "mred1 P t (x1', m1) ta1 (x1'', m1')"
and "¬ τMOVE1 P (x1', m1) ta1 (x1'', m1')"
and τexec: "?τexec t (x2, m2) (x2', m2)"
and exec: "?exec t (x2', m2) ta2 (x2'', m2')"
and "¬ τMOVE2 (compP2 P) (x2', m2) ta2 (x2'', m2')"
and b2: "wbisim1 t (x1'', m1') (x2'', m2')"
from red have "hext m1 m1'" by(auto simp add: split_beta intro: Red1_hext_incr)
moreover from b2 have "m1' = m2'" by(cases x1'', cases x2'') simp
moreover from b2 have "hconf m2'"
by(cases x1'', cases x2'')(auto elim!: bisim1_list1.cases simp add: correct_state_def)
moreover from b' exec have "preallocated m2"
by(cases x1, cases x2)(auto elim!: bisim1_list1.cases simp add: correct_state_def)
moreover from b' τred red have tconf: "compP2 P,m2 ⊢ t √t"
by(cases x1, cases x2)(auto elim!: bisim1_list1.cases Red1.cases simp add: correct_state_def τmreds1_Val_Nil τmreds1_Throw_Nil)
from τexec have τexec': "τExec_1_dr (compP2 P) t (fst x2, m2, snd x2) (fst x2', m2, snd x2')"
unfolding τExec_1_dr_conv_rtranclp by simp
with b' tconf have "compTP P ⊢ t: (fst x2', m2, snd x2') √"
using ‹preallocated m2›
apply(cases x1, cases x2)
apply(erule τExec_1_dr_preserves_correct_state[OF wt_compTP_compP2[OF wf]])
apply(auto elim!: bisim1_list1.cases simp add: correct_state_def)
done
ultimately show "wbisim1 t' (x, m1') (xx, m2')" using b exec
apply(cases x, cases xx)
apply(auto elim!: bisim1_list1.cases intro!: bisim1_list1.intros simp add: split_beta intro: preallocated_hext)
apply(erule (2) correct_state_heap_change[OF wt_compTP_compP2[OF wf]])
apply(erule (1) bisim1_hext_mono)
apply(erule List.list_all2_mono)
apply(erule (1) bisim1_fr_hext_mono)
done
next
fix t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w
assume b: "wbisim1 t (x1, m1) (x2, m2)"
and τred: "?τred t (x1, m1) (x1', m1)"
and red: "mred1 P t (x1', m1) ta1 (x1'', m1')"
and "¬ τMOVE1 P (x1', m1) ta1 (x1'', m1')"
and τexec: "?τexec t (x2, m2) (x2', m2)"
and exec: "?exec t (x2', m2) ta2 (x2'', m2')"
and "¬ τMOVE2 (compP2 P) (x2', m2) ta2 (x2'', m2')"
and b': "wbisim1 t (x1'', m1') (x2'', m2')"
and "ta_bisim wbisim1 ta1 ta2"
and Suspend: "Suspend w ∈ set ⦃ta1⦄⇘w⇙" "Suspend w ∈ set ⦃ta2⦄⇘w⇙"
from red Suspend
have "call1 (fst (fst x1'')) ≠ None"
by(cases x1')(cases x1'', auto dest: Red1_Suspend_is_call)
moreover from mexecd_Suspend_Invoke[OF exec Suspend(2)]
obtain xcp stk loc C M pc frs' M' n where "x2'' = (xcp, (stk, loc, C, M, pc) # frs')"
"instrs_of (compP2 P) C M ! pc = Invoke M' n" by blast
ultimately show "bisim_wait1JVM (compP2 P) x1'' x2''"
by(simp add: bisim_wait1JVM_def split_beta)
next
fix t x1 m1 x2 m2 ta1 x1' m1'
assume "wbisim1 t (x1, m1) (x2, m2)"
and "bisim_wait1JVM (compP2 P) x1 x2"
and "mred1 P t (x1, m1) ta1 (x1', m1')"
and wakeup: "Notified ∈ set ⦃ta1⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1⦄⇘w⇙"
moreover obtain e1 xs1 exs1 where [simp]: "x1 = ((e1, xs1), exs1)" by(cases x1) auto
moreover obtain xcp frs where [simp]: "x2 = (xcp, frs)" by(cases x2)
moreover obtain e1' xs1' exs1' where [simp]: "x1' = ((e1', xs1'), exs1')" by(cases x1') auto
ultimately have [simp]: "m1 = m2"
and bisim: "bisim1_list1 t m2 (e1, xs1) exs1 xcp frs"
and red: "True,P,t ⊢1 ⟨(e1, xs1)/exs1, m2⟩ -ta1→ ⟨(e1', xs1')/exs1', m1'⟩"
and call: "call1 e1 ≠ None"
"case frs of [] ⇒ False | (stk, loc, C, M, pc) # frs' ⇒ ∃M' n. instrs_of (compP2 P) C M ! pc = Invoke M' n"
by(auto simp add: bisim_wait1JVM_def split_def)
from red wakeup have "¬ τMove1 P m2 ((e1, xs1), exs1)"
by(auto elim!: Red1.cases dest: red1_τ_taD simp add: split_beta ta_upd_simps)
from exec_1_simulates_Red1_not_τ[OF wf red bisim this] call
show "∃ta2 x2' m2'. mexecd (compP2 P) t (x2, m2) ta2 (x2', m2') ∧ wbisim1 t (x1', m1') (x2', m2') ∧ ta_bisim wbisim1 ta1 ta2"
by(auto simp del: not_None_eq simp add: split_paired_Ex ta_bisim_def ta_upd_simps split: list.split_asm)
next
fix t x1 m1 x2 m2 ta2 x2' m2'
assume "wbisim1 t (x1, m1) (x2, m2)"
and "bisim_wait1JVM (compP2 P) x1 x2"
and "mexecd (compP2 P) t (x2, m2) ta2 (x2', m2')"
and wakeup: "Notified ∈ set ⦃ta2⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta2⦄⇘w⇙"
moreover obtain e1 xs1 exs1 where [simp]: "x1 = ((e1, xs1), exs1)" by(cases x1) auto
moreover obtain xcp frs where [simp]: "x2 = (xcp, frs)" by(cases x2)
moreover obtain xcp' frs' where [simp]: "x2' = (xcp', frs')" by(cases x2')
ultimately have [simp]: "m1 = m2"
and bisim: "bisim1_list1 t m2 (e1, xs1) exs1 xcp frs"
and exec: "compP2 P,t ⊢ Normal (xcp, m2, frs) -ta2-jvmd→ Normal (xcp', m2', frs')"
and call: "call1 e1 ≠ None"
"case frs of [] ⇒ False | (stk, loc, C, M, pc) # frs' ⇒ ∃M' n. instrs_of (compP2 P) C M ! pc = Invoke M' n"
by(auto simp add: bisim_wait1JVM_def split_def)
from exec wakeup have "¬ τMove2 (compP2 P) (xcp, m2, frs)"
by(auto dest: τexec_1_taD simp add: split_beta ta_upd_simps)
from τRed1_simulates_exec_1_not_τ[OF wf exec bisim this] call
show "∃ta1 x1' m1'. mred1 P t (x1, m1) ta1 (x1', m1') ∧ wbisim1 t (x1', m1') (x2', m2') ∧ ta_bisim wbisim1 ta1 ta2"
by(auto simp del: not_None_eq simp add: split_paired_Ex ta_bisim_def ta_upd_simps split: list.split_asm)
next
show "(∃x. final_expr1 x) ⟷ (∃x. JVM_final x)"
by(auto simp add: split_paired_Ex final_iff)
qed
qed
end
sublocale J1_JVM_heap_conf_base < Red1_mexecd:
FWbisimulation_base
final_expr1
"mred1 P"
JVM_final
"mexecd (compP2 P)"
convert_RA
"wbisim1"
"bisim_wait1JVM (compP2 P)"
.
context J1_JVM_heap_conf begin
lemma bisim_J1_JVM_start:
assumes wf: "wf_J1_prog P"
and wf_start: "wf_start_state P C M vs"
shows "Red1_execd.mbisim (J1_start_state P C M vs) (JVM_start_state (compP2 P) C M vs)"
proof -
from wf_start obtain Ts T body D where start: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T=⌊body⌋ in D" and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases
let ?e = "blocks1 0 (Class D#Ts) body"
let ?xs = "Null # vs @ replicate (max_vars body) undefined_value"
from sees_wf_mdecl[OF wf sees] obtain T'
where B: "ℬ body (Suc (length Ts))"
and wt: "P,Class D # Ts ⊢1 body :: T'"
and da: "𝒟 body ⌊{..length Ts}⌋"
and sv: "syncvars body"
by(auto simp add: wf_mdecl_def)
have "P,?e,start_heap ⊢ (?e, ?xs) ↔ ([], ?xs, 0, None)" by(rule bisim1_refl)
moreover
from wf have wf': "wf_jvm_prog⇘compTP P⇙ (compP2 P)" by(rule wt_compTP_compP2)
from sees_method_compP[OF sees, of "λC M Ts T. compMb2"]
have sees': "compP2 P ⊢ C sees M: Ts→T = ⌊compMb2 body⌋ in D" by(simp add: compP2_def)
from conf have "compP2 P,start_heap ⊢ vs [:≤] Ts" by(simp add: compP2_def heap_base.compP_confs)
from BV_correct_initial[OF wf' start sees' this] sees'
have "compTP P ⊢ start_tid:(None, start_heap, [([], ?xs, D, M, 0)]) √"
by(simp add: JVM_start_state'_def compP2_def compMb2_def)
hence "bisim1_list1 start_tid start_heap (?e, ?xs) [] None [([], ?xs, D, M, 0)]"
using sees_method_idemp[OF sees]
proof
show "P,?e,start_heap ⊢ (?e, ?xs) ↔ ([], ?xs, 0, None)"
by(rule bisim1_refl)
show "max_vars ?e ≤ length ?xs" using conf
by(auto simp add: blocks1_max_vars dest: list_all2_lengthD)
qed simp
thus ?thesis
using sees sees' unfolding start_state_def
by -(rule Red1_execd.mbisimI, auto split: if_split_asm intro: wset_thread_okI simp add: compP2_def compMb2_def)
qed
lemmas τred1_Val_simps = τred1r_Val τred1t_Val τreds1r_map_Val τreds1t_map_Val
end
end