Theory SC

(*  Title:      JinjaThreads/MM/SC.thy
    Author:     David von Oheimb, Andreas Lochbihler

    Based on the Jinja theories Common/Objects.thy and Common/Conform by David von Oheimb
*)

section ‹Sequential consistency›

theory SC
imports 
  "../Common/Conform"
  MM
begin

subsection‹Objects and Arrays›

type_synonym 
  fields = "vname × cname ⇀ addr val"       ― ‹field name, defining class, value›

type_synonym
  cells = "addr val list"

datatype heapobj
  = Obj cname fields
    ― ‹class instance with class name and fields›

  | Arr ty fields cells
    ― ‹element type, fields (from object), and list of each cell's content›

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 fs cs) = Array_type T (length cs)"

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

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

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

definition init_fields :: "('field_name × (ty × fmod)) list ⇒ 'field_name ⇀ addr val"
where "init_fields ≡ map_of ∘ map (λ(FD,(T, fm)). (FD,default_val T))"

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 (fields P C))"
| "blank P (Array_type T n) = Arr T (init_fields (fields P Object)) (replicate n (default_val T))"

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


subsection‹Heap›

type_synonym heap = "addr ⇀ heapobj"

translations
  (type) "heap" <= (type) "nat ⇒ heapobj option"

abbreviation sc_empty :: heap
where "sc_empty ≡ Map.empty"

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

fun the_arr :: "heapobj ⇒ ty × fields × cells" where
  "the_arr (Arr T f el) = (T, f, el)"

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

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

definition sc_typeof_addr :: "heap ⇒ addr ⇒ htype option"
where "sc_typeof_addr h a = map_option obj_ty (h a)"

inductive sc_heap_read :: "heap ⇒ addr ⇒ addr_loc ⇒ addr val ⇒ bool"
for h :: heap and a :: addr
where
  Obj: "⟦ h a = ⌊Obj C fs⌋; fs (F, D) = ⌊v⌋ ⟧ ⟹ sc_heap_read h a (CField D F) v"
| Arr: "⟦ h a = ⌊Arr T f el⌋; n < length el ⟧ ⟹ sc_heap_read h a (ACell n) (el ! n)"
| ArrObj: "⟦ h a = ⌊Arr T f el⌋; f (F, Object) = ⌊v⌋ ⟧ ⟹ sc_heap_read h a (CField Object F) v"

hide_fact (open) Obj Arr ArrObj

inductive_cases sc_heap_read_cases [elim!]:
  "sc_heap_read h a (CField C F) v"
  "sc_heap_read h a (ACell n) v"

inductive sc_heap_write :: "heap ⇒ addr ⇒ addr_loc ⇒ addr val ⇒ heap ⇒ bool"
for h :: heap and a :: addr
where
  Obj: "⟦ h a = ⌊Obj C fs⌋; h' = h(a ↦ Obj C (fs((F, D) ↦ v))) ⟧ ⟹ sc_heap_write h a (CField D F) v h'"
| Arr: "⟦ h a = ⌊Arr T f el⌋; h' = h(a ↦ Arr T f (el[n := v])) ⟧ ⟹ sc_heap_write h a (ACell n) v h'"
| ArrObj: "⟦ h a = ⌊Arr T f el⌋; h' = h(a ↦ Arr T (f((F, Object) ↦ v)) el) ⟧ ⟹ 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

interpretation sc: 
  heap_base
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read"
    "sc_heap_write"
  for P .

text ‹Translate notation from ‹heap_base››

(* FIXME! Why does sc.preallocated need the type token?? *)
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)
  ⇒ 'm prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ (addr, thread_id, 'x, heap, addr) state"
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"
apply(simp add: sc.start_heap_ok_def sc.start_heap_data_def initialization_list_def sc.create_initial_object_simps sc_allocate_def sys_xcpts_list_def case_option_conv_if new_Addr_SomeI del: blank.simps split del: option.split if_split)
done

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)"
by(simp add: sc.wf_start_state.simps sc_start_heap_ok)

lemma sc_heap:
  "heap addr2thread_id thread_id2addr (sc_allocate P) sc_typeof_addr sc_heap_write P"
proof
  fix h' a h hT
  assume "(h', a) ∈ sc_allocate P h hT"
  thus "sc_typeof_addr h' a = ⌊hT⌋"
    by(auto simp add: sc_allocate_def sc_typeof_addr_def dest: new_Addr_SomeD split: if_split_asm)
next
  fix h' h hT a
  assume "(h', a) ∈ sc_allocate P h hT"
  from this[symmetric] show "h ⊴sc h'"
    by(fastforce simp add: sc_allocate_def sc_typeof_addr_def sc.hext_def dest: new_Addr_SomeD intro!: map_leI)
next
  fix h a al v h'
  assume "sc_heap_write h a al v h'"
  thus "h ⊴sc h'"
    by(cases al)(auto intro!: sc.hextI simp add: sc_typeof_addr_def)
qed simp

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

lemma sc_hext_new:
  "h a = None ⟹ h ⊴sc h(a ↦ arrobj)"
