# Theory JMM_Heap

```(*  Title:      JinjaThreads/MM/JMM_Heap.thy
Author:     Andreas Lochbihler
*)

section ‹Locales for heap operations with set of allocated addresses›

theory JMM_Heap
imports
"../Common/WellForm"
SC_Completion
HB_Completion
begin

lemma w_addrs_empty [simp]: "w_addrs (λ_. {}) = {}"

locale allocated_heap_base = heap_base +
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
fixes allocated :: "'heap ⇒ 'addr set"

locale allocated_heap =
allocated_heap_base +
heap +
and spurious_wakeups :: bool
and empty_heap :: "'heap"
and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
and allocated :: "'heap ⇒ 'addr set"
and P :: "'m prog"

assumes allocated_empty: "allocated empty_heap = {}"
and allocate_allocatedD:
"(h', a) ∈ allocate h hT ⟹ allocated h' = insert a (allocated h) ∧ a ∉ allocated h"
and heap_write_allocated_same:
"heap_write h a al v h' ⟹ allocated h' = allocated h"
begin

lemma allocate_allocated_mono: "(h', a) ∈ allocate h C ⟹ allocated h ⊆ allocated h'"

lemma
shows start_addrs_allocated: "allocated start_heap = set start_addrs"
proof -
{ fix h ads b and xs :: "cname list"
let "?start_addrs h ads b xs" = "fst (snd (foldl create_initial_object (h, ads, b) xs))"
let "?start_heap h ads b xs" = "fst (foldl create_initial_object (h, ads, b) xs)"
assume "allocated h = set ads"
hence "allocated (?start_heap h ads b xs) = set (?start_addrs h ads b xs) ∧
(is "?concl xs h ads b")
proof(induct xs arbitrary: h ads b)
case Nil thus ?case by auto
next
case (Cons x xs)
note ads = ‹allocated h = set ads›
show ?case
proof(cases "b ∧ allocate h (Class_type x) ≠ {}")
case False thus ?thesis using ads
by(simp add: create_initial_object_simps zip_append1)
next
case [simp]: True
then obtain h' a'
where h'a': "(SOME ha. ha ∈ allocate h (Class_type x)) = (h', a')"
and new_obj: "(h', a') ∈ allocate h (Class_type x)"
by(cases "(SOME ha. ha ∈ allocate h (Class_type x))")(auto simp del: True dest: allocate_Eps)

from new_obj have "allocated h' = insert a' (allocated h)" "a' ∉ allocated h"
by(auto dest: allocate_allocatedD)
with ads have "allocated h' = set (ads @ [a'])" by auto
hence "?concl xs h' (ads @ [a']) True" by(rule Cons)
moreover have "a' ∉ set ads" using ‹a' ∉ allocated h› ads by blast
ultimately show ?thesis by(simp add: create_initial_object_simps new_obj h'a')
qed
qed }
from this[of empty_heap "[]" True initialization_list]
show "allocated start_heap = set start_addrs"
unfolding start_heap_def start_addrs_def start_heap_data_def
by(auto simp add: allocated_empty)
qed

lemma w_addrs_start_heap_obs: "w_addrs (w_values P vs (map NormalAction start_heap_obs)) ⊆ w_addrs vs"
proof -
{ fix xs
let ?NewObj = "λa C. NewHeapElem a (Class_type C) :: ('addr, 'thread_id) obs_event"
let "?start_heap_obs xs" = "map (λ(C, a). ?NewObj a C) xs"
have "w_addrs (w_values P vs (map NormalAction (?start_heap_obs xs))) ⊆ w_addrs vs"
(is "?concl xs")
proof(induct xs arbitrary: vs)
case Nil thus ?case by simp
next
case (Cons x xs)
have "w_addrs (w_values P vs (map NormalAction (map (λ(C, a). ?NewObj a C) (x # xs))))
= w_addrs (w_values P (w_value P vs (NormalAction (?NewObj (snd x) (fst x)))) (map NormalAction (map (λ(C, a). ?NewObj a C) xs)))"
also have "… ⊆ w_addrs (w_value P vs (NormalAction (?NewObj (snd x) (fst x))))" by(rule Cons)
also have "… ⊆ w_addrs vs"
finally show ?case .
qed }
thus ?thesis by(simp add: start_heap_obs_def)
qed

end

context heap_base begin

"P ⊢ class_type_of CTn has F:T (fm) in C
⟹ P,h ⊢ addr_loc_default P CTn (CField C F) :≤ T"
apply(cases CTn)
apply simp
apply(frule has_field_decl_above)
apply simp
done

definition vs_conf :: "'m prog ⇒ 'heap ⇒ ('addr × addr_loc ⇒ 'addr val set) ⇒ bool"
where "vs_conf P h vs ⟷ (∀ad al v. v ∈ vs (ad, al) ⟶ (∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T))"

lemma vs_confI:
"(⋀ad al v. v ∈ vs (ad, al) ⟹ ∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T) ⟹ vs_conf P h vs"
unfolding vs_conf_def by blast

lemma vs_confD:
"⟦ vs_conf P h vs; v ∈ vs (ad, al) ⟧ ⟹ ∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T"
unfolding vs_conf_def by blast

lemma vs_conf_insert_iff:
"vs_conf P h (vs((ad, al) := insert v (vs (ad, al))))
⟷ vs_conf P h vs ∧ (∃T. P,h ⊢ ad@al : T ∧ P,h ⊢ v :≤ T)"
by(auto 4 3 elim: vs_confD intro: vs_confI split: if_split_asm)

end

context heap begin

lemma vs_conf_hext: "⟦ vs_conf P h vs; h ⊴ h' ⟧ ⟹ vs_conf P h' vs"
by(blast intro!: vs_confI intro: conf_hext addr_loc_type_hext_mono dest: vs_confD)

lemma vs_conf_allocate:
"⟦ vs_conf P h vs; (h', a) ∈ allocate h hT; is_htype P hT ⟧
⟹ vs_conf P h' (w_value P vs (NormalAction (NewHeapElem a hT)))"
apply(drule vs_conf_hext)
apply(erule hext_allocate)
apply(auto intro!: vs_confI simp add: addr_locs_def split: if_split_asm htype.split_asm)
apply(auto 3 3 intro: addr_loc_type.intros defval_conf dest: allocate_SomeD elim: has_field_is_class vs_confD)
apply(rule exI conjI addr_loc_type.intros|drule allocate_SomeD|erule has_field_is_class|simp)+
done

end

text ‹
‹heap_read_typeable› must not be defined in @{term heap_conf_base} (where it should be) because
this would lead to duplicate definitions of ‹heap_read_typeable› in contexts where @{term heap_conf_base}
is imported twice with different parameters, e.g., @{term P} and @{term "J2JVM P"} in @{term "J_JVM_heap_conf_read"}.
›

context heap_base begin

definition heap_read_typeable :: "('heap ⇒ bool) ⇒ 'm prog ⇒ bool"
where "heap_read_typeable hconf P ⟷ (∀h ad al v T. hconf h ⟶ P,h ⊢ ad@al : T ⟶ P,h ⊢ v :≤ T ⟶ heap_read h ad al v)"

"(⋀h ad al v T. ⟦ P,h ⊢ ad@al : T; P,h ⊢ v :≤ T; hconf h ⟧ ⟹ heap_read h ad al v) ⟹ heap_read_typeable hconf P"
unfolding heap_read_typeable_def by blast

"⟦ heap_read_typeable hconf P; P,h ⊢ ad@al : T; P,h ⊢ v :≤ T; hconf h ⟧ ⟹ heap_read h ad al v"
unfolding heap_read_typeable_def by blast

end

context heap_base begin

definition heap_read_typed :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
where "heap_read_typed P h ad al v ⟷ heap_read h ad al v ∧ (∀T. P,h ⊢ ad@al : T ⟶ P,h ⊢ v :≤ T)"

"⟦ heap_read h ad al v; ⋀T. P,h ⊢ ad@al : T ⟹ P,h ⊢ v :≤ T ⟧ ⟹ heap_read_typed P h ad al v"
unfolding heap_read_typed_def by blast

unfolding heap_read_typed_def by blast

"⟦ heap_read_typed P h ad al v; P,h ⊢ ad@al : T ⟧ ⟹ P,h ⊢ v :≤ T"
unfolding heap_read_typed_def by blast

end

context heap_conf begin

proof
fix h a al v T
assume "heap_read_typed P h a al v" "P,h ⊢ a@al : T"
thus "P,h ⊢ v :≤ T" by(rule heap_read_typed_typed)
qed

end

context heap begin

assumes wf: "wf_syscls P"
and a: "a ∈ set start_addrs"
and adal: "P,start_heap ⊢ a@al : T"
shows "w_values P (λ_. {}) (map NormalAction start_heap_obs) (a, al) ≠ {}"
proof -
from a obtain CTn where CTn: "NewHeapElem a CTn ∈ set start_heap_obs"
then obtain obs obs' where obs: "start_heap_obs = obs @ NewHeapElem a CTn # obs'" by(auto dest: split_list)
have "w_value P (w_values P (λ_. {}) (map NormalAction obs)) (NormalAction (NewHeapElem a CTn)) (a, al) ≠ {}"
proof(cases CTn)
case [simp]: (Class_type C)
with wf CTn have "typeof_addr start_heap a = ⌊Class_type C⌋"
by(auto intro: NewHeapElem_start_heap_obsD)
with adal show ?thesis by cases auto
next
case [simp]: (Array_type T n)
with wf CTn have "typeof_addr start_heap a = ⌊Array_type T n⌋"
by(auto dest: NewHeapElem_start_heap_obsD)
with adal show ?thesis by cases(auto dest: has_field_decl_above)
qed
moreover have "w_value P (w_values P (λ_. {}) (map NormalAction obs)) (NormalAction (NewHeapElem a CTn :: ('addr, 'thread_id) obs_event))
(a, al) ⊆ w_values P (λ_. {}) (map NormalAction start_heap_obs) (a, al)"
by(simp add: obs del: w_value.simps)(rule w_values_mono)
ultimately show ?thesis by blast
qed

end

end
```