# Theory JMM_Type2

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

section ‹JMM heap implementation 2›

theory JMM_Type2
imports
"../Common/ExternalCallWF"
JMM_Heap
begin

subsection ‹Definitions›

datatype addr = Address htype nat   ― ‹heap type and sequence number›

definition "monitor_finfun_to_list (ls :: addr ⇒f nat) = (SOME xs. set xs = {x. finfun_dom ls \$ x })"
instance
proof
fix ls :: "addr ⇒f nat"
show "set (monitor_finfun_to_list ls) = Collect ((\$) (finfun_dom ls))"
using finite_list[OF finite_finfun_dom, where ?f.1 = "ls"]
by(rule someI_ex)
qed
end

text ‹
The JMM heap only stores which sequence numbers of a given @{typ "htype"} have already been allocated.
›

type_synonym JMM_heap = "htype ⇒ nat set"

translations (type) "JMM_heap" <= (type) "htype ⇒ nat set"

definition jmm_allocate :: "JMM_heap ⇒ htype ⇒ (JMM_heap × addr) set"
where "jmm_allocate h hT = (let hhT = h hT in (λn. (h(hT := insert n hhT), Address hT n)) ` (- hhT))"

abbreviation jmm_empty :: "JMM_heap" where "jmm_empty == (λ_. {})"

where "jmm_typeof_addr P h = (λhT. if is_htype P hT then Some hT else None) ∘ fst ∘ the_Address"

where "jmm_typeof_addr' P = (λhT. if is_htype P hT then Some hT else None) ∘ fst ∘ the_Address"

context
notes [[inductive_internals]]
begin

where "jmm_heap_write h a ad v h"

end

definition jmm_hconf :: "JMM_heap ⇒ bool"
where "jmm_hconf h ⟷ True"

definition jmm_allocated :: "JMM_heap ⇒ addr set"
where "jmm_allocated h = {Address CTn n|CTn n. n ∈ h CTn}"

definition jmm_spurious_wakeups :: "bool"
where "jmm_spurious_wakeups = True"

lemmas jmm_heap_ops_defs =
jmm_allocated_def jmm_spurious_wakeups_def

interpretation jmm: heap_base
jmm_spurious_wakeups
for P
.

abbreviation jmm_hext :: "'m prog ⇒ JMM_heap ⇒ JMM_heap ⇒ bool" ("_ ⊢ _ ⊴jmm _" [51,51,51] 50)
where "jmm_hext ≡ jmm.hext TYPE('m)"

abbreviation jmm_conf :: "'m prog ⇒ JMM_heap ⇒ addr val ⇒ ty ⇒ bool"
("_,_ ⊢jmm _ :≤ _"  [51,51,51,51] 50)
where "jmm_conf P ≡ jmm.conf TYPE('m) P P"

("_,_ ⊢jmm _@_ : _" [50, 50, 50, 50, 50] 51)

abbreviation jmm_confs :: "'m prog ⇒ JMM_heap ⇒ addr val list ⇒ ty list ⇒ bool"
("_,_ ⊢jmm _ [:≤] _"  [51,51,51,51] 50)
where "jmm_confs P ≡ jmm.confs TYPE('m) P P"

abbreviation jmm_tconf :: "'m prog ⇒ JMM_heap ⇒ addr ⇒ bool" ("_,_ ⊢jmm _ √t" [51,51,51] 50)
where "jmm_tconf P ≡ jmm.tconf TYPE('m) P P"

interpretation jmm: allocated_heap_base
jmm_spurious_wakeups
jmm_allocated
for P
.

text ‹Now a variation of the JMM with a different read operation that permits to read only type-conformant values›

interpretation jmm': heap_base
jmm_spurious_wakeups
for P .

abbreviation jmm'_hext :: "'m prog ⇒ JMM_heap ⇒ JMM_heap ⇒ bool" ("_ ⊢ _ ⊴jmm'' _" [51,51,51] 50)
where "jmm'_hext ≡ jmm'.hext TYPE('m)"

