# Theory SC_Collections

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

section ‹Sequential consistency with efficient data structures›

theory SC_Collections
imports
"../Common/Conform"
(*"../../Collections/impl/RBTMapImpl"
"../../Collections/impl/TrieMapImpl"
"../../Collections/impl/ListMapImpl"*)
"../Basic/JT_ICF"
MM
begin

subsection‹Objects and Arrays›

type_synonym fields = "(char, (cname, addr val) lm) tm"
type_synonym array_cells = "(nat, addr val) rbt"
type_synonym array_fields = "(vname, addr val) lm"

datatype heapobj
= Obj cname fields                    ― ‹class instance with class name and fields›
| Arr ty nat array_fields array_cells                 ― ‹element type, size, fields and cell contents›

lemma rec_heapobj [simp]: "rec_heapobj = case_heapobj"
by(auto intro!: ext split: heapobj.split)

primrec obj_ty  :: "heapobj ⇒ htype"
where
"obj_ty (Obj c f)   = Class_type c"
| "obj_ty (Arr t si f e) = Array_type t si"

fun is_Arr :: "heapobj ⇒ bool" where
"is_Arr (Obj C fs)      = False"
| "is_Arr (Arr T f si el) = True"

lemma is_Arr_conv:
"is_Arr arrobj = (∃T si f el. arrobj = Arr T si f el)"
by(cases arrobj, auto)

lemma is_ArrE:
"⟦ is_Arr arrobj; ⋀T si f el. arrobj = Arr T si f el ⟹ thesis ⟧ ⟹ thesis"
"⟦ ¬ is_Arr arrobj; ⋀C fs. arrobj = Obj C fs ⟹ thesis ⟧ ⟹ thesis"
by(cases arrobj, auto)+

definition init_fields :: "((vname × cname) × ty) list ⇒ fields"
where
"init_fields FDTs ≡
foldr (λ((F, D), T) fields.
let F' = String.explode F
in tm_update F' (lm_update D (default_val T)
(case tm_lookup F' fields of None ⇒ lm_empty () | Some lm ⇒ lm)) fields)
FDTs (tm_empty ())"

definition init_fields_array :: "(vname × ty) list ⇒ array_fields"
where
"init_fields_array ≡ lm.to_map ∘ map (λ(F, T). (F, default_val T))"

definition init_cells :: "ty ⇒ nat ⇒ array_cells"
where "init_cells T n = foldl (λcells i. rm_update i (default_val T) cells) (rm_empty ()) [0..<n]"

primrec ― ‹a new, blank object with default values in all fields:›
blank :: "'m prog ⇒ htype ⇒ heapobj"
where
"blank P (Class_type C) = Obj C (init_fields (map (λ(FD, (T, fm)). (FD, T)) (TypeRel.fields P C)))"
| "blank P (Array_type T n) =
Arr T n (init_fields_array (map (λ((F, D), (T, fm)). (F, T)) (TypeRel.fields P Object))) (init_cells T n)"

lemma obj_ty_blank [iff]: "obj_ty (blank P hT) = hT"
by(cases hT) simp_all

subsection‹Heap›

type_synonym heap = "(addr, heapobj) rbt"

translations
(type) "heap" <= (type) "(nat, heapobj) rbt"

abbreviation sc_empty :: heap
where "sc_empty ≡ rm_empty ()"

fun the_obj :: "heapobj ⇒ cname × fields" where
"the_obj (Obj C fs) = (C, fs)"

fun the_arr :: "heapobj ⇒ ty × nat × array_fields × array_cells" where
"the_arr (Arr T si f el) = (T, si, f, el)"

abbreviation
cname_of :: "heap ⇒ addr ⇒ cname" where
"cname_of hp a == fst (the_obj (the (rm_lookup a hp)))"

where "new_Addr h = Some (case rm_max h (λ_. True) of None ⇒ 0 | Some (a, _) ⇒ a + 1)"

definition sc_allocate :: "'m prog ⇒ heap ⇒ htype ⇒ (heap × addr) set"
where
"sc_allocate P h hT =
(case new_Addr h of None ⇒ {}
| Some a ⇒ {(rm_update a (blank P hT) h, a)})"

where "sc_typeof_addr h a = map_option obj_ty (rm_lookup a h)"

for h :: heap and a :: addr
where
Obj: "⟦ rm_lookup a h = ⌊Obj C fs⌋; tm_lookup (String.explode F) fs = ⌊fs'⌋; lm_lookup D fs' = ⌊v⌋ ⟧ ⟹ sc_heap_read h a (CField D F) v"
| Arr: "⟦ rm_lookup a h = ⌊Arr T si f el⌋; n < si ⟧ ⟹ sc_heap_read h a (ACell n) (the (rm_lookup n el))"
| ArrObj: "⟦ rm_lookup a h = ⌊Arr T si f el⌋; lm_lookup F f = ⌊v⌋ ⟧ ⟹ sc_heap_read h a (CField Object F) v"

hide_fact (open) Obj Arr ArrObj

"sc_heap_read h a (CField C F) v"
"sc_heap_read h a (ACell n) v"

for h :: heap and a :: addr
where
Obj:
"⟦ rm_lookup a h = ⌊Obj C fs⌋; F' = String.explode F;
h' = rm_update a (Obj C (tm_update F' (lm_update D v (case tm_lookup (String.explode F) fs of None ⇒ lm_empty () | Some fs' ⇒ fs')) fs)) h ⟧
⟹ sc_heap_write h a (CField D F) v h'"