by(rule sc.hextI)(auto simp add: sc_typeof_addr_def dest!: new_Addr_SomeD)

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

lemma sc_hext_upd_arr: "⟦ h a = Some (Arr T f e); length e = length e' ⟧ ⟹ h ⊴sc h(a↦(Arr T f' e'))"
by(rule sc.hextI)(auto simp:fun_upd_apply sc_typeof_addr_def)

subsection ‹Conformance›

definition sc_fconf :: "'m prog ⇒ cname ⇒ heap ⇒ fields ⇒ bool" (‹_,_,_ ⊢sc _ √› [51,51,51,51] 50)
where "P,C,h ⊢sc fs √ = (∀F D T fm. P ⊢ C has F:T (fm) in D ⟶ (∃v. fs(F,D) = Some v ∧ P,h ⊢sc v :≤ T))"

primrec sc_oconf :: "'m prog ⇒ heap ⇒ heapobj ⇒ bool"   (‹_,_ ⊢sc _ √› [51,51,51] 50)
where
  "P,h ⊢sc Obj C fs √ ⟷ is_class P C ∧ P,C,h ⊢sc fs √"
| "P,h ⊢sc Arr T fs el √ ⟷ is_type P (T⌊⌉) ∧ P,Object,h ⊢sc fs √ ∧ (∀v ∈ set el. P,h ⊢sc v :≤ T)"

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

interpretation sc: heap_conf_base  
  "addr2thread_id"
  "thread_id2addr"
  "sc_spurious_wakeups"
  "sc_empty"
  "sc_allocate P"
  "sc_typeof_addr"
  "sc_heap_read"
  "sc_heap_write"
  "sc_hconf P"
  "P"
for P .

declare sc.typeof_addr_thread_id2_addr_addr2thread_id [simp del]

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

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

lemma sc_oconf_hext: "P,h ⊢sc obj √ ⟹ h ⊴sc h' ⟹ P,h' ⊢sc obj √"
by(cases obj)(fastforce elim: sc.conf_hext simp add: sc_fconf_def)+

lemma sc_oconf_init_fields:
  assumes "P ⊢ C has_fields FDTs"
  shows "P,h ⊢sc (Obj C (init_fields FDTs)) √"
using assms has_fields_is_class[OF assms]
by(auto simp add: has_field_def init_fields_def sc_fconf_def split_def o_def map_of_map[simplified split_def, where f="λp. default_val (fst p)"] dest: has_fields_fun)

lemma sc_oconf_init:
 "is_htype P hT ⟹ P,h ⊢sc blank P hT √"
by(cases hT)(auto simp add: sc_fconf_def has_field_def init_fields_def split_def o_def map_of_map[simplified split_def, where f="λp. default_val (fst p)"] dest: has_fields_fun)

lemma sc_oconf_fupd [intro?]:
  "⟦ P ⊢ C has F:T (fm) in D; P,h ⊢sc v :≤ T; P,h ⊢sc (Obj C fs) √ ⟧ 
  ⟹ P,h ⊢sc (Obj C (fs((F,D)↦v))) √"
unfolding has_field_def
by(auto simp add: sc_fconf_def has_field_def dest: has_fields_fun)

lemma sc_oconf_fupd_arr [intro?]:
  "⟦ P,h ⊢sc v :≤ T; P,h ⊢sc (Arr T f el) √ ⟧
  ⟹ P,h ⊢sc (Arr T f (el[i := v])) √"
by(auto dest: subsetD[OF set_update_subset_insert])

lemma sc_oconf_fupd_arr_fields:
  "⟦ P ⊢ Object has F:T (fm) in Object; P,h ⊢sc v :≤ T; P,h ⊢sc (Arr T' f el) √ ⟧
  ⟹ P,h ⊢sc (Arr T' (f((F, Object) ↦ v)) el) √"
by(auto dest: has_fields_fun simp add: sc_fconf_def has_field_def)

lemma sc_oconf_new: "⟦ P,h ⊢sc obj √; h a = None ⟧ ⟹ P,h(a ↦ arrobj) ⊢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: "h a = ⌊Arr T f el⌋"
  shows "P,h(a ↦ Arr T f' el') ⊢sc obj √"
using assms
by(cases obj)(auto simp add: sc_conf_upd_arr[where h=h, OF ha] sc_fconf_def)

lemma sc_hconfD: "⟦ P ⊢sc h √; h a = Some obj ⟧ ⟹ P,h ⊢sc obj √"
unfolding sc_hconf_def by blast

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 √; h a = None; P,h ⊢sc obj √ ⟧ ⟹ P ⊢sc h(a↦obj) √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_new)

lemma sc_hconf_upd_obj: "⟦ P ⊢sc h √; h a = Some (Obj C fs); P,h ⊢sc (Obj C fs') √ ⟧ ⟹ P ⊢sc h(a↦(Obj C fs')) √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_obj simp del: sc_oconf.simps)