abbreviation jmm'_conf :: "'m prog ⇒ JMM_heap ⇒ addr val ⇒ ty ⇒ bool"
("_,_ ⊢jmm'' _ :≤ _"  [51,51,51,51] 50)
where "jmm'_conf P ≡ jmm'.conf TYPE('m) P P"

("_,_ ⊢jmm'' _@_ : _" [50, 50, 50, 50, 50] 51)

abbreviation jmm'_confs :: "'m prog ⇒ JMM_heap ⇒ addr val list ⇒ ty list ⇒ bool"
("_,_ ⊢jmm'' _ [:≤] _"  [51,51,51,51] 50)
where "jmm'_confs P ≡ jmm'.confs TYPE('m) P P"

abbreviation jmm'_tconf :: "'m prog ⇒ JMM_heap ⇒ addr ⇒ bool" ("_,_ ⊢jmm'' _ √t" [51,51,51] 50)
where "jmm'_tconf P ≡ jmm'.tconf TYPE('m) P P"

subsection ‹Heap locale interpretations›

subsection ‹Locale ‹heap››

proof
fix h' a h hT
assume "(h', a) ∈ jmm_allocate h hT" "is_htype P hT"
thus "jmm_typeof_addr P h' a = ⌊hT⌋"
next
fix h hT h' a
assume "(h', a) ∈ jmm_allocate h hT"
thus "P ⊢ h ⊴jmm h'" by(auto simp add: jmm_heap_ops_defs intro: jmm.hextI)
next
fix h a al v h'
assume "jmm_heap_write h a al v h'"
thus "P ⊢ h ⊴jmm h'" by cases auto
qed simp

interpretation jmm: heap
jmm_spurious_wakeups
P
for P
by(rule jmm_heap)

lemmas jmm'_heap = jmm_heap