| Arr:
"⟦ rm_lookup a h = ⌊Arr T si f el⌋; h' = rm_update a (Arr T si f (rm_update n v el)) h ⟧
⟹ sc_heap_write h a (ACell n) v h'"

| ArrObj:
"⟦ rm_lookup a h = ⌊Arr T si f el⌋; h' = rm_update a (Arr T si (lm_update F v f) el) h ⟧
⟹ sc_heap_write h a (CField Object F) v h'"

hide_fact (open) Obj Arr ArrObj

inductive_cases sc_heap_write_cases [elim!]:
"sc_heap_write h a (CField C F) v h'"
"sc_heap_write h a (ACell n) v h'"

consts sc_spurious_wakeups :: bool

lemma new_Addr_SomeD: "new_Addr h = ⌊a⌋ ⟹ rm_lookup a h = None"
apply(drule rm.max_None[OF rm.invar])
apply(frule rm.max_Some[OF rm.invar])
apply(hypsubst_thin)
apply(rule ccontr)
apply(clarsimp)
apply(drule_tac k'="Suc a" in rm.max_Some(2)[OF rm.invar])
done

interpretation sc:
heap_base
"sc_spurious_wakeups"
"sc_empty"
"sc_allocate P"
"sc_heap_write"
for P .

text ‹Translate notation from ‹heap_base››

abbreviation sc_preallocated :: "'m prog ⇒ heap ⇒ bool"
where "sc_preallocated == sc.preallocated TYPE('m)"

abbreviation sc_start_tid :: "'md prog ⇒ thread_id"
where "sc_start_tid ≡ sc.start_tid TYPE('md)"

abbreviation sc_start_heap_ok :: "'m prog ⇒ bool"
where "sc_start_heap_ok ≡ sc.start_heap_ok TYPE('m)"

abbreviation sc_start_heap :: "'m prog ⇒ heap"
where "sc_start_heap ≡ sc.start_heap TYPE('m)"

abbreviation sc_start_state ::
"(cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'm ⇒ addr val list ⇒ 'x)
where
"sc_start_state f P ≡ sc.start_state TYPE('m) P f P"

abbreviation sc_wf_start_state :: "'m prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ bool"
where "sc_wf_start_state P ≡ sc.wf_start_state TYPE('m) P P"

notation sc.conf ("_,_ ⊢sc _ :≤ _"  [51,51,51,51] 50)
notation sc.confs ("_,_ ⊢sc _ [:≤] _" [51,51,51,51] 50)
notation sc.hext ("_ ⊴sc _" [51,51] 50)

lemma sc_start_heap_ok: "sc_start_heap_ok P"
by(simp add: sc.start_heap_ok_def sc.start_heap_data_def initialization_list_def sc.create_initial_object_simps sc_allocate_def case_option_conv_if new_Addr_SomeI sys_xcpts_list_def del: blank.simps split del: option.split if_split)

lemma sc_wf_start_state_iff:
"sc_wf_start_state P C M vs ⟷ (∃Ts T meth D. P ⊢ C sees M:Ts→T = ⌊meth⌋ in D ∧ P,sc_start_heap P ⊢sc vs [:≤] Ts)"

lemma sc_heap:
proof
fix h' a h hT
assume "(h', a) ∈ sc_allocate P h hT"
thus "sc_typeof_addr h' a = ⌊hT⌋"
next
fix h h' hT a
assume "(h', a) ∈ sc_allocate P h hT"
from this[symmetric] show "h ⊴sc h'"
next
fix h a al v h'
assume "sc_heap_write h a al v h'"
thus "h ⊴sc h'"
qed simp

interpretation sc:
heap
"sc_spurious_wakeups"
"sc_empty"
"sc_allocate P"
"sc_heap_write"
P
for P by(rule sc_heap)

lemma sc_hext_new:
"rm_lookup a h = None ⟹ h ⊴sc rm_update a arrobj h"

lemma sc_hext_upd_obj: "rm_lookup a h = Some (Obj C fs) ⟹ h ⊴sc rm_update a (Obj C fs') h"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def rm.lookup_correct rm.update_correct)

