(* Title: JinjaThreads/BV/JVMDeadlocked.thy Author: Andreas Lochbihler *) section ‹Preservation of deadlock for the JVMs› theory JVMDeadlocked imports BVProgressThreaded begin context JVM_progress begin lemma must_sync_preserved_d: assumes wf: "wf_jvm_prog⇘Φ⇙ P" and ml: "execd_mthr.must_sync P t (xcp, frs) h" and hext: "hext h h'" and hconf': "hconf h'" and cs: "Φ ⊢ t: (xcp, h, frs) √" shows "execd_mthr.must_sync P t (xcp, frs) h'" proof(rule execd_mthr.must_syncI) from ml obtain ta xcp' frs' m' where red: "P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', m', frs')" by(auto elim: execd_mthr.must_syncE) then obtain f Frs where check: "check P (xcp, h, frs)" and exec: "(ta, xcp', m', frs') ∈ exec P t (xcp, h, frs)" and [simp]: "frs = f # Frs" by(auto elim: jvmd_NormalE) from cs hext hconf' have cs': "Φ ⊢ t: (xcp, h', frs) √" by(rule correct_state_hext_mono) then obtain ta σ' where exec: "P,t ⊢ (xcp, h', frs) -ta-jvm→ σ'" by(auto dest: progress[OF wf]) hence "P,t ⊢ Normal (xcp, h', frs) -ta-jvmd→ Normal σ'" unfolding welltyped_commute[OF wf cs'] . moreover from exec have "∃s. exec_mthr.actions_ok s t ta" by(rule exec_ta_satisfiable) ultimately show "∃ta x' m' s. mexecd P t ((xcp, frs), h') ta (x', m') ∧ exec_mthr.actions_ok s t ta" by(cases σ')(fastforce simp del: split_paired_Ex) qed lemma can_sync_devreserp_d: assumes wf: "wf_jvm_prog⇘Φ⇙ P" and cl': "execd_mthr.can_sync P t (xcp, frs) h' L" and cs: "Φ ⊢ t: (xcp, h, frs) √" and hext: "hext h h'" and hconf': "hconf h'" shows "∃L'⊆L. execd_mthr.can_sync P t (xcp, frs) h L'" proof - from cl' obtain ta xcp' frs' m' where red: "P,t ⊢ Normal (xcp, h', frs) -ta-jvmd→ Normal (xcp', m', frs')" and L: "L = collect_locks ⦃ta⦄⇘_{l}⇙ <+> collect_cond_actions ⦃ta⦄⇘_{c}⇙ <+> collect_interrupts ⦃ta⦄⇘_{i}⇙" by -(erule execd_mthr.can_syncE, auto) then obtain f Frs where check: "check P (xcp, h', frs)" and exec: "(ta, xcp', m', frs') ∈ exec P t (xcp, h', frs)" and [simp]: "frs = f # Frs" by(auto elim: jvmd_NormalE simp add: finfun_upd_apply) obtain stk loc C M pc where [simp]: "f = (stk, loc, C, M, pc)" by (cases f, blast) from cs obtain ST LT Ts T mxs mxl ins xt where hconf: "hconf h" and tconf: "P,h ⊢ t √t" and meth: "P ⊢ C sees M:Ts→T = ⌊(mxs, mxl, ins, xt)⌋ in C" and Φ: "Φ C M ! pc = Some (ST,LT)" and frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T Frs" by (fastforce simp add: correct_state_def dest: sees_method_fun) from cs have "exec P t (xcp, h, f # Frs) ≠ {}" by(auto dest!: progress[OF wf] simp add: exec_1_iff) with no_type_error[OF wf cs] have check': "check P (xcp, h, frs)" by(auto simp add: exec_d_def split: if_split_asm) from wf obtain wfmd where wfp: "wf_prog wfmd P" by(auto dest: wt_jvm_progD) from tconf hext have tconf': "P,h' ⊢ t √t" by(rule tconf_hext_mono) show ?thesis proof(cases xcp) case [simp]: (Some a) with exec have [simp]: "m' = h'" by(auto) from ‹Φ ⊢ t: (xcp, h, frs) √› obtain D where D: "typeof_addr h a = ⌊Class_type D⌋" by(auto simp add: correct_state_def) with hext have "cname_of h a = cname_of h' a" by(auto dest: hext_objD simp add: cname_of_def) with exec have "(ta, xcp', h, frs') ∈ exec P t (xcp, h, frs)" by auto moreover from check D hext have "check P (xcp, h, frs)" by(auto simp add: check_def check_xcpt_def dest: hext_objD) ultimately have "P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h, frs')" by -(rule exec_1_d_NormalI, simp only: exec_d_def if_True) with L have "execd_mthr.can_sync P t (xcp, frs) h L" by(auto intro: execd_mthr.can_syncI) thus ?thesis by auto next case [simp]: None note [simp] = defs1 list_all2_Cons2 from frame have ST: "P,h ⊢ stk [:≤] ST" and LT: "P,h ⊢ loc [:≤⇩_{⊤}] LT" and pc: "pc < length ins" by simp_all from wf meth pc have wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" by(rule wt_jvm_prog_impl_wt_instr) from ‹Φ ⊢ t: (xcp, h, frs) √› have "∃ta σ'. P,t ⊢ (xcp, h, f # Frs) -ta-jvm→ σ'" by(auto dest: progress[OF wf] simp del: correct_state_def split_paired_Ex) with exec meth have "∃ta' σ'. (ta', σ') ∈ exec P t (xcp, h, frs) ∧ collect_locks ⦃ta'⦄⇘_{l}⇙ ⊆ collect_locks ⦃ta⦄⇘_{l}⇙ ∧ collect_cond_actions ⦃ta'⦄⇘_{c}⇙ ⊆ collect_cond_actions ⦃ta⦄⇘_{c}⇙ ∧ collect_interrupts ⦃ta'⦄⇘_{i}⇙ ⊆ collect_interrupts ⦃ta⦄⇘_{i}⇙" proof(cases "ins ! pc") case (Invoke M' n) show ?thesis proof(cases "stk ! n = Null") case True with Invoke exec meth show ?thesis by simp next case False with check meth obtain a where a: "stk ! n = Addr a" and n: "n < length stk" by(auto simp add: check_def is_Ref_def Invoke) from frame have stk: "P,h ⊢ stk [:≤] ST" by(auto simp add: conf_f_def) hence "P,h ⊢ stk ! n :≤ ST ! n" using n by(rule list_all2_nthD) with a obtain ao Ta where Ta: "typeof_addr h a = ⌊Ta⌋" by(auto simp add: conf_def) from hext Ta have Ta': "typeof_addr h' a = ⌊Ta⌋" by(rule typeof_addr_hext_mono) with check a meth Invoke False obtain D Ts' T' meth D' where C: "D = class_type_of Ta" and sees': "P ⊢ D sees M':Ts'→T' = meth in D'" and params: "P,h' ⊢ rev (take n stk) [:≤] Ts'" by(auto simp add: check_def has_method_def) show ?thesis proof(cases "meth") case Some with exec meth a Ta Ta' Invoke n sees' C show ?thesis by(simp add: split_beta) next case None with exec meth a Ta Ta' Invoke n sees' C obtain ta' va h'' where ta': "ta = extTA2JVM P ta'" and va: "(xcp', m', frs') = extRet2JVM n h'' stk loc C M pc Frs va" and exec': "(ta', va, h'') ∈ red_external_aggr P t a M' (rev (take n stk)) h'" by(fastforce) from va have [simp]: "h'' = m'" by(cases va) simp_all note Ta moreover from None sees' wfp have "D'∙M'(Ts') :: T'" by(auto intro: sees_wf_native) with C sees' params Ta' None have "P,h' ⊢ a∙M'(rev (take n stk)) : T'" by(auto simp add: external_WT'_iff confs_conv_map) 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 stk have "P,h ⊢ take n stk [:≤] take n ST" by(rule list_all2_takeI) then obtain Ts where "map typeof⇘h⇙ (take n stk) = map Some Ts" by(auto simp add: confs_conv_map) hence "map typeof⇘h⇙ (rev (take n stk)) = map Some (rev Ts)" by(simp only: rev_map[symmetric]) moreover hence "map typeof⇘h'⇙ (rev (take n stk)) = map Some (rev Ts)" using hext by(rule map_typeof_hext_mono) with ‹P,h' ⊢ a∙M'(rev (take n stk)) : T'› ‹D'∙M'(Ts') :: T'› sees' C Ta' Ta have "P ⊢ rev Ts [≤] Ts'" by cases (auto dest: sees_method_fun) ultimately have "P,h ⊢ a∙M'(rev (take n stk)) : T'" using Ta C sees' params None ‹D'∙M'(Ts') :: T'› by(auto simp add: external_WT'_iff confs_conv_map) from red_external_wt_hconf_hext[OF wfp red hext this tconf hconf] obtain ta'' va' h''' where "P,t ⊢ ⟨a∙M'(rev (take n stk)),h⟩ -ta''→ext ⟨va',h'''⟩" and ta'': "collect_locks ⦃ta''⦄⇘_{l}⇙ = collect_locks ⦃ta'⦄⇘_{l}⇙" "collect_cond_actions ⦃ta''⦄⇘_{c}⇙ = collect_cond_actions ⦃ta'⦄⇘_{c}⇙" "collect_interrupts ⦃ta''⦄⇘_{i}⇙ = collect_interrupts ⦃ta'⦄⇘_{i}⇙" by auto with None a Ta Invoke meth Ta' n C sees' have "(extTA2JVM P ta'', extRet2JVM n h''' stk loc C M pc Frs va') ∈ exec P t (xcp, h, frs)" by(force intro: red_external_imp_red_external_aggr simp del: split_paired_Ex) with ta'' ta' show ?thesis by(fastforce simp del: split_paired_Ex) qed qed qed(auto 4 4 split: if_split_asm simp add: split_beta ta_upd_simps exec_1_iff intro: rev_image_eqI simp del: split_paired_Ex) with check' have "∃ta' σ'. P,t ⊢ Normal (xcp, h, frs) -ta'-jvmd→ Normal σ' ∧ collect_locks ⦃ta'⦄⇘_{l}⇙ ⊆ collect_locks ⦃ta⦄⇘_{l}⇙ ∧ collect_cond_actions ⦃ta'⦄⇘_{c}⇙ ⊆ collect_cond_actions ⦃ta⦄⇘_{c}⇙ ∧ collect_interrupts ⦃ta'⦄⇘_{i}⇙ ⊆ collect_interrupts ⦃ta⦄⇘_{i}⇙" apply clarify apply(rule exI conjI)+ apply(rule exec_1_d.exec_1_d_NormalI, auto simp add: exec_d_def) done with L show ?thesis apply - apply(erule exE conjE|rule exI conjI)+ prefer 2 apply(rule_tac x'="(fst σ', snd (snd σ'))" and m'="fst (snd σ')" in execd_mthr.can_syncI) apply auto done qed qed end context JVM_typesafe begin lemma execd_preserve_deadlocked: assumes wf: "wf_jvm_prog⇘Φ⇙ P" shows "preserve_deadlocked JVM_final (mexecd P) convert_RA (correct_jvm_state Φ)" proof(unfold_locales) show "invariant3p (mexecdT P) (correct_jvm_state Φ)" by(rule invariant3p_correct_jvm_state_mexecdT[OF wf]) next fix s t' ta' s' t x ln assume s: "s ∈ correct_jvm_state Φ" and red: "P ⊢ s -t'▹ta'→⇘_{jvmd}⇙ s'" and tst: "thr s t = ⌊(x, ln)⌋" and "execd_mthr.must_sync P t x (shr s)" moreover obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto) ultimately have ml: "execd_mthr.must_sync P t (xcp, frs) (shr s)" by simp moreover from s have cs': "correct_state_ts Φ (thr s) (shr s)" by(simp add: correct_jvm_state_def) with tst have "Φ ⊢ t: (xcp, shr s, frs) √" by(auto dest: ts_okD) moreover from red have "hext (shr s) (shr s')" by(rule execd_hext) moreover from wf red cs' have "correct_state_ts Φ (thr s') (shr s')" by(rule lifting_wf.redT_preserves[OF lifting_wf_correct_state_d]) from red tst have "thr s' t ≠ None" by(cases s)(cases s', rule notI, auto dest: execd_mthr.redT_thread_not_disappear) with ‹correct_state_ts Φ (thr s') (shr s')› have "hconf (shr s')" by(auto dest: ts_okD simp add: correct_state_def) ultimately have "execd_mthr.must_sync P t (xcp, frs) (shr s')" by-(rule must_sync_preserved_d[OF wf]) thus "execd_mthr.must_sync P t x (shr s')" by simp next fix s t' ta' s' t x ln L assume s: "s ∈ correct_jvm_state Φ" and red: "P ⊢ s -t'▹ta'→⇘_{jvmd}⇙ s'" and tst: "thr s t = ⌊(x, ln)⌋" and "execd_mthr.can_sync P t x (shr s') L" moreover obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto) ultimately have ml: "execd_mthr.can_sync P t (xcp, frs) (shr s') L" by simp moreover from s have cs': "correct_state_ts Φ (thr s) (shr s)" by(simp add: correct_jvm_state_def) with tst have "Φ ⊢ t: (xcp, shr s, frs) √" by(auto dest: ts_okD) moreover from red have "hext (shr s) (shr s')" by(rule execd_hext) moreover from red tst have "thr s' t ≠ None" by(cases s)(cases s', rule notI, auto dest: execd_mthr.redT_thread_not_disappear) from red cs' have "correct_state_ts Φ (thr s') (shr s')" by(rule lifting_wf.redT_preserves[OF lifting_wf_correct_state_d[OF wf]]) with ‹thr s' t ≠ None› have "hconf (shr s')" by(auto dest: ts_okD simp add: correct_state_def) ultimately have "∃L' ⊆ L. execd_mthr.can_sync P t (xcp, frs) (shr s) L'" by-(rule can_sync_devreserp_d[OF wf]) thus "∃L' ⊆ L. execd_mthr.can_sync P t x (shr s) L'" by simp qed end text ‹and now everything again for the aggresive VM› context JVM_heap_conf_base' begin lemma must_lock_d_eq_must_lock: "⟦ wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t: (xcp, h, frs) √ ⟧ ⟹ execd_mthr.must_sync P t (xcp, frs) h = exec_mthr.must_sync P t (xcp, frs) h" apply(rule iffI) apply(rule exec_mthr.must_syncI) apply(erule execd_mthr.must_syncE) apply(simp only: mexec_eq_mexecd) apply(blast) apply(rule execd_mthr.must_syncI) apply(erule exec_mthr.must_syncE) apply(simp only: mexec_eq_mexecd[symmetric]) apply(blast) done lemma can_lock_d_eq_can_lock: "⟦ wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t: (xcp, h, frs) √ ⟧ ⟹ execd_mthr.can_sync P t (xcp, frs) h L = exec_mthr.can_sync P t (xcp, frs) h L" apply(rule iffI) apply(erule execd_mthr.can_syncE) apply(rule exec_mthr.can_syncI) apply(simp only: mexec_eq_mexecd) apply(assumption)+ apply(erule exec_mthr.can_syncE) apply(rule execd_mthr.can_syncI) by(simp only: mexec_eq_mexecd) end context JVM_typesafe begin lemma exec_preserve_deadlocked: assumes wf: "wf_jvm_prog⇘Φ⇙ P" shows "preserve_deadlocked JVM_final (mexec P) convert_RA (correct_jvm_state Φ)" proof - interpret preserve_deadlocked JVM_final "mexecd P" convert_RA "correct_jvm_state Φ" by(rule execd_preserve_deadlocked) fact+ { fix s t' ta' s' t x assume s: "s ∈ correct_jvm_state Φ" and red: "P ⊢ s -t'▹ta'→⇘_{jvm}⇙ s'" and tst: "thr s t = ⌊(x, no_wait_locks)⌋" obtain xcp frs where x [simp]: "x = (xcp, frs)" by(cases x, auto) from s have css: "correct_state_ts Φ (thr s) (shr s)" by(simp add: correct_jvm_state_def) with red have redd: "P ⊢ s -t'▹ta'→⇘_{jvmd}⇙ s'" by(simp add: mexecT_eq_mexecdT[OF wf]) from css tst have cst: "Φ ⊢ t: (xcp, shr s, frs) √" by(auto dest: ts_okD) from redd have cst': "Φ ⊢ t: (xcp, shr s', frs) √" proof(cases rule: execd_mthr.redT_elims) case acquire with cst show ?thesis by simp next case (normal X X' M' ws') obtain XCP FRS where X [simp]: "X = (XCP, FRS)" by(cases X, auto) obtain XCP' FRS' where X' [simp]: "X' = (XCP', FRS')" by(cases X', auto) from ‹mexecd P t' (X, shr s) ta' (X', M')› have "P,t' ⊢ Normal (XCP, shr s, FRS) -ta'-jvmd→ Normal (XCP', M', FRS')" by simp moreover from ‹thr s t' = ⌊(X, no_wait_locks)⌋› css have "Φ ⊢ t': (XCP, shr s, FRS) √" by(auto dest: ts_okD) ultimately have "Φ ⊢ t': (XCP, M', FRS) √" by -(rule correct_state_heap_change[OF wf]) moreover from lifting_wf.redT_updTs_preserves[OF lifting_wf_correct_state_d[OF wf] css, OF ‹mexecd P t' (X, shr s) ta' (X', M')› ‹thr s t' = ⌊(X, no_wait_locks)⌋›, of no_wait_locks] ‹thread_oks (thr s) ⦃ta'⦄⇘_{t}⇙› have "correct_state_ts Φ ((redT_updTs (thr s) ⦃ta'⦄⇘_{t}⇙)(t' ↦ (X', no_wait_locks))) M'" by simp ultimately have "correct_state_ts Φ (redT_updTs (thr s) ⦃ta'⦄⇘_{t}⇙) M'" using ‹thr s t' = ⌊(X, no_wait_locks)⌋› ‹thread_oks (thr s) ⦃ta'⦄⇘_{t}⇙› apply(auto intro!: ts_okI dest: ts_okD) apply(case_tac "t=t'") apply(fastforce dest: redT_updTs_Some) apply(drule_tac t=t in ts_okD, fastforce+) done hence "correct_state_ts Φ (redT_updTs (thr s) ⦃ta'⦄⇘_{t}⇙) (shr s')" using ‹s' = (redT_updLs (locks s) t' ⦃ta'⦄⇘_{l}⇙, ((redT_updTs (thr s) ⦃ta'⦄⇘_{t}⇙)(t' ↦ (X', redT_updLns (locks s) t' no_wait_locks ⦃ta'⦄⇘_{l}⇙)), M'), ws', redT_updIs (interrupts s) ⦃ta'⦄⇘_{i}⇙)› by simp moreover from tst ‹thread_oks (thr s) ⦃ta'⦄⇘_{t}⇙› have "redT_updTs (thr s) ⦃ta'⦄⇘_{t}⇙ t = ⌊(x, no_wait_locks)⌋" by(auto intro: redT_updTs_Some) ultimately show ?thesis by(auto dest: ts_okD) qed { assume "exec_mthr.must_sync P t x (shr s)" hence ml: "exec_mthr.must_sync P t (xcp, frs) (shr s)" by simp with cst have "execd_mthr.must_sync P t (xcp, frs) (shr s)" by(auto dest: must_lock_d_eq_must_lock[OF wf]) with s redd tst have "execd_mthr.must_sync P t x (shr s')" unfolding x by(rule can_lock_preserved) with cst' have "exec_mthr.must_sync P t x (shr s')" by(auto dest: must_lock_d_eq_must_lock[OF wf]) } note ml = this { fix L assume "exec_mthr.can_sync P t x (shr s') L" hence cl: "exec_mthr.can_sync P t (xcp, frs) (shr s') L" by simp with cst' have "execd_mthr.can_sync P t (xcp, frs) (shr s') L" by(auto dest: can_lock_d_eq_can_lock[OF wf]) with s redd tst have "∃L' ⊆ L. execd_mthr.can_sync P t x (shr s) L'" unfolding x by(rule can_lock_devreserp) then obtain L' where "execd_mthr.can_sync P t x (shr s) L'" and L': "L'⊆ L" by blast with cst have "exec_mthr.can_sync P t x (shr s) L'" by(auto dest: can_lock_d_eq_can_lock[OF wf]) with L' have "∃L' ⊆ L. exec_mthr.can_sync P t x (shr s) L'" by(blast) } note this ml } moreover have "invariant3p (mexecT P) (correct_jvm_state Φ)" by(rule invariant3p_correct_jvm_state_mexecT[OF wf]) ultimately show ?thesis by(unfold_locales) qed end end