Theory DRF_JVM
section ‹JMM Instantiation for bytecode›
theory DRF_JVM
imports
JMM_Common
JMM_JVM
"../BV/BVProgressThreaded"
SC_Legal
begin
subsection ‹DRF guarantee for the JVM›
abbreviation (input) ka_xcp :: "'addr option ⇒ 'addr set"
where "ka_xcp ≡ set_option"
primrec jvm_ka :: "'addr jvm_thread_state ⇒ 'addr set"
where
"jvm_ka (xcp, frs) =
ka_xcp xcp ∪ (⋃(stk, loc, C, M, pc) ∈ set frs. (⋃v ∈ set stk. ka_Val v) ∪ (⋃v ∈ set loc. ka_Val v))"
context heap begin
lemma red_external_aggr_read_mem_typeable:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ∃T'. P,h ⊢ ad@al : T'"
by(auto simp add: red_external_aggr_def split_beta split: if_split_asm dest: heap_clone_read_typeable)
end
context JVM_heap_base begin
definition jvm_known_addrs :: "'thread_id ⇒ 'addr jvm_thread_state ⇒ 'addr set"
where "jvm_known_addrs t xcpfrs = {thread_id2addr t} ∪ jvm_ka xcpfrs ∪ set start_addrs"
end
context JVM_heap begin
lemma exec_instr_known_addrs:
assumes ok: "start_heap_ok"
and exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
shows "jvm_known_addrs t (xcp', frs') ⊆ jvm_known_addrs t (None, (stk, loc, C, M, pc) # frs) ∪ new_obs_addrs ⦃ta⦄⇘o⇙"
proof -
note [simp] = jvm_known_addrs_def new_obs_addrs_def addr_of_sys_xcpt_start_addr[OF ok] subset_Un1 subset_Un2 subset_insert ka_Val_subset_new_obs_Addr_ReadMem SUP_subset_mono split_beta neq_Nil_conv tl_conv_drop set_drop_subset is_Ref_def
from exec check show ?thesis
proof(cases "i")
case Load with exec check show ?thesis by auto
next
case (Store V) with exec check show ?thesis
using set_update_subset_insert[of loc V]
by(clarsimp simp del: set_update_subsetI) blast
next
case (Push v)
with check have "ka_Val v = {}" by(cases v) simp_all
with Push exec check show ?thesis by(simp)
next
case (CAS F D)
then show ?thesis using exec check
by(clarsimp split: if_split_asm)(fastforce dest!: in_set_dropD)+
next
case (Invoke M' n)
show ?thesis
proof(cases "stk ! n = Null")
case True with exec check Invoke show ?thesis by(simp)
next
case [simp]: False
with check Invoke obtain a where stkn: "stk ! n = Addr a" "n < length stk" by auto
hence a: "a ∈ (⋃v ∈ set stk. ka_Val v)" by(fastforce dest: nth_mem)
show ?thesis
proof(cases "snd (snd (snd (method P (class_type_of (the (typeof_addr h (the_Addr (stk ! n))))) M'))) = Native")
case True
with exec check Invoke a stkn show ?thesis
apply clarsimp
apply(drule red_external_aggr_known_addrs_mono[OF ok], simp)
apply(auto dest!: in_set_takeD dest: bspec subsetD split: extCallRet.split_asm simp add: has_method_def is_native.simps)
done
next
case False
with exec check Invoke a stkn show ?thesis
by(auto simp add: set_replicate_conv_if dest!: in_set_takeD)
qed
qed
next
case Swap with exec check show ?thesis
by(cases stk)(simp, case_tac list, auto)
next
case (BinOpInstr bop) with exec check show ?thesis
using binop_known_addrs[OF ok, of bop "hd (drop (Suc 0) stk)" "hd stk"]
apply(cases stk)
apply(simp, case_tac list, simp)
apply clarsimp
apply(drule (2) binop_progress)
apply(auto 6 2 split: sum.split_asm)
done
next
case MExit with exec check show ?thesis by(auto split: if_split_asm)
qed(clarsimp split: if_split_asm)+
qed
lemma exec_d_known_addrs_mono:
assumes ok: "start_heap_ok"
and exec: "mexecd P t (xcpfrs, h) ta (xcpfrs', h')"
shows "jvm_known_addrs t xcpfrs' ⊆ jvm_known_addrs t xcpfrs ∪ new_obs_addrs ⦃ta⦄⇘o⇙"
using exec
apply(cases xcpfrs)
apply(cases xcpfrs')
apply(simp add: split_beta)
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(fastforce simp add: check_def split_beta del: subsetI dest!: exec_instr_known_addrs[OF ok])
apply(fastforce simp add: jvm_known_addrs_def split_beta dest!: in_set_dropD)
done
lemma exec_instr_known_addrs_ReadMem:
assumes exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
and read: "ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙"
shows "ad ∈ jvm_known_addrs t (None, (stk, loc, C, M, pc) # frs)"
using assms
proof(cases i)
case ALoad thus ?thesis using assms
by(cases stk)(case_tac [2] list, auto simp add: split_beta is_Ref_def jvm_known_addrs_def split: if_split_asm)
next
case (Invoke M n)
with check have "stk ! n ≠ Null ⟶ the_Addr (stk ! n) ∈ ka_Val (stk ! n)" "stk ! n ∈ set stk"
by(auto simp add: is_Ref_def)
with assms Invoke show ?thesis
by(auto simp add: split_beta is_Ref_def simp del: ka_Val.simps nth_mem split: if_split_asm dest!: red_external_aggr_known_addrs_ReadMem in_set_takeD del: is_AddrE)(auto simp add: jvm_known_addrs_def simp del: ka_Val.simps nth_mem del: is_AddrE)
next
case Getfield thus ?thesis using assms
by(auto simp add: jvm_known_addrs_def neq_Nil_conv is_Ref_def split: if_split_asm)
next
case CAS thus ?thesis using assms
apply(cases stk; simp)
subgoal for v stk
apply(cases stk; simp)
subgoal for v stk
by(cases stk)(auto split: if_split_asm simp add: jvm_known_addrs_def is_Ref_def)
done
done
qed(auto simp add: split_beta is_Ref_def neq_Nil_conv split: if_split_asm)
lemma mexecd_known_addrs_ReadMem:
"⟦ mexecd P t (xcpfrs, h) ta (xcpfrs', h'); ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ad ∈ jvm_known_addrs t xcpfrs"
apply(cases xcpfrs)
apply(cases xcpfrs')
apply simp
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(auto simp add: check_def dest: exec_instr_known_addrs_ReadMem)
done
lemma exec_instr_known_addrs_WriteMem:
assumes exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
and "write": "⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr a)" "n < length ⦃ta⦄⇘o⇙"
shows "a ∈ jvm_known_addrs t (None, (stk, loc, C, M, pc) # frs) ∨ a ∈ new_obs_addrs (take n ⦃ta⦄⇘o⇙)"
using assms
proof(cases i)
case (Invoke M n)
with check have "stk ! n ≠ Null ⟶ the_Addr (stk ! n) ∈ ka_Val (stk ! n)" "stk ! n ∈ set stk"
by(auto simp add: is_Ref_def)
thus ?thesis using assms Invoke
by(auto simp add: is_Ref_def split_beta split: if_split_asm simp del: ka_Val.simps nth_mem dest!: red_external_aggr_known_addrs_WriteMem in_set_takeD del: is_AddrE)(auto simp add: jvm_known_addrs_def del: is_AddrE)
next
case AStore with assms show ?thesis
by(cases stk)(auto simp add: jvm_known_addrs_def split: if_split_asm)
next
case Putfield with assms show ?thesis
by(cases stk)(auto simp add: jvm_known_addrs_def split: if_split_asm)
next
case CAS with assms show ?thesis
apply(cases stk; simp)
subgoal for v stk
apply(cases stk; simp)
subgoal for v stk
by(cases stk)(auto split: if_split_asm simp add: take_Cons' jvm_known_addrs_def)
done
done
qed(auto simp add: split_beta split: if_split_asm)
lemma mexecd_known_addrs_WriteMem:
"⟦ mexecd P t (xcpfrs, h) ta (xcpfrs', h'); ⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr a); n < length ⦃ta⦄⇘o⇙ ⟧
⟹ a ∈ jvm_known_addrs t xcpfrs ∨ a ∈ new_obs_addrs (take n ⦃ta⦄⇘o⇙)"
apply(cases xcpfrs)
apply(cases xcpfrs')
apply simp
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(auto simp add: check_def dest: exec_instr_known_addrs_WriteMem)
done
lemma exec_instr_known_addrs_new_thread:
assumes exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
and new: "NewThread t' x' h'' ∈ set ⦃ta⦄⇘t⇙"
shows "jvm_known_addrs t' x' ⊆ jvm_known_addrs t (None, (stk, loc, C, M, pc) # frs)"
using assms
proof(cases i)
case (Invoke M n)
with assms have "stk ! n ≠ Null ⟶ the_Addr (stk ! n) ∈ ka_Val (stk ! n) ∧ thread_id2addr (addr2thread_id (the_Addr (stk ! n))) = the_Addr (stk ! n)" "stk ! n ∈ set stk"
apply(auto simp add: is_Ref_def split: if_split_asm)
apply(frule red_external_aggr_NewThread_idD, simp, simp)
apply(drule red_external_aggr_new_thread_sub_thread)
apply(auto intro: addr2thread_id_inverse)
done
with assms Invoke show ?thesis
apply(auto simp add: is_Ref_def split_beta split: if_split_asm simp del: nth_mem del: is_AddrE)
apply(drule red_external_aggr_NewThread_idD)
apply(auto simp add: extNTA2JVM_def jvm_known_addrs_def split_beta simp del: nth_mem del: is_AddrE)
done
qed(auto simp add: split_beta split: if_split_asm)
lemma mexecd_known_addrs_new_thread:
"⟦ mexecd P t (xcpfrs, h) ta (xcpfrs', h'); NewThread t' x' h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ jvm_known_addrs t' x' ⊆ jvm_known_addrs t xcpfrs"
apply(cases xcpfrs)
apply(cases xcpfrs')
apply simp
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(auto 4 3 simp add: check_def dest: exec_instr_known_addrs_new_thread)
done
lemma exec_instr_New_same_addr_same:
"⟦ (ta, xcp', h', frs') ∈ exec_instr ins P t h stk loc C M pc frs;
⦃ta⦄⇘o⇙ ! i = NewHeapElem a x; i < length ⦃ta⦄⇘o⇙;
⦃ta⦄⇘o⇙ ! j = NewHeapElem a x'; j < length ⦃ta⦄⇘o⇙ ⟧
⟹ i = j"
apply(cases ins)
apply(auto simp add: nth_Cons' split: prod.split_asm if_split_asm)
apply(auto split: extCallRet.split_asm dest: red_external_aggr_New_same_addr_same)
done
lemma exec_New_same_addr_same:
"⟦ (ta, xcp', h', frs') ∈ exec P t (xcp, h, frs);
⦃ta⦄⇘o⇙ ! i = NewHeapElem a x; i < length ⦃ta⦄⇘o⇙;
⦃ta⦄⇘o⇙ ! j = NewHeapElem a x'; j < length ⦃ta⦄⇘o⇙ ⟧
⟹ i = j"
apply(cases "(P, t, xcp, h, frs)" rule: exec.cases)
apply(auto dest: exec_instr_New_same_addr_same)
done
lemma exec_1_d_New_same_addr_same:
"⟦ P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs');
⦃ta⦄⇘o⇙ ! i = NewHeapElem a x; i < length ⦃ta⦄⇘o⇙;
⦃ta⦄⇘o⇙ ! j = NewHeapElem a x'; j < length ⦃ta⦄⇘o⇙ ⟧
⟹ i = j"
by(erule jvmd_NormalE)(rule exec_New_same_addr_same)
end
locale JVM_allocated_heap = allocated_heap +
constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
and P :: "'addr jvm_prog"
sublocale JVM_allocated_heap < JVM_heap
by(unfold_locales)
context JVM_allocated_heap begin
lemma exec_instr_allocated_mono:
"⟦ (ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs; check_instr i P h stk loc C M pc frs ⟧
⟹ allocated h ⊆ allocated h'"
apply(cases i)
apply(auto 4 4 simp add: split_beta has_method_def is_native.simps split: if_split_asm sum.split_asm intro: allocate_allocated_mono dest: heap_write_allocated_same dest!: red_external_aggr_allocated_mono del: subsetI)
done
lemma mexecd_allocated_mono:
"mexecd P t (xcpfrs, h) ta (xcpfrs', h') ⟹ allocated h ⊆ allocated h'"
apply(cases xcpfrs)
apply(cases xcpfrs')
apply(simp)
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(auto del: subsetI simp add: check_def dest: exec_instr_allocated_mono)
done
lemma exec_instr_allocatedD:
"⟦ (ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs;
check_instr i P h stk loc C M pc frs; NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ad ∈ allocated h' ∧ ad ∉ allocated h"
apply(cases i)
apply(auto 4 4 split: if_split_asm prod.split_asm dest: allocate_allocatedD dest!: red_external_aggr_allocatedD simp add: has_method_def is_native.simps)
done
lemma mexecd_allocatedD:
"⟦ mexecd P t (xcpfrs, h) ta (xcpfrs', h'); NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ad ∈ allocated h' ∧ ad ∉ allocated h"
apply(cases xcpfrs)
apply(cases xcpfrs')
apply(simp)
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(auto del: subsetI dest: exec_instr_allocatedD simp add: check_def)
done
lemma exec_instr_NewHeapElemD:
"⟦ (ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs; check_instr i P h stk loc C M pc frs;
ad ∈ allocated h'; ad ∉ allocated h ⟧
⟹ ∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
apply(cases i)
apply(auto 4 3 split: if_split_asm prod.split_asm sum.split_asm dest: allocate_allocatedD heap_write_allocated_same dest!: red_external_aggr_NewHeapElemD simp add: is_native.simps has_method_def)
done
lemma mexecd_NewHeapElemD:
"⟦ mexecd P t (xcpfrs, h) ta (xcpfrs', h'); ad ∈ allocated h'; ad ∉ allocated h ⟧
⟹ ∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
apply(cases xcpfrs)
apply(cases xcpfrs')
apply(simp)
apply(erule jvmd_NormalE)
apply(cases "fst xcpfrs")
apply(auto dest: exec_instr_NewHeapElemD simp add: check_def)
done
lemma mexecd_allocated_multithreaded:
"allocated_multithreaded addr2thread_id thread_id2addr empty_heap allocate typeof_addr heap_write allocated JVM_final (mexecd P) P"
proof
fix t x m ta x' m'
assume "mexecd P t (x, m) ta (x', m')"
thus "allocated m ⊆ allocated m'" by(rule mexecd_allocated_mono)
next
fix x t m ta x' m' ad CTn
assume "mexecd P t (x, m) ta (x', m')"
and "NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
thus "ad ∈ allocated m' ∧ ad ∉ allocated m" by(rule mexecd_allocatedD)
next
fix t x m ta x' m' ad
assume "mexecd P t (x, m) ta (x', m')"
and "ad ∈ allocated m'" "ad ∉ allocated m"
thus "∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙" by(rule mexecd_NewHeapElemD)
next
fix t x m ta x' m' i a CTn j CTn'
assume "mexecd P t (x, m) ta (x', m')"
and "⦃ta⦄⇘o⇙ ! i = NewHeapElem a CTn" "i < length ⦃ta⦄⇘o⇙"
and "⦃ta⦄⇘o⇙ ! j = NewHeapElem a CTn'" "j < length ⦃ta⦄⇘o⇙"
thus "i = j" by(auto dest: exec_1_d_New_same_addr_same simp add: split_beta)
qed
end
sublocale JVM_allocated_heap < execd_mthr: allocated_multithreaded
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write allocated
JVM_final "mexecd P"
P
by(rule mexecd_allocated_multithreaded)
context JVM_allocated_heap begin
lemma mexecd_known_addrs:
assumes wf: "wf_prog wfmd P"
and ok: "start_heap_ok"
shows "known_addrs addr2thread_id thread_id2addr empty_heap allocate typeof_addr heap_write allocated jvm_known_addrs JVM_final (mexecd P) P"
proof
fix t x m ta x' m'
assume "mexecd P t (x, m) ta (x', m')"
thus "jvm_known_addrs t x' ⊆ jvm_known_addrs t x ∪ new_obs_addrs ⦃ta⦄⇘o⇙"
by(rule exec_d_known_addrs_mono[OF ok])
next
fix t x m ta x' m' t' x'' m''
assume "mexecd P t (x, m) ta (x', m')"
and "NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
thus "jvm_known_addrs t' x'' ⊆ jvm_known_addrs t x" by(rule mexecd_known_addrs_new_thread)
next
fix t x m ta x' m' ad al v
assume "mexecd P t (x, m) ta (x', m')"
and "ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙"
thus "ad ∈ jvm_known_addrs t x" by(rule mexecd_known_addrs_ReadMem)
next
fix t x m ta x' m' n ad al ad'
assume "mexecd P t (x, m) ta (x', m')"
and "⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr ad')" "n < length ⦃ta⦄⇘o⇙"
thus "ad' ∈ jvm_known_addrs t x ∨ ad' ∈ new_obs_addrs (take n ⦃ta⦄⇘o⇙)"
by(rule mexecd_known_addrs_WriteMem)
qed
end
context JVM_heap begin
lemma exec_instr_read_typeable:
assumes exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
and read: "ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙"
shows "∃T'. P,h ⊢ ad@al : T'"
using exec check read
proof(cases i)
case ALoad
with assms show ?thesis
by(fastforce simp add: split_beta is_Ref_def nat_less_iff word_sless_alt intro: addr_loc_type.intros split: if_split_asm)
next
case (Getfield F D)
with assms show ?thesis
by(clarsimp simp add: split_beta is_Ref_def split: if_split_asm)(blast intro: addr_loc_type.intros dest: has_visible_field has_field_mono)
next
case (Invoke M n)
with exec check read obtain a vs ta' va T
where "(ta', va, h') ∈ red_external_aggr P t a M vs h"
and "ReadMem ad al v ∈ set ⦃ta'⦄⇘o⇙"
by(auto split: if_split_asm simp add: is_Ref_def)
thus ?thesis by(rule red_external_aggr_read_mem_typeable)
next
case (CAS F D)
with assms show ?thesis
by(clarsimp simp add: split_beta is_Ref_def conf_def split: if_split_asm)
(force intro: addr_loc_type.intros dest: has_visible_field[THEN has_field_mono])
qed(auto simp add: split_beta is_Ref_def split: if_split_asm)
lemma exec_1_d_read_typeable:
"⟦ P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs');
ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ ∃T'. P,h ⊢ ad@al : T'"
apply(erule jvmd_NormalE)
apply(cases "(P, t, xcp, h, frs)" rule: exec.cases)
apply(auto intro: exec_instr_read_typeable simp add: check_def)
done
end
sublocale JVM_heap_base < execd_mthr:
if_multithreaded
JVM_final
"mexecd P"
convert_RA
for P
by(unfold_locales)
context JVM_heap_conf begin
lemma JVM_conf_read_heap_read_typed:
"JVM_conf_read addr2thread_id thread_id2addr empty_heap allocate typeof_addr (heap_read_typed P) heap_write hconf P"
proof -
interpret conf: heap_conf_read
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr "heap_read_typed P" heap_write hconf
P
by(rule heap_conf_read_heap_read_typed)
show ?thesis by(unfold_locales)
qed
lemma exec_instr_New_typeof_addrD:
"⟦ (ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs;
check_instr i P h stk loc C M pc frs; hconf h;
NewHeapElem a x ∈ set ⦃ta⦄⇘o⇙ ⟧
⟹ typeof_addr h' a = Some x"
apply(cases i)
apply(auto dest: allocate_SomeD split: prod.split_asm if_split_asm)
apply(auto 4 4 split: extCallRet.split_asm dest!: red_external_aggr_New_typeof_addrD simp add: has_method_def is_native.simps)
done
lemma exec_1_d_New_typeof_addrD:
"⟦ P,t ⊢ Normal (xcp, h, frs) -ta-jvmd→ Normal (xcp', h', frs'); NewHeapElem a x ∈ set ⦃ta⦄⇘o⇙; hconf h ⟧
⟹ typeof_addr h' a = Some x"
apply(erule jvmd_NormalE)
apply(cases "xcp")
apply(auto dest: exec_instr_New_typeof_addrD simp add: check_def)
done
lemma exec_instr_non_speculative_typeable:
assumes exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
and sc: "non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙))"
and vs_conf: "vs_conf P h vs"
and hconf: "hconf h"
shows "(ta, xcp', h', frs') ∈ JVM_heap_base.exec_instr addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_read_typed P) heap_write i P t h stk loc C M pc frs"
proof -
note [simp] = JVM_heap_base.exec_instr.simps
and [split] = if_split_asm prod.split_asm sum.split_asm
and [split del] = if_split
from assms show "?thesis"
proof(cases i)
case ALoad with assms show ?thesis
by(auto 4 3 intro!: heap_read_typedI dest: vs_confD addr_loc_type_fun)
next
case Getfield with assms show ?thesis
by(auto 4 3 intro!: heap_read_typedI dest: vs_confD addr_loc_type_fun)
next
case CAS with assms show ?thesis
by(auto 4 3 intro!: heap_read_typedI dest: vs_confD addr_loc_type_fun)
next
case Invoke with assms show ?thesis
by(fastforce dest: red_external_aggr_non_speculative_typeable simp add: has_method_def is_native.simps)
qed(auto)
qed
lemma exec_instr_non_speculative_vs_conf:
assumes exec: "(ta, xcp', h', frs') ∈ exec_instr i P t h stk loc C M pc frs"
and check: "check_instr i P h stk loc C M pc frs"
and sc: "non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
and vs_conf: "vs_conf P h vs"
and hconf: "hconf h"
shows "vs_conf P h' (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
proof -
note [simp] = JVM_heap_base.exec_instr.simps take_Cons'
and [split] = if_split_asm prod.split_asm sum.split_asm
and [split del] = if_split
from assms show ?thesis
proof(cases i)
case New with assms show ?thesis
by(auto 4 4 dest: hext_allocate vs_conf_allocate intro: vs_conf_hext)
next
case NewArray with assms show ?thesis
by(auto 4 4 dest: hext_allocate vs_conf_allocate intro: vs_conf_hext cong: if_cong)
next
case Invoke with assms show ?thesis
by(fastforce dest: red_external_aggr_non_speculative_vs_conf simp add: has_method_def is_native.simps)
next
case AStore
{
assume "hd (tl (tl stk)) ≠ Null"
and "¬ the_Intg (hd (tl stk)) <s 0"
and "¬ int (alen_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))) ≤ sint (the_Intg (hd (tl stk)))"
and "P ⊢ the (typeof⇘h⇙ (hd stk)) ≤ the_Array (ty_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk)))))))"
moreover hence "nat (sint (the_Intg (hd (tl stk)))) < alen_of_htype (the (typeof_addr h (the_Addr (hd (tl (tl stk))))))"
by(auto simp add: not_le nat_less_iff word_sle_eq word_sless_eq not_less)
with assms AStore have "nat (sint (the_Intg (hd (tl stk)))) < alen_of_htype (the (typeof_addr h' (the_Addr (hd (tl (tl stk))))))"
by(auto dest!: hext_arrD hext_heap_write)
ultimately have "∃T. P,h' ⊢ the_Addr (hd (tl (tl stk)))@ACell (nat (sint (the_Intg (hd (tl stk))))) : T ∧ P,h' ⊢ hd stk :≤ T"
using assms AStore
by(auto 4 4 simp add: is_Ref_def conf_def dest!: hext_heap_write dest: hext_arrD intro!: addr_loc_type.intros intro: typeof_addr_hext_mono type_of_hext_type_of) }
thus ?thesis using assms AStore
by(auto intro!: vs_confI)(blast intro: addr_loc_type_hext_mono conf_hext dest: hext_heap_write vs_confD)+
next
case Putfield
show ?thesis using assms Putfield
by(auto intro!: vs_confI dest!: hext_heap_write)(blast intro: addr_loc_type.intros addr_loc_type_hext_mono typeof_addr_hext_mono has_field_mono[OF has_visible_field] conf_hext dest: vs_confD)+
next
case CAS
show ?thesis using assms CAS
by(auto intro!: vs_confI dest!: hext_heap_write)(blast intro: addr_loc_type.intros addr_loc_type_hext_mono typeof_addr_hext_mono has_field_mono[OF has_visible_field] conf_hext dest: vs_confD)+
qed(auto)
qed
lemma mexecd_non_speculative_typeable:
"⟦ P,t ⊢ Normal (xcp, h, stk) -ta-jvmd→ Normal (xcp', h', frs'); non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙));
vs_conf P h vs; hconf h ⟧
⟹ JVM_heap_base.exec_1_d addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_read_typed P) heap_write P t (Normal (xcp, h, stk)) ta (Normal (xcp', h', frs'))"
apply(erule jvmd_NormalE)
apply(cases xcp)
apply(auto intro!: JVM_heap_base.exec_1_d.intros simp add: JVM_heap_base.exec_d_def check_def JVM_heap_base.exec.simps intro: exec_instr_non_speculative_typeable)
done
lemma mexecd_non_speculative_vs_conf:
"⟦ P,t ⊢ Normal (xcp, h, stk) -ta-jvmd→ Normal (xcp', h', frs');
non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙)));
vs_conf P h vs; hconf h ⟧
⟹ vs_conf P h' (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
apply(erule jvmd_NormalE)
apply(cases xcp)
apply(auto intro!: JVM_heap_base.exec_1_d.intros simp add: JVM_heap_base.exec_d_def check_def JVM_heap_base.exec.simps intro: exec_instr_non_speculative_vs_conf)
done
end
locale JVM_allocated_heap_conf =
JVM_heap_conf
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write hconf
P
+
JVM_allocated_heap
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated
P
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and hconf :: "'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
and P :: "'addr jvm_prog"
begin
lemma mexecd_known_addrs_typing:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and ok: "start_heap_ok"
shows "known_addrs_typing addr2thread_id thread_id2addr empty_heap allocate typeof_addr heap_write allocated jvm_known_addrs JVM_final (mexecd P) (λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √) P"
proof -
from wf obtain wf_md where "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
then
interpret known_addrs
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated jvm_known_addrs
JVM_final "mexecd P" P
using ok by(rule mexecd_known_addrs)
show ?thesis
proof
fix t x m ta x' m'
assume "mexecd P t (x, m) ta (x', m')"
thus "m ⊴ m'" by(auto simp add: split_beta intro: exec_1_d_hext)
next
fix t x m ta x' m' vs
assume exec: "mexecd P t (x, m) ta (x', m')"
and ts_ok: "(λ(xcp, frstls) h. Φ ⊢ t:(xcp, h, frstls) √) x m"
and vs: "vs_conf P m vs"
and ns: "non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙))"
let ?mexecd = "JVM_heap_base.mexecd addr2thread_id thread_id2addr spurious_wakeups empty_heap allocate typeof_addr (heap_read_typed P) heap_write P"
have lift: "lifting_wf JVM_final ?mexecd (λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √)"
by(intro JVM_conf_read.lifting_wf_correct_state_d JVM_conf_read_heap_read_typed wf)
from exec ns vs ts_ok have exec': "?mexecd t (x, m) ta (x', m')"
by(auto simp add: split_beta correct_state_def dest: mexecd_non_speculative_typeable)
thus "(λ(xcp, frstls) h. Φ ⊢ t:(xcp, h, frstls) √) x' m'" using ts_ok
by(rule lifting_wf.preserves_red[OF lift])
{
fix t'' x'' m''
assume New: "NewThread t'' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
with exec have "m'' = snd (x', m')" by(rule execd_mthr.new_thread_memory)
thus "(λ(xcp, frstls) h. Φ ⊢ t'':(xcp, h, frstls) √) x'' m''"
using lifting_wf.preserves_NewThread[where ?r="?mexecd", OF lift exec' ts_ok] New
by auto }
{ fix t'' x''
assume "(λ(xcp, frstls) h. Φ ⊢ t'':(xcp, h, frstls) √) x'' m"
with lift exec' ts_ok show "(λ(xcp, frstls) h. Φ ⊢ t'':(xcp, h, frstls) √) x'' m'"
by(rule lifting_wf.preserves_other) }
next
fix t x m ta x' m' vs n
assume exec: "mexecd P t (x, m) ta (x', m')"
and ts_ok: "(λ(xcp, frstls) h. Φ ⊢ t:(xcp, h, frstls) √) x m"
and vs: "vs_conf P m vs"
and ns: "non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
thus "vs_conf P m' (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
by(auto simp add: correct_state_def dest: mexecd_non_speculative_vs_conf)
next
fix t x m ta x' m' ad al v
assume "mexecd P t (x, m) ta (x', m')"
and "(λ(xcp, frstls) h. Φ ⊢ t:(xcp, h, frstls) √) x m"
and "ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙"
thus "∃T. P,m ⊢ ad@al : T"
by(auto simp add: correct_state_def split_beta dest: exec_1_d_read_typeable)
next
fix t x m ta x' m' ad hT
assume "mexecd P t (x, m) ta (x', m')"
and "(λ(xcp, frstls) h. Φ ⊢ t:(xcp, h, frstls) √) x m"
and "NewHeapElem ad hT ∈ set ⦃ta⦄⇘o⇙"
thus "typeof_addr m' ad = ⌊hT⌋"
by(auto dest: exec_1_d_New_typeof_addrD[where x="hT"] simp add: split_beta correct_state_def)
qed
qed
lemma executions_sc:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and wf_start: "wf_start_state P C M vs"
and vs2: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "executions_sc_hb (JVMd_ℰ P C M vs status) P"
(is "executions_sc_hb ?E P")
proof -
from wf_start obtain Ts T meth D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T=⌊meth⌋ in D"
and vs1: "P,start_heap ⊢ vs [:≤] Ts" by cases
interpret known_addrs_typing
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated jvm_known_addrs
JVM_final "mexecd P" "λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √" P
using wf ok by(rule mexecd_known_addrs_typing)
from wf obtain wf_md where wf': "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
hence "wf_syscls P" by(rule wf_prog_wf_syscls)
thus ?thesis
proof(rule executions_sc_hb)
from correct_jvm_state_initial[OF wf wf_start]
show "correct_state_ts Φ (thr (JVM_start_state P C M vs)) start_heap"
by(simp add: correct_jvm_state_def start_state_def split_beta)
next
show "jvm_known_addrs start_tid ((λ(mxs, mxl0, b) vs. (None, [([], Null # vs @ replicate mxl0 undefined_value, fst (method P C M), M, 0)])) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using vs2
by(auto simp add: split_beta start_addrs_allocated jvm_known_addrs_def intro: start_tid_start_addrs[OF ‹wf_syscls P› ok])
qed
qed
end
declare split_paired_Ex [simp del]
declare eq_upto_seq_inconsist_simps [simp]
context JVM_progress begin
abbreviation (input) jvm_non_speculative_read_bound :: nat where
"jvm_non_speculative_read_bound ≡ 2"
lemma exec_instr_non_speculative_read:
assumes hrt: "heap_read_typeable hconf P"
and vs: "vs_conf P (shr s) vs"
and hconf: "hconf (shr s)"
and exec_i: "(ta, xcp', h', frs') ∈ 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 aok: "execd_mthr.mthr.if.actions_ok s t ta"
and i: "I < length ⦃ta⦄⇘o⇙"
and read: "⦃ta⦄⇘o⇙ ! I = ReadMem a'' al'' v"
and v': "v' ∈ w_values P vs (map NormalAction (take I ⦃ta⦄⇘o⇙)) (a'', al'')"
and ns: "non_speculative P vs (llist_of (map NormalAction (take I ⦃ta⦄⇘o⇙)))"
shows "∃ta' xcp'' h'' frs''. (ta', xcp'', h'', frs'') ∈ exec_instr i P t (shr s) stk loc C M pc frs ∧
execd_mthr.mthr.if.actions_ok s t ta' ∧
I < length ⦃ta'⦄⇘o⇙ ∧ take I ⦃ta'⦄⇘o⇙ = take I ⦃ta⦄⇘o⇙ ∧
⦃ta'⦄⇘o⇙ ! I = ReadMem a'' al'' v' ∧
length ⦃ta'⦄⇘o⇙ ≤ max jvm_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
using exec_i i read
proof(cases i)
case [simp]: ALoad
let ?a = "the_Addr (hd (tl stk))"
let ?i = "the_Intg (hd stk)"
from exec_i i read have Null: "hd (tl stk) ≠ Null"
and bounds: "0 <=s ?i" "sint ?i < int (alen_of_htype (the (typeof_addr (shr s) ?a)))"
and [simp]: "I = 0" "a'' = ?a" "al'' = ACell (nat (sint ?i))"
by(auto split: if_split_asm)
from Null check obtain a T n
where a: "length stk > 1" "hd (tl stk) = Addr a"
and type: "typeof_addr (shr s) ?a = ⌊Array_type T n⌋" by(fastforce simp add: is_Ref_def)
from bounds type have "nat (sint ?i) < n"
by (simp add: word_sle_eq nat_less_iff)
with type have adal: "P,shr s ⊢ ?a@ACell (nat (sint ?i)) : T"
by(rule addr_loc_type.intros)
from v' vs adal have "P,shr s ⊢ v' :≤ T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
with hrt adal have "heap_read (shr s) ?a (ACell (nat (sint ?i))) v'" using hconf by(rule heap_read_typeableD)
with type Null aok exec_i show ?thesis apply auto using bounds by fastforce+
next
case [simp]: (Getfield F D)
let ?a = "the_Addr (hd stk)"
from exec_i i read have Null: "hd stk ≠ Null"
and [simp]: "I = 0" "a'' = ?a" "al'' = CField D F"
by(auto split: if_split_asm)
with check obtain U T fm C' a
where sees: "P ⊢ D sees F:T (fm) in D"
and type: "typeof_addr (shr s) ?a = ⌊U⌋"
and sub: "P ⊢ class_type_of U ≼⇧* D"
and a: "hd stk = Addr a" "length stk > 0" by(auto simp add: is_Ref_def)
from has_visible_field[OF sees] sub
have "P ⊢ class_type_of U has F:T (fm) in D" by(rule has_field_mono)
with type have adal: "P,shr s ⊢ ?a@CField D F : T"
by(rule addr_loc_type.intros)
from v' vs adal have "P,shr s ⊢ v' :≤ T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
with hrt adal have "heap_read (shr s) ?a (CField D F) v'" using hconf by(rule heap_read_typeableD)
with type Null aok exec_i show ?thesis by(fastforce)
next
case [simp]: (CAS F D)
let ?a = "the_Addr (hd (tl (tl stk)))"
from exec_i i read have Null: "hd (tl (tl stk)) ≠ Null"
and [simp]: "I = 0" "a'' = ?a" "al'' = CField D F"
by(auto split: if_split_asm simp add: nth_Cons')
with check obtain U T fm C' a
where sees: "P ⊢ D sees F:T (fm) in D"
and type: "typeof_addr (shr s) ?a = ⌊U⌋"
and sub: "P ⊢ class_type_of U ≼⇧* D"
and a: "hd (tl (tl stk)) = Addr a" "length stk > 2"
and v: "P,shr s ⊢ hd stk :≤ T"
by(auto simp add: is_Ref_def)
from has_visible_field[OF sees] sub
have "P ⊢ class_type_of U has F:T (fm) in D" by(rule has_field_mono)
with type have adal: "P,shr s ⊢ ?a@CField D F : T"
by(rule addr_loc_type.intros)
from v' vs adal have "P,shr s ⊢ v' :≤ T" by(auto dest!: vs_confD dest: addr_loc_type_fun)
with hrt adal have read: "heap_read (shr s) ?a (CField D F) v'" using hconf by(rule heap_read_typeableD)
show ?thesis
proof(cases "v' = hd (tl stk)")
case True
from heap_write_total[OF hconf adal v] a obtain h'
where "heap_write (shr s) a (CField D F) (hd stk) h'" by auto
then show ?thesis using read a True aok exec_i by fastforce
next
case False
then show ?thesis using read a aok exec_i
by(fastforce intro!: disjI2)
qed
next
case [simp]: (Invoke M n)
let ?a = "the_Addr (stk ! n)"
let ?vs = "rev (take n stk)"
from exec_i i read have Null: "stk ! n ≠ Null"
and iec: "snd (snd (snd (method P (class_type_of (the (typeof_addr (shr s) ?a))) M))) = Native"
by(auto split: if_split_asm)
with check obtain a T Ts Tr D
where a: "stk ! n = Addr a" "n < length stk"
and type: "typeof_addr (shr s) ?a = ⌊T⌋"
and extwt: "P ⊢ class_type_of T sees M:Ts→Tr = Native in D" "D∙M(Ts) :: Tr"
by(auto simp add: is_Ref_def has_method_def)
from extwt have native: "is_native P T M" by(auto simp add: is_native.simps)
from Null iec type exec_i obtain ta' va
where red: "(ta', va, h') ∈ red_external_aggr P t ?a M ?vs (shr s)"
and ta: "ta = extTA2JVM P ta'" by(fastforce)
from aok ta have aok': "execd_mthr.mthr.if.actions_ok s t ta'" by simp
from red_external_aggr_non_speculative_read[OF hrt vs red[unfolded a the_Addr.simps] _ aok' hconf, of I a'' al'' v v']
native type i read v' ns a ta
obtain ta'' va'' h''
where "(ta'', va'', h'') ∈ red_external_aggr P t a M (rev (take n stk)) (shr s)"
and "execd_mthr.mthr.if.actions_ok s t ta''"
and "I < length ⦃ta''⦄⇘o⇙" "take I ⦃ta''⦄⇘o⇙ = take I ⦃ta'⦄⇘o⇙"
and "⦃ta''⦄⇘o⇙ ! I = ReadMem a'' al'' v'" "length ⦃ta''⦄⇘o⇙ ≤ length ⦃ta'⦄⇘o⇙" by auto
thus ?thesis using Null iec ta extwt a type
by(cases va'') force+
qed(auto simp add: split_beta split: if_split_asm)
lemma exec_1_d_non_speculative_read:
assumes hrt: "heap_read_typeable hconf P"
and vs: "vs_conf P (shr s) vs"
and exec: "P,t ⊢ Normal (xcp, shr s, frs) -ta-jvmd→ Normal (xcp', h', frs')"
and aok: "execd_mthr.mthr.if.actions_ok s t ta"
and hconf: "hconf (shr s)"
and i: "I < length ⦃ta⦄⇘o⇙"
and read: "⦃ta⦄⇘o⇙ ! I = ReadMem a'' al'' v"
and v': "v' ∈ w_values P vs (map NormalAction (take I ⦃ta⦄⇘o⇙)) (a'', al'')"
and ns: "non_speculative P vs (llist_of (map NormalAction (take I ⦃ta⦄⇘o⇙)))"
shows "∃ta' xcp'' h'' frs''. P,t ⊢ Normal (xcp, shr s, frs) -ta'-jvmd→ Normal (xcp'', h'', frs'') ∧
execd_mthr.mthr.if.actions_ok s t ta' ∧
I < length ⦃ta'⦄⇘o⇙ ∧ take I ⦃ta'⦄⇘o⇙ = take I ⦃ta⦄⇘o⇙ ∧
⦃ta'⦄⇘o⇙ ! I = ReadMem a'' al'' v' ∧
length ⦃ta'⦄⇘o⇙ ≤ max jvm_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
using assms
apply -
apply(erule jvmd_NormalE)
apply(cases "(P, t, xcp, shr s, frs)" rule: exec.cases)
apply simp
defer
apply simp
apply clarsimp
apply(drule (3) exec_instr_non_speculative_read)
apply(clarsimp simp add: check_def has_method_def)
apply simp
apply(rule i)
apply(rule read)
apply(rule v')
apply(rule ns)
apply(clarsimp simp add: exec_1_d.simps exec_d_def)
done
end
declare split_paired_Ex [simp]
declare eq_upto_seq_inconsist_simps [simp del]
locale JVM_allocated_progress =
JVM_progress
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write hconf
P
+
JVM_allocated_heap_conf
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write hconf
allocated
P
for addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
and thread_id2addr :: "'thread_id ⇒ 'addr"
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and hconf :: "'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
and P :: "'addr jvm_prog"
begin
lemma non_speculative_read:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "execd_mthr.if.non_speculative_read jvm_non_speculative_read_bound
(init_fin_lift_state status (JVM_start_state P C M vs))
(w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs)))"
(is "execd_mthr.if.non_speculative_read _ ?start_state ?start_vs")
proof(rule execd_mthr.if.non_speculative_readI)
fix ttas s' t x ta x' m' i ad al v v'
assume τRed: "execd_mthr.mthr.if.RedT P ?start_state ttas s'"
and sc: "non_speculative P ?start_vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
and ts't: "thr s' t = ⌊(x, no_wait_locks)⌋"
and red: "execd_mthr.init_fin P t (x, shr s') ta (x', m')"
and aok: "execd_mthr.mthr.if.actions_ok s' t ta"
and i: "i < length ⦃ta⦄⇘o⇙"
and ns': "non_speculative P (w_values P ?start_vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙))"
and read: "⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v)"
and v': "v' ∈ w_values P ?start_vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al)"
from wf_start obtain Ts T meth D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T = ⌊meth⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases
let ?conv = "λttas. concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)"
let ?vs' = "w_values P ?start_vs (?conv ttas)"
let ?wt_ok = "init_fin_lift (λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √)"
let ?start_obs = "map snd (lift_start_obs start_tid start_heap_obs)"
from wf obtain wf_md where wf': "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
interpret known_addrs_typing
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated jvm_known_addrs
JVM_final "mexecd P" "λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √"
using wf ok by(rule mexecd_known_addrs_typing)
from conf have len2: "length vs = length Ts" by(rule list_all2_lengthD)
from correct_jvm_state_initial[OF wf wf_start]
have "correct_state_ts Φ (thr (JVM_start_state P C M vs)) start_heap"
by(simp add: correct_jvm_state_def start_state_def split_beta)
hence ts_ok_start: "ts_ok ?wt_ok (thr ?start_state) (shr ?start_state)"
unfolding ts_ok_init_fin_lift_init_fin_lift_state by(simp add: start_state_def split_beta)
have sc': "non_speculative P ?start_vs (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of ttas))))"
using sc by(simp add: lmap_lconcat llist.map_comp o_def split_def lconcat_llist_of[symmetric])
from start_state_vs_conf[OF wf_prog_wf_syscls[OF wf']]
have vs_conf_start: "vs_conf P (shr ?start_state) ?start_vs"
by(simp add:init_fin_lift_state_conv_simps start_state_def split_beta)
with τRed ts_ok_start sc
have wt': "ts_ok ?wt_ok (thr s') (shr s')"
and vs': "vs_conf P (shr s') ?vs'" by(rule if_RedT_non_speculative_invar)+
from red i read obtain xcp frs xcp' frs' ta'
where x: "x = (Running, xcp, frs)" and x': "x' = (Running, xcp', frs')"
and ta: "ta = convert_TA_initial (convert_obs_initial ta')"
and red': "P,t ⊢ Normal (xcp, shr s', frs) -ta'-jvmd→ Normal (xcp', m', frs')"
by cases fastforce+
from ts't wt' x have hconf: "hconf (shr s')" by(auto dest!: ts_okD simp add: correct_state_def)
have aok': "execd_mthr.mthr.if.actions_ok s' t ta'" using aok unfolding ta by simp
from i read v' ns' ta have "i < length ⦃ta'⦄⇘o⇙"
and "⦃ta'⦄⇘o⇙ ! i = ReadMem ad al v"
and "v' ∈ w_values P ?vs' (map NormalAction (take i ⦃ta'⦄⇘o⇙)) (ad, al)"
and "non_speculative P ?vs' (llist_of (map NormalAction (take i ⦃ta'⦄⇘o⇙)))"
by(simp_all add: take_map)
from exec_1_d_non_speculative_read[OF hrt vs' red' aok' hconf this]
obtain ta'' xcp'' frs'' h''
where red'': "P,t ⊢ Normal (xcp, shr s', frs) -ta''-jvmd→ Normal (xcp'', h'', frs'')"
and aok'': "execd_mthr.mthr.if.actions_ok s' t ta''"
and i'': " i < length ⦃ta''⦄⇘o⇙"
and eq'': "take i ⦃ta''⦄⇘o⇙ = take i ⦃ta'⦄⇘o⇙"
and read'': "⦃ta''⦄⇘o⇙ ! i = ReadMem ad al v'"
and len'': "length ⦃ta''⦄⇘o⇙ ≤ max jvm_non_speculative_read_bound (length ⦃ta'⦄⇘o⇙)" by blast
let ?x' = "(Running, xcp'', frs'')"
let ?ta' = "convert_TA_initial (convert_obs_initial ta'')"
from red'' have "execd_mthr.init_fin P t (x, shr s') ?ta' (?x', h'')"
unfolding x by -(rule execd_mthr.init_fin.NormalAction, simp)
moreover from aok'' have "execd_mthr.mthr.if.actions_ok s' t ?ta'" by simp
moreover from i'' have "i < length ⦃?ta'⦄⇘o⇙" by simp
moreover from eq'' have "take i ⦃?ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙" unfolding ta by(simp add: take_map)
moreover from read'' i'' have "⦃?ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v')" by(simp add: nth_map)
moreover from len'' have "length ⦃?ta'⦄⇘o⇙ ≤ max jvm_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
unfolding ta by simp
ultimately
show "∃ta' x'' m''. execd_mthr.init_fin P t (x, shr s') ta' (x'', m'') ∧
execd_mthr.mthr.if.actions_ok s' t ta' ∧
i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧
⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
length ⦃ta'⦄⇘o⇙ ≤ max jvm_non_speculative_read_bound (length ⦃ta⦄⇘o⇙)"
by blast
qed
lemma JVM_cut_and_update:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "execd_mthr.if.cut_and_update (init_fin_lift_state status (JVM_start_state P C M vs))
(mrw_values P Map.empty (map snd (lift_start_obs start_tid start_heap_obs)))"
proof -
from wf_start obtain Ts T meth D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T = ⌊meth⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases
interpret known_addrs_typing
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated jvm_known_addrs
JVM_final "mexecd P" "λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √"
using wf ok by(rule mexecd_known_addrs_typing)
let ?start_vs = "w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs))"
let ?wt_ok = "init_fin_lift (λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √)"
let ?start_obs = "map snd (lift_start_obs start_tid start_heap_obs)"
let ?start_state = "init_fin_lift_state status (JVM_start_state P C M vs)"
from wf obtain wf_md where wf': "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
hence "wf_syscls P" by(rule wf_prog_wf_syscls)
moreover
note non_speculative_read[OF wf hrt wf_start ka]
moreover have "ts_ok ?wt_ok (thr ?start_state) (shr ?start_state)"
using correct_jvm_state_initial[OF wf wf_start]
by(simp add: correct_jvm_state_def start_state_def split_beta)
moreover have ka: "jvm_known_addrs start_tid ((λ(mxs, mxl0, b) vs. (None, [([], Null # vs @ replicate mxl0 undefined_value, fst (method P C M), M, 0)])) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using ka by(auto simp add: split_beta start_addrs_allocated jvm_known_addrs_def intro: start_tid_start_addrs[OF ‹wf_syscls P› ok])
ultimately show ?thesis by(rule non_speculative_read_into_cut_and_update)
qed
lemma JVM_drf:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "drf (JVMd_ℰ P C M vs status) P"
proof -
from wf_start obtain Ts T meth D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T = ⌊meth⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases
from wf obtain wf_md where wf': "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
hence "wf_syscls P" by(rule wf_prog_wf_syscls)
with JVM_cut_and_update[OF assms]
show ?thesis
proof(rule known_addrs_typing.drf[OF mexecd_known_addrs_typing[OF wf ok]])
from correct_jvm_state_initial[OF wf wf_start]
show "correct_state_ts Φ (thr (JVM_start_state P C M vs)) start_heap"
by(simp add: correct_jvm_state_def start_state_def split_beta)
next
show "jvm_known_addrs start_tid ((λ(mxs, mxl0, b) vs. (None, [([], Null # vs @ replicate mxl0 undefined_value, fst (method P C M), M, 0)])) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using ka by(auto simp add: split_beta start_addrs_allocated jvm_known_addrs_def intro: start_tid_start_addrs[OF ‹wf_syscls P› ok])
qed
qed
lemma JVM_sc_legal:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "sc_legal (JVMd_ℰ P C M vs status) P"
proof -
from wf_start obtain Ts T meth D where ok: "start_heap_ok"
and sees: "P ⊢ C sees M:Ts→T = ⌊meth⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts" by cases
interpret known_addrs_typing
addr2thread_id thread_id2addr
spurious_wakeups
empty_heap allocate typeof_addr heap_read heap_write
allocated jvm_known_addrs
JVM_final "mexecd P" "λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √"
using wf ok by(rule mexecd_known_addrs_typing)
from wf obtain wf_md where wf': "wf_prog wf_md P" by(blast dest: wt_jvm_progD)
hence "wf_syscls P" by(rule wf_prog_wf_syscls)
let ?start_vs = "w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs))"
let ?wt_ok = "init_fin_lift (λt (xcp, frstls) h. Φ ⊢ t: (xcp, h, frstls) √)"
let ?start_obs = "map snd (lift_start_obs start_tid start_heap_obs)"
let ?start_state = "init_fin_lift_state status (JVM_start_state P C M vs)"
note ‹wf_syscls P› non_speculative_read[OF wf hrt wf_start ka]
moreover have "ts_ok ?wt_ok (thr ?start_state) (shr ?start_state)"
using correct_jvm_state_initial[OF wf wf_start]
by(simp add: correct_jvm_state_def start_state_def split_beta)
moreover
have ka_allocated: "jvm_known_addrs start_tid ((λ(mxs, mxl0, b) vs. (None, [([], Null # vs @ replicate mxl0 undefined_value, fst (method P C M), M, 0)])) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
using ka by(auto simp add: split_beta start_addrs_allocated jvm_known_addrs_def intro: start_tid_start_addrs[OF ‹wf_syscls P› ok])
ultimately have "execd_mthr.if.hb_completion ?start_state (lift_start_obs start_tid start_heap_obs)"
by(rule non_speculative_read_into_hb_completion)
thus ?thesis using ‹wf_syscls P›
proof(rule sc_legal)
from correct_jvm_state_initial[OF wf wf_start]
show "correct_state_ts Φ (thr (JVM_start_state P C M vs)) start_heap"
by(simp add: correct_jvm_state_def start_state_def split_beta)
qed(rule ka_allocated)
qed
lemma JVM_jmm_consistent:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "jmm_consistent (JVMd_ℰ P C M vs status) P"
(is "jmm_consistent ?ℰ P")
proof -
interpret drf "?ℰ" P using assms by(rule JVM_drf)
interpret sc_legal "?ℰ" P using assms by(rule JVM_sc_legal)
show ?thesis by unfold_locales
qed
lemma JVM_ex_sc_exec:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "∃E ws. E ∈ JVMd_ℰ P C M vs status ∧ P ⊢ (E, ws) √ ∧ sequentially_consistent P (E, ws)"
(is "∃E ws. _ ∈ ?ℰ ∧ _")
proof -
interpret jmm: executions_sc_hb ?ℰ P using assms by -(rule executions_sc)
let ?start_state = "init_fin_lift_state status (JVM_start_state P C M vs)"
let ?start_mrw = "mrw_values P Map.empty (map snd (lift_start_obs start_tid start_heap_obs))"
from execd_mthr.if.sequential_completion_Runs[OF execd_mthr.if.cut_and_update_imp_sc_completion[OF JVM_cut_and_update[OF assms]] ta_seq_consist_convert_RA]
obtain ttas where Red: "execd_mthr.mthr.if.mthr.Runs P ?start_state ttas"
and sc: "ta_seq_consist P ?start_mrw (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) ttas))" by blast
let ?E = "lappend (llist_of (lift_start_obs start_tid start_heap_obs)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
from Red have "?E ∈ ?ℰ" by(blast intro: execd_mthr.mthr.if.ℰ.intros)
moreover from Red have tsa: "thread_start_actions_ok ?E"
by(blast intro: execd_mthr.thread_start_actions_ok_init_fin execd_mthr.mthr.if.ℰ.intros)
from sc have "ta_seq_consist P Map.empty (lmap snd ?E)"
unfolding lmap_lappend_distrib lmap_lconcat llist.map_comp split_def o_def lmap_llist_of map_map snd_conv
by(simp add: ta_seq_consist_lappend ta_seq_consist_start_heap_obs)
from ta_seq_consist_imp_sequentially_consistent[OF tsa jmm.ℰ_new_actions_for_fun[OF ‹?E ∈ ?ℰ›] this]
obtain ws where "sequentially_consistent P (?E, ws)" "P ⊢ (?E, ws) √" by iprover
ultimately show ?thesis by blast
qed
theorem JVM_consistent:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and hrt: "heap_read_typeable hconf P"
and wf_start: "wf_start_state P C M vs"
and ka: "⋃(ka_Val ` set vs) ⊆ set start_addrs"
shows "∃E ws. legal_execution P (JVMd_ℰ P C M vs status) (E, ws)"
proof -
let ?ℰ = "JVMd_ℰ P C M vs status"
interpret sc_legal "?ℰ" P using assms by(rule JVM_sc_legal)
from JVM_ex_sc_exec[OF assms]
obtain E ws where "E ∈ ?ℰ" "P ⊢ (E, ws) √" "sequentially_consistent P (E, ws)" by blast
hence "legal_execution P ?ℰ (E, ws)" by(rule SC_is_legal)
thus ?thesis by blast
qed
end
text ‹
One could now also prove that the aggressive JVM satisfies @{term drf}.
The key would be that ‹welltyped_commute› also holds for @{term "non_speculative"} prefixes from start.
›
end