Theory State_Refinement

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

chapter ‹Schedulers›

section ‹Refinement for multithreaded states›

theory State_Refinement

  ('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"

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


sublocale state_refine_base < α: final_thread final .
sublocale state_refine_base < α:
    "λ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"
  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 tao = [] then None else Some (t, tao))"

lemmas [code] =