interpretation jmm': heap
jmm_spurious_wakeups
P
for P
by(rule jmm'_heap)

lemma jmm_allocate_Eps:
"(SOME ha. ha ∈ jmm_allocate h hT) = (h', a')
⟹ jmm_allocate h hT ≠ {} ⟶ (h', a') ∈ jmm_allocate h hT"
by(auto dest: jmm.allocate_Eps)

lemma jmm_allocate_eq_empty: "jmm_allocate h hT = {} ⟷ h hT = UNIV"

lemma jmm_allocate_otherD:
"(h', a) ∈ jmm_allocate h hT ⟹ ∀hT'. hT' ≠ hT ⟶ h' hT' = h hT'"

lemma jmm_start_heap_ok: "jmm.start_heap_ok"
apply(simp add: jmm.start_heap_ok_def jmm.start_heap_data_def initialization_list_def sys_xcpts_list_def jmm.create_initial_object_simps)
apply(split prod.split, clarify, clarsimp simp add: jmm.create_initial_object_simps jmm_allocate_eq_empty Thread_neq_sys_xcpts sys_xcpts_neqs dest!: jmm_allocate_Eps jmm_allocate_otherD)+
done

subsection ‹Locale ‹heap_conf››

interpretation jmm: heap_conf_base
jmm_spurious_wakeups
P
for P .

abbreviation (input) jmm'_hconf :: "JMM_heap ⇒ bool"
where "jmm'_hconf == jmm_hconf"

interpretation jmm': heap_conf_base
jmm_spurious_wakeups
P
for P .

abbreviation jmm_heap_read_typeable :: "'m prog ⇒ bool"

abbreviation jmm'_heap_read_typeable :: "'m prog ⇒ bool"

lemma jmm_heap_conf:
by(unfold_locales)(simp_all add: jmm_hconf_def jmm_heap_ops_defs split: if_split_asm)

interpretation jmm: heap_conf
jmm_spurious_wakeups
P
for P
by(rule jmm_heap_conf)

lemmas jmm'_heap_conf = jmm_heap_conf

interpretation jmm': heap_conf
jmm_spurious_wakeups
P
for P
by(rule jmm'_heap_conf)

subsection ‹Locale ‹heap_progress››

lemma jmm_heap_progress:
proof
fix h a al T
assume "jmm_hconf h"
and al: "P,h ⊢jmm a@al : T"
show "∃v. jmm_heap_read h a al v ∧ P,h ⊢jmm v :≤ T"
using jmm.defval_conf[of P P h T] unfolding jmm_heap_ops_defs by blast
next
fix h a al T v
assume "P,h ⊢jmm a@al : T"
show "∃h'. jmm_heap_write h a al v h'"
by(auto intro: jmm_heap_write.intros)
qed

interpretation jmm: heap_progress
jmm_spurious_wakeups
P
for P
by(rule jmm_heap_progress)

lemma jmm'_heap_progress:
proof
fix h a al T
assume "jmm'_hconf h"
and al: "P,h ⊢jmm' a@al : T"
thus "∃v. jmm_heap_read_typed P h a al v ∧ P,h ⊢jmm' v :≤ T"
next
fix h a al T v
assume "P,h ⊢jmm' a@al : T"
and "P,h ⊢jmm' v :≤ T"
thus "∃h'. jmm_heap_write h a al v h'"
by(auto intro: jmm_heap_write.intros)
qed

interpretation jmm': heap_progress
jmm_spurious_wakeups
P
for P
by(rule jmm'_heap_progress)

jmm_spurious_wakeups
P
for P

interpretation jmm': heap_typesafe
jmm_spurious_wakeups
P
for P
..

subsection ‹Locale ‹allocated_heap››

lemma jmm_allocated_heap:
proof
show "jmm_allocated jmm_empty = {}" by(simp add: jmm_allocated_def)
next
fix h' a h hT
assume "(h', a) ∈ jmm_allocate h hT"
thus "jmm_allocated h' = insert a (jmm_allocated h) ∧ a ∉ jmm_allocated h"
by(auto simp add: jmm_heap_ops_defs split: if_split_asm)
next
fix h a al v h'
assume "jmm_heap_write h a al v h'"
thus "jmm_allocated h' = jmm_allocated h" by cases simp
qed

interpretation jmm: allocated_heap
jmm_spurious_wakeups
jmm_allocated
P
for P
by(rule jmm_allocated_heap)

lemmas jmm'_allocated_heap = jmm_allocated_heap

interpretation jmm': allocated_heap
jmm_spurious_wakeups
jmm_allocated
P
for P
by(rule jmm'_allocated_heap)

subsection ‹Syntax translations›

notation jmm'.external_WT' ("_,_ ⊢jmm'' (_∙_'(_')) : _" [50,0,0,0,50] 60)

abbreviation jmm'_red_external ::
⇒ addr extCallRet ⇒ JMM_heap ⇒ bool"
where "jmm'_red_external P ≡ jmm'.red_external (TYPE('m)) P P"

abbreviation jmm'_red_external_syntax ::
⇒ addr extCallRet ⇒ JMM_heap ⇒ bool"
("_,_ ⊢jmm'' (⟨(_∙_'(_')),/_⟩) -_→ext (⟨(_),/(_)⟩)" [50, 0, 0, 0, 0, 0, 0, 0, 0] 51)
where
"P,t ⊢jmm' ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ≡ jmm'_red_external P t h a M vs ta va h'"

abbreviation jmm'_red_external_aggr ::
where "jmm'_red_external_aggr P ≡ jmm'.red_external_aggr TYPE('m) P P"

abbreviation jmm'_heap_copy_loc ::
where "jmm'_heap_copy_loc ≡ jmm'.heap_copy_loc TYPE('m)"

abbreviation jmm'_heap_copies ::