Theory JVMThreaded

(*  Title:      JinjaThreads/JVM/JVMDefensive.thy
    Author:     Andreas Lochbihler
*)

section ‹Instantiating the framework semantics with the JVM›

theory JVMThreaded
imports
  JVMDefensive
  "../Common/ConformThreaded"
  "../Framework/FWLiftingSem"
  "../Framework/FWProgressAux"
begin

primrec JVM_final :: "'addr jvm_thread_state ⇒ bool"
where
  "JVM_final (xcp, frs) = (frs = [])"

text‹The aggressive JVM›

context JVM_heap_base begin

abbreviation mexec :: 
  "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr jvm_thread_state × 'heap)
  ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action ⇒ ('addr jvm_thread_state × 'heap) ⇒ bool"
where
  "mexec P t ≡ (λ((xcp, frstls), h) ta ((xcp', frstls'), h'). P,t ⊢ (xcp, h, frstls) -ta-jvm→ (xcp', h', frstls'))"

lemma NewThread_memory_exec_instr:
  "⟦ (ta, s) ∈ exec_instr I P t h stk loc C M pc frs; NewThread t' x m ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ m = fst (snd s)"
apply(cases I)
apply(auto split: if_split_asm simp add: split_beta ta_upd_simps)
apply(auto dest!: red_ext_aggr_new_thread_heap simp add: extRet2JVM_def split: extCallRet.split)
done

lemma NewThread_memory_exec:
  "⟦ P,t ⊢ σ -ta-jvm→ σ'; NewThread t' x m ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ m = (fst (snd σ'))"
apply(erule exec_1.cases)
apply(clarsimp)
apply(case_tac bb, simp)
apply(case_tac ag, auto simp add: exception_step_def_raw split: list.split_asm)
apply(drule NewThread_memory_exec_instr, simp+)
done

lemma exec_instr_Wakeup_no_Lock_no_Join_no_Interrupt:
  "⟦ (ta, s) ∈ exec_instr I P t h stk loc C M pc frs; Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙ ⟧
  ⟹ collect_locks ⦃ta⦄⇘l⇙ = {} ∧ collect_cond_actions ⦃ta⦄⇘c⇙ = {} ∧ collect_interrupts ⦃ta⦄⇘i⇙ = {}"
apply(cases I)
apply(auto split: if_split_asm simp add: split_beta ta_upd_simps dest: red_external_aggr_Wakeup_no_Join)
done

lemma mexec_instr_Wakeup_no_Join:
  "⟦ P,t ⊢ σ -ta-jvm→ σ'; Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙ ⟧
  ⟹ collect_locks ⦃ta⦄⇘l⇙ = {} ∧ collect_cond_actions ⦃ta⦄⇘c⇙ = {} ∧ collect_interrupts ⦃ta⦄⇘i⇙ = {}"
apply(erule exec_1.cases)
apply(clarsimp)
apply(case_tac bb, simp)
apply(case_tac ag, clarsimp simp add: exception_step_def_raw split: list.split_asm del: disjE)
apply(drule exec_instr_Wakeup_no_Lock_no_Join_no_Interrupt)
apply auto
done

lemma mexec_final: 
  "⟦ mexec P t (x, m) ta (x', m'); JVM_final x ⟧ ⟹ False"
by(cases x)(auto simp add: exec_1_iff)

lemma exec_mthr: "multithreaded JVM_final (mexec P)"
apply(unfold_locales)
apply(clarsimp, drule NewThread_memory_exec, fastforce, simp)
apply(erule (1) mexec_final)
done

end

sublocale JVM_heap_base < exec_mthr: 
  multithreaded
    JVM_final
    "mexec P"
    convert_RA
  for P
by(rule exec_mthr)

context JVM_heap_base begin

abbreviation mexecT ::
  "'addr jvm_prog
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state
  ⇒ 'thread_id × ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state ⇒ bool"
where
  "mexecT P ≡ exec_mthr.redT P"

abbreviation mexecT_syntax1 ::
  "'addr jvm_prog ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state
  ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state ⇒ bool"
  (‹_ ⊢ _ -_▹_→⇘jvm⇙ _› [50,0,0,0,50] 80)
where
  "mexecT_syntax1 P s t ta s' ≡ mexecT P s (t, ta) s'"


abbreviation mExecT_syntax1 :: 
  "'addr jvm_prog ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state
  ⇒ ('thread_id × ('addr, 'thread_id, 'heap) jvm_thread_action) list
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state ⇒ bool"
  (‹_ ⊢ _ -▹_→⇘jvm⇙* _› [50,0,0,50] 80)
where
  "P ⊢ s -▹ttas→⇘jvm⇙* s' ≡ exec_mthr.RedT P s ttas s'"

text‹The defensive JVM›

abbreviation mexecd :: 
  "'addr jvm_prog ⇒ 'thread_id ⇒ 'addr jvm_thread_state × 'heap 
  ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action ⇒ 'addr jvm_thread_state × 'heap ⇒ bool"
where
  "mexecd P t ≡ (λ((xcp, frstls), h) ta ((xcp', frstls'), h'). P,t ⊢ Normal (xcp, h, frstls) -ta-jvmd→ Normal (xcp', h', frstls'))"

lemma execd_mthr: "multithreaded JVM_final (mexecd P)"
apply(unfold_locales)
 apply(fastforce dest: defensive_imp_aggressive_1 NewThread_memory_exec)
