Theory State_Refinement

(*  Title:      JinjaThreads/Execute/State_Refinement.thy
    Author:     Andreas Lochbihler
*)

chapter ‹Schedulers›

section ‹Refinement for multithreaded states›

theory State_Refinement
imports
  "../Framework/FWSemantics"
  "../Common/StartConfig"
begin

type_synonym
  ('l,'t,'m,'m_t,'m_w,'s_i) state_refine = "('l,'t) locks × ('m_t × 'm) × 'm_w × 's_i"

locale state_refine_base =
  fixes final :: "'x ⇒ bool"
  and r :: "'t ⇒ ('x × 'm) ⇒ (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
  and thr_invar :: "'m_t ⇒ bool"
  and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
  and ws_invar :: "'m_w ⇒ bool"
  and is_α :: "'s_i ⇒ 't interrupts"
  and is_invar :: "'s_i ⇒ bool"
begin

fun state_α :: "('l,'t,'m,'m_t,'m_w, 's_i) state_refine ⇒ ('l,'t,'x,'m,'w) state"
where "state_α (ls, (ts, m), ws, is) = (ls, (thr_α ts, m), ws_α ws, is_α is)"

lemma state_α_conv [simp]:
  "locks (state_α s) = locks s"
  "thr (state_α s) = thr_α (thr s)"
  "shr (state_α s) = shr s"
  "wset (state_α s) = ws_α (wset s)"
  "interrupts (state_α s) = is_α (interrupts s)"
by(case_tac [!] s) auto

inductive state_invar :: "('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ bool"
where "⟦ thr_invar ts; ws_invar ws; is_invar is ⟧ ⟹ state_invar (ls, (ts, m), ws, is)"

inductive_simps state_invar_simps [simp]:
  "state_invar (ls, (ts, m), ws, is)"

lemma state_invarD [simp]:
  assumes "state_invar s"
  shows "thr_invar (thr s)" "ws_invar (wset s)" "is_invar (interrupts s)"
using assms by(case_tac [!] s) auto

end

sublocale state_refine_base < α: final_thread final .
sublocale state_refine_base < α:
  multithreaded_base
    final
    "λt xm ta x'm'. Predicate.eval (r t xm) (ta, x'm')"
.

definition (in heap_base) start_state_refine :: 
  "'m_t ⇒ ('thread_id ⇒ ('x × 'addr released_locks) ⇒ 'm_t ⇒ 'm_t) ⇒ 'm_w ⇒ 's_i
  ⇒ (cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'md ⇒ 'addr val list ⇒ 'x) ⇒ 'md prog ⇒ cname ⇒ mname ⇒ 'addr val list
  ⇒ ('addr, 'thread_id, 'heap, 'm_t, 'm_w, 's_i) state_refine"
where
  "⋀is_empty.
  start_state_refine thr_empty thr_update ws_empty is_empty f P C M vs =
  (let (D, Ts, T, m) = method P C M
   in (K$ None, (thr_update start_tid (f D M Ts T (the m) vs, no_wait_locks) thr_empty, start_heap), ws_empty, is_empty))"

definition Jinja_output :: 
  "'s ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) thread_action 
  ⇒ ('thread_id × ('addr, 'thread_id) obs_event list) option"
where "Jinja_output σ t ta = (if ⦃ta⦄⇘o⇙ = [] then None else Some (t, ⦃ta⦄⇘o⇙))"

lemmas [code] =
  heap_base.start_state_refine_def

end