lemma sc_hconf_upd_arr: "⟦ P ⊢sc h √; h a = Some(Arr T f el); P,h ⊢sc (Arr T f' el') √ ⟧ ⟹ P ⊢sc h(a↦(Arr T f' el')) √"
unfolding sc_hconf_def
by(auto intro: sc_oconf_upd_arr simp del: sc_oconf.simps)

lemma sc_heap_conf: 
  "heap_conf addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_write (sc_hconf P) P"
proof
  show "P ⊢sc sc_empty √" by(simp add: sc_hconf_def)
next
  fix h a hT
  assume "sc_typeof_addr h a = ⌊hT⌋" "P ⊢sc h √"
  thus "is_htype P hT"
    by(auto simp add: sc_typeof_addr_def sc_oconf_def dest!: sc_hconfD split: heapobj.split_asm)
next
  fix h h' hT a
  assume "P ⊢sc h √" "(h', a) ∈ sc_allocate P h hT" "is_htype P hT"
  thus "P ⊢sc h' √"
    by(auto simp add: sc_allocate_def dest!: new_Addr_SomeD intro: sc_hconf_new sc_oconf_init split: if_split_asm)
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' √"
    by(cases al)(fastforce elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def intro: sc_hconf_upd_obj sc_oconf_fupd sc_hconfD sc_hconf_upd_arr sc_oconf_fupd_arr sc_oconf_fupd_arr_fields)+
qed

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

lemma sc_heap_progress:
  "heap_progress addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write (sc_hconf P) P"
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: "h a = ⌊arrobj⌋"
    by(auto elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
  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
      have [simp]: "C' = class_type_of U" by(auto simp add: sc_typeof_addr_def)
      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 v 
        where "fs (F, D) = ⌊v⌋" "P,h ⊢sc v :≤ T" by(fastforce simp add: sc_fconf_def)
      thus ?thesis using Obj arrobj by(auto intro: sc_heap_read.intros)
    next
      case (Arr T' f el)
      with ‹sc_typeof_addr h a = ⌊U⌋› arrobj
      have [simp]: "U = Array_type T' (length el)" by(auto simp add: sc_typeof_addr_def)
      from hconf arrobj Arr have "P,h ⊢sc Arr T' 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' f el √› ‹P ⊢ class_type_of U has F:T (fm) in D›
      obtain v where "f (F, Object) = ⌊v⌋" "P,h ⊢sc v :≤ T"
        by(fastforce simp add: sc_fconf_def)
      thus ?thesis using Arr arrobj by(auto intro: sc_heap_read.intros)
    qed
  next
    case (addr_loc_type_cell n' n)
    with arrobj obtain f el
      where [simp]: "arrobj = Arr T f el"
      by(cases arrobj)(auto simp add: sc_typeof_addr_def)
    from addr_loc_type_cell arrobj
    have [simp]: "al = ACell n" "n < length el" by(auto simp add: sc_typeof_addr_def)
    from hconf arrobj have "P,h ⊢sc Arr T f el √" by(auto dest: sc_hconfD)
    hence "P,h ⊢sc el ! n :≤ T" by(fastforce)
    thus ?thesis using arrobj 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: "h a = ⌊arrobj⌋"
    by(auto elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def)
  thus "∃h'. sc_heap_write h a al v h'" using alt
    by(cases arrobj)(fastforce intro: sc_heap_write.intros elim!: sc.addr_loc_type.cases simp add: sc_typeof_addr_def dest: has_field_decl_above)+
qed

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

lemma sc_heap_conf_read:
  "heap_conf_read addr2thread_id thread_id2addr sc_empty (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write (sc_hconf P) P"
proof
  fix h a al v T
  assume read: "sc_heap_read h a al v"
    and alt: "sc.addr_loc_type P h a al T"
    and hconf: "P ⊢sc h √"
  thus "P,h ⊢sc v :≤ T"
    by(auto elim!: sc_heap_read.cases sc.addr_loc_type.cases simp add: sc_typeof_addr_def)(fastforce dest!: sc_hconfD simp add: sc_fconf_def)+
qed

interpretation sc: heap_conf_read
  "addr2thread_id"
  "thread_id2addr"
  "sc_spurious_wakeups"
  "sc_empty"
  "sc_allocate P"
  "sc_typeof_addr"
  "sc_heap_read"
  "sc_heap_write"
  "sc_hconf P"
  "P"
for P
by(rule sc_heap_conf_read)

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"
by(rule sc.deterministic_heap_opsI)(auto elim: sc_heap_read.cases sc_heap_write.cases simp add: sc_allocate_def)

subsection ‹Code generation›

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

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

lemma eval_sc_heap_read_i_i_i_o:
  "Predicate.eval (sc_heap_read_i_i_i_o h ad al) = sc_heap_read h ad al"
by(auto elim: sc_heap_read_i_i_i_oE intro: sc_heap_read_i_i_i_oI intro!: ext)

lemma eval_sc_heap_write_i_i_i_i_o:
  "Predicate.eval (sc_heap_write_i_i_i_i_o h ad al v) = sc_heap_write h ad al v"
by(auto elim: sc_heap_write_i_i_i_i_oE intro: sc_heap_write_i_i_i_i_oI intro!: ext)

end