apply(auto elim: jvmd_NormalE)
done

end

sublocale JVM_heap_base < execd_mthr:
  multithreaded
    JVM_final
    "mexecd P"
    convert_RA
  for P
by(rule execd_mthr)

context JVM_heap_base begin

abbreviation mexecdT ::
  "'addr jvm_prog ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state
  ⇒ 'thread_id × ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state ⇒ bool"
where
  "mexecdT P ≡ execd_mthr.redT P"


abbreviation mexecdT_syntax1 ::
  "'addr jvm_prog ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state
  ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state ⇒ bool"
  (‹_ ⊢ _ -_▹_→⇘jvmd⇙ _› [50,0,0,0,50] 80)
where
  "mexecdT_syntax1 P s t ta s' ≡ mexecdT P s (t, ta) s'"

abbreviation mExecdT_syntax1 ::
  "'addr jvm_prog ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state
  ⇒ ('thread_id × ('addr, 'thread_id, 'heap) jvm_thread_action) list
  ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state ⇒ bool"
  (‹_ ⊢ _ -▹_→⇘jvmd⇙* _› [50,0,0,50] 80)
where
  "P ⊢ s -▹ttas→⇘jvmd⇙* s' ≡ execd_mthr.RedT P s ttas s'"

lemma mexecd_Suspend_Invoke:
  "⟦ mexecd P t (x, m) ta (x', m'); Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧
  ⟹ ∃stk loc C M pc frs' n a T Ts Tr D. x' = (None, (stk, loc, C, M, pc) # frs') ∧ instrs_of P C M ! pc = Invoke wait n ∧ stk ! n = Addr a ∧ typeof_addr m a = ⌊T⌋ ∧ P ⊢ class_type_of T sees wait:Ts→Tr = Native in D ∧ D∙wait(Ts) :: Tr"
apply(cases x')
apply(cases x)
apply(cases "fst x")
apply(auto elim!: jvmd_NormalE simp add: split_beta)
apply(rename_tac [!] stk loc C M pc frs)
apply(case_tac [!] "instrs_of P C M ! pc")
apply(auto split: if_split_asm simp add: split_beta check_def is_Ref_def has_method_def)
apply(frule red_external_aggr_Suspend_StaySame, simp, drule red_external_aggr_Suspend_waitD, simp, fastforce)+
done

end

context JVM_heap begin

lemma exec_instr_New_Thread_exists_thread_object:
  "⟦ (ta, xcp', h', frs') ∈ exec_instr ins P t h stk loc C M pc frs;
     check_instr ins P h stk loc C M pc frs;
     NewThread t' x h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
  ⟹ ∃C. typeof_addr h' (thread_id2addr t') = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread"
apply(cases ins)
apply(fastforce simp add: split_beta ta_upd_simps split: if_split_asm intro: red_external_aggr_new_thread_exists_thread_object)+
done

lemma exec_New_Thread_exists_thread_object:
  "⟦ P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs'); NewThread t' x h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
  ⟹ ∃C. typeof_addr h' (thread_id2addr t') = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread"
apply(cases xcp)
apply(case_tac [!] frs)
apply(auto simp add: check_def elim!: jvmd_NormalE dest!: exec_instr_New_Thread_exists_thread_object)
done

lemma exec_instr_preserve_tconf:
  "⟦ (ta, xcp', h', frs') ∈ exec_instr ins P t h stk loc C M pc frs;
     check_instr ins P h stk loc C M pc frs;
     P,h ⊢ t' √t ⟧
  ⟹ P,h' ⊢ t' √t"
apply(cases ins)
apply(auto intro: tconf_hext_mono hext_allocate hext_heap_write red_external_aggr_preserves_tconf split: if_split_asm sum.split_asm simp add: split_beta has_method_def intro!: is_native.intros cong del: image_cong_simp)
done

lemma exec_preserve_tconf:
  "⟦ P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs'); P,h ⊢ t' √t ⟧ ⟹ P,h' ⊢ t' √t"
apply(cases xcp)
apply(case_tac [!] frs)
apply(auto simp add: check_def elim!: jvmd_NormalE elim!: exec_instr_preserve_tconf)
done

lemma lifting_wf_thread_conf: "lifting_wf JVM_final (mexecd P) (λt x m. P,m ⊢ t √t)"
by(unfold_locales)(auto intro: exec_preserve_tconf dest: exec_New_Thread_exists_thread_object intro: tconfI)

end

sublocale JVM_heap < execd_tconf: lifting_wf JVM_final "mexecd P" convert_RA "λt x m. P,m ⊢ t √t"
by(rule lifting_wf_thread_conf)

context JVM_heap begin

lemma execd_hext:
  "P ⊢ s -t▹ta→⇘jvmd⇙ s' ⟹ shr s ⊴ shr s'"
by(auto elim!: execd_mthr.redT.cases dest!: exec_1_d_hext intro: hext_trans)

lemma Execd_hext:
  assumes "P ⊢ s -▹tta→⇘jvmd⇙* s'"
  shows "shr s ⊴ shr s'"
using assms unfolding execd_mthr.RedT_def
by(induct)(auto dest!: execd_hext intro: hext_trans simp add: execd_mthr.RedT_def)

end

end