lemma sc_hext_upd_arr: "⟦ rm_lookup a h = Some (Arr T si f e) ⟧ ⟹ h ⊴sc rm_update a (Arr T si f' e') h"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def rm.lookup_correct rm.update_correct)

subsection ‹Conformance›

definition sc_oconf :: "'m prog ⇒ heap ⇒ heapobj ⇒ bool"   ("_,_ ⊢sc _ √" [51,51,51] 50)
where
"P,h ⊢sc obj √  ≡
(case obj of
Obj C fs ⇒
is_class P C ∧
(∀F D T fm. P ⊢ C has F:T (fm) in D ⟶
(∃fs' v. tm_α fs (String.explode F) = Some fs' ∧ lm_α fs' D = Some v ∧ P,h ⊢sc v :≤ T))
| Arr T si f el ⇒
is_type P (T⌊⌉) ∧ (∀n. n < si ⟶ (∃v. rm_α el n = Some v ∧ P,h ⊢sc v :≤ T)) ∧
(∀F T fm. P ⊢ Object has F:T (fm) in Object ⟶ (∃v. lm_lookup F f = Some v ∧ P,h ⊢sc v :≤ T)))"

definition sc_hconf :: "'m prog ⇒ heap ⇒ bool"  ("_ ⊢sc _ √" [51,51] 50)
where "P ⊢sc h √ ⟷ (∀a obj. rm_α h a = Some obj ⟶ P,h ⊢sc obj √)"

interpretation sc:
heap_conf_base
"sc_spurious_wakeups"
"sc_empty"
"sc_allocate P"
"sc_heap_write"
"sc_hconf P"
"P"
for P
.

lemma sc_conf_upd_obj: "rm_lookup a h = Some(Obj C fs) ⟹ (P,rm_update a (Obj C fs') h ⊢sc x :≤ T) = (P,h ⊢sc x :≤ T)"
apply (unfold sc.conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
done

lemma sc_conf_upd_arr:
"rm_lookup a h = Some(Arr T si f el) ⟹ (P,rm_update a (Arr T si f' el') h ⊢sc x :≤ T') = (P,h ⊢sc x :≤ T')"
apply(unfold sc.conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
done

lemma sc_oconf_hext: "P,h ⊢sc obj √ ⟹ h ⊴sc h' ⟹ P,h' ⊢sc obj √"
unfolding sc_oconf_def
by(fastforce split: heapobj.split elim: sc.conf_hext)

lemma map_of_fields_init_fields:
assumes "map_of FDTs (F, D) = ⌊(T, fm)⌋"
shows "∃fs' v. tm_α (init_fields (map (λ(FD, (T, fm)). (FD, T)) FDTs)) (String.explode F) = ⌊fs'⌋ ∧ lm_α fs' D = ⌊v⌋ ∧ sc.conf P h v T"
using assms
by(induct FDTs)(auto simp add: tm.lookup_correct tm.update_correct lm.update_correct init_fields_def String.explode_inject)

lemma sc_oconf_init_fields:
assumes "P ⊢ C has_fields FDTs"
shows "P,h ⊢sc (Obj C (init_fields (map (λ(FD, (T, fm)). (FD, T)) FDTs))) √"
using assms has_fields_is_class[OF assms] map_of_fields_init_fields[of FDTs]
by(fastforce simp add: has_field_def sc_oconf_def dest: has_fields_fun)

lemma sc_oconf_init_arr:
assumes type: "is_type P (T⌊⌉)"
shows "P,h ⊢sc Arr T n (init_fields_array (map (λ((F, D), (T, fm)). (F, T)) (TypeRel.fields P Object))) (init_cells T n) √"
proof -
{ fix n'
assume "n' < n"
{ fix rm and k :: nat
assume "∀i<k. ∃v. rm_α rm i = ⌊v⌋ ∧ sc.conf P h v T"
with ‹n' < n› have "∃v. rm_α (foldl (λcells i. rm_update i (default_val T) cells) rm [k..<n]) n' = ⌊v⌋ ∧ sc.conf P h v T"
by(induct m≡"n-k" arbitrary: n k rm)(auto simp add: rm.update_correct upt_conv_Cons type)
}
from this[of 0 "rm_empty ()"]
have "∃v. rm_α (foldl (λcells i. rm_update i (default_val T) cells) (rm_empty ()) [0..<n]) n' = ⌊v⌋ ∧ sc.conf P h v T" by simp
}
moreover
{ fix F T fm
assume "P ⊢ Object has F:T (fm) in Object"
then obtain FDTs where has: "P ⊢ Object has_fields FDTs"
and FDTs: "map_of FDTs (F, Object) = ⌊(T, fm)⌋"
from has have "snd ` fst ` set FDTs ⊆ {Object}" by(rule Object_has_fields_Object)
with FDTs have "map_of (map ((λ(F, T). (F, default_val T)) ∘ (λ((F, D), T, fm). (F, T))) FDTs) F = ⌊default_val T⌋"
by(induct FDTs) auto
with has FDTs
have "∃v. lm_lookup F (init_fields_array (map (λ((F, D), T, fm). (F, T)) (TypeRel.fields P Object))) = ⌊v⌋ ∧
sc.conf P h v T"
by(auto simp add: init_fields_array_def lm_correct has_field_def)
}
ultimately show ?thesis using type by(auto simp add: sc_oconf_def init_cells_def)
qed

lemma sc_oconf_fupd [intro?]:
"⟦ P ⊢ C has F:T (fm) in D; P,h ⊢sc v :≤ T; P,h ⊢sc (Obj C fs) √;
fs' = (case tm_lookup (String.explode F) fs of None ⇒ lm_empty () | Some fs' ⇒ fs') ⟧
⟹ P,h ⊢sc (Obj C (tm_update (String.explode F) (lm_update D v fs') fs)) √"
unfolding sc_oconf_def has_field_def
apply(auto dest: has_fields_fun simp add: lm.update_correct tm.update_correct tm.lookup_correct String.explode_inject)
apply(drule (1) has_fields_fun, fastforce)
apply(drule (1) has_fields_fun, fastforce)
done

lemma sc_oconf_fupd_arr [intro?]:
"⟦ P,h ⊢sc v :≤ T; P,h ⊢sc (Arr T si f el) √ ⟧
⟹ P,h ⊢sc (Arr T si f (rm_update i v el)) √"
unfolding sc_oconf_def

lemma sc_oconf_fupd_arr_fields:
"⟦ P ⊢ Object has F:T (fm) in Object; P,h ⊢sc v :≤ T; P,h ⊢sc (Arr T' si f el) √ ⟧
⟹ P,h ⊢sc (Arr T' si (lm_update F v f) el) √"
unfolding sc_oconf_def by(auto dest: has_field_fun simp add: lm_correct)

lemma sc_oconf_new: "⟦ P,h ⊢sc obj √; rm_lookup a h = None ⟧ ⟹ P,rm_update a arrobj h ⊢sc obj √"
by(erule sc_oconf_hext)(rule sc_hext_new)

lemmas sc_oconf_upd_obj = sc_oconf_hext [OF _ sc_hext_upd_obj]

lemma sc_oconf_upd_arr:
assumes "P,h ⊢sc obj √"
and ha: "rm_lookup a h = ⌊Arr T si f el⌋"
shows "P,rm_update a (Arr T si f' el') h ⊢sc obj √"
using assms
by(fastforce simp add: sc_oconf_def sc_conf_upd_arr[OF ha] split: heapobj.split)

lemma sc_oconf_blank: "is_htype P hT ⟹ P,h ⊢sc blank P hT √"
apply(cases hT)
apply(fastforce dest: map_of_fields_init_fields simp add: has_field_def sc_oconf_def)
by(auto intro: sc_oconf_init_arr)

lemma sc_hconfD: "⟦ P ⊢sc h √; rm_lookup a h = Some obj ⟧ ⟹ P,h ⊢sc obj √"
unfolding sc_hconf_def by(auto simp add: rm.lookup_correct)

lemmas sc_preallocated_new = sc.preallocated_hext[OF _ sc_hext_new]
lemmas sc_preallocated_upd_obj = sc.preallocated_hext [OF _ sc_hext_upd_obj]
lemmas sc_preallocated_upd_arr = sc.preallocated_hext [OF _ sc_hext_upd_arr]

lemma sc_hconf_new: "⟦ P ⊢sc h √; rm_lookup a h = None; P,h ⊢sc obj √ ⟧ ⟹ P ⊢sc rm_update a obj h √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_new simp add: rm.lookup_correct rm.update_correct)

lemma sc_hconf_upd_obj: "⟦ P ⊢sc h √; rm_lookup a h = Some (Obj C fs); P,h ⊢sc (Obj C fs') √ ⟧ ⟹ P ⊢sc rm_update a (Obj C fs') h √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_obj simp add: rm.lookup_correct rm.update_correct)

lemma sc_hconf_upd_arr: "⟦ P ⊢sc h √; rm_lookup a h = Some(Arr T si f el); P,h ⊢sc (Arr T si f' el') √ ⟧ ⟹ P ⊢sc rm_update a (Arr T si f' el') h √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_arr simp add: rm.lookup_correct rm.update_correct)

lemma sc_heap_conf:
proof
show "P ⊢sc sc_empty √" by(simp add: sc_hconf_def rm.empty_correct)
next
fix h a hT
assume "sc_typeof_addr h a = ⌊hT⌋" "P ⊢sc h √"
thus "is_htype P hT"
next
fix h' hT h a
assume "P ⊢sc h √" "(h', a) ∈ sc_allocate P h hT" "is_htype P hT"
thus "P ⊢sc h' √"
next
fix h a al T v h'
assume "P ⊢sc h √"
and "sc.addr_loc_type P h a al T"
and "P,h ⊢sc v :≤ T"
and "sc_heap_write h a al v h'"
thus "P ⊢sc h' √"
qed

interpretation sc:
heap_conf
"sc_spurious_wakeups"
"sc_empty"
"sc_allocate P"
"sc_heap_write"
"sc_hconf P"
"P"
for P
by(rule sc_heap_conf)

lemma sc_heap_progress:
proof
fix h a al T
assume hconf: "P ⊢sc h √"
and alt: "sc.addr_loc_type P h a al T"
from alt obtain arrobj where arrobj: "rm_lookup a h = ⌊arrobj⌋"
from alt show "∃v. sc_heap_read h a al v ∧ P,h ⊢sc v :≤ T"
proof(cases)
case (addr_loc_type_field U F fm D)
note [simp] = ‹al = CField D F›
show ?thesis
proof(cases "arrobj")
case (Obj C' fs)
with ‹sc_typeof_addr h a = ⌊U⌋› arrobj
from hconf arrobj Obj have "P,h ⊢sc Obj (class_type_of U) fs √" by(auto dest: sc_hconfD)
with ‹P ⊢ class_type_of U has F:T (fm) in D› obtain fs' v
where "tm_lookup (String.explode F) fs = ⌊fs'⌋" "lm_lookup D fs' = ⌊v⌋" "P,h ⊢sc v :≤ T"
by(fastforce simp add: sc_oconf_def tm.lookup_correct lm.lookup_correct)
thus ?thesis using Obj arrobj by(auto intro: sc_heap_read.intros)
next
case (Arr T' si f el)
with ‹sc_typeof_addr h a = ⌊U⌋› arrobj
from hconf arrobj Arr have "P,h ⊢sc Arr T' si f el √" by(auto dest: sc_hconfD)
from ‹P ⊢ class_type_of U has F:T (fm) in D› have [simp]: "D = Object"
by(auto dest: has_field_decl_above)
with ‹P,h ⊢sc Arr T' si f el √› ‹P ⊢ class_type_of U has F:T (fm) in D›
obtain v where "lm_lookup F f = ⌊v⌋" "P,h ⊢sc v :≤ T"
thus ?thesis using Arr arrobj by(auto intro: sc_heap_read.intros)
qed
next
with arrobj obtain si f el
where [simp]: "arrobj = Arr T si f el"
have [simp]: "al = ACell n" and n: "n < si" by(auto simp add: sc_typeof_addr_def)
from hconf arrobj have "P,h ⊢sc Arr T si f el √" by(auto dest: sc_hconfD)
with n obtain v where "rm_lookup n el = ⌊v⌋" "P,h ⊢sc v :≤ T"
thus ?thesis using arrobj n by(fastforce intro: sc_heap_read.intros)
qed
next
fix h a al T v
assume alt: "sc.addr_loc_type P h a al T"
from alt obtain arrobj where arrobj: "rm_lookup a h = ⌊arrobj⌋"
thus "∃h'. sc_heap_write h a al v h'" using alt
qed

interpretation sc:
heap_progress
"sc_spurious_wakeups"
"sc_empty"
"sc_allocate P"
"sc_heap_write"
"sc_hconf P"
"P"
for P
by(rule sc_heap_progress)

proof
fix h a al v T
and alt: "sc.addr_loc_type P h a al T"
and hconf: "P ⊢sc h √"
thus "P,h ⊢sc v :≤ T"
apply(fastforce dest!: sc_hconfD simp add: sc_oconf_def tm.lookup_correct lm.lookup_correct rm.lookup_correct)+
done
qed

interpretation sc:
"sc_spurious_wakeups"
"sc_empty"
"sc_allocate P"
"sc_heap_write"
"sc_hconf P"
"P"
for P

abbreviation sc_deterministic_heap_ops :: "'m prog ⇒ bool"
where "sc_deterministic_heap_ops ≡ sc.deterministic_heap_ops TYPE('m)"

lemma sc_deterministic_heap_ops: "¬ sc_spurious_wakeups ⟹ sc_deterministic_heap_ops P"

subsection ‹Code generation›

code_pred
(modes: i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ bool)

code_pred
(modes: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool)
sc_heap_write .