Theory JVM_Execute

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

theory JVM_Execute
imports
  SC_Schedulers
  JVMExec_Execute
  "../BV/BVProgressThreaded"
begin

abbreviation sc_heap_read_cset :: "heap ⇒ addr ⇒ addr_loc ⇒ addr val set"
where "sc_heap_read_cset h ad al ≡ set_of_pred (sc_heap_read_i_i_i_o h ad al)"

abbreviation sc_heap_write_cset :: "heap ⇒ addr ⇒ addr_loc ⇒ addr val ⇒ heap set"
where "sc_heap_write_cset h ad al v ≡ set_of_pred (sc_heap_write_i_i_i_i_o h ad al v)"

interpretation sc: 
  JVM_heap_execute
    "addr2thread_id"
    "thread_id2addr"
    "sc_spurious_wakeups"
    "sc_empty"
    "sc_allocate P"
    "sc_typeof_addr"
    "sc_heap_read_cset"
    "sc_heap_write_cset"
  rewrites "⋀h ad al v. v ∈ sc_heap_read_cset h ad al ≡ sc_heap_read h ad al v"
  and "⋀h ad al v h'. h' ∈ sc_heap_write_cset h ad al v ≡ sc_heap_write h ad al v h'"
  for P
apply(simp_all add: eval_sc_heap_read_i_i_i_o eval_sc_heap_write_i_i_i_i_o)
done

interpretation sc_execute: 
  JVM_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"
  for P
by(unfold_locales)

fun sc_mexec :: 
  "addr jvm_prog ⇒ thread_id ⇒ (addr jvm_thread_state × heap) 
  ⇒ ((addr, thread_id, heap) jvm_thread_action × addr jvm_thread_state × heap) Predicate.pred"
where 
  "sc_mexec P t ((xcp, frs), h) =
   sc.exec_1 (TYPE(addr jvm_method)) P P t (xcp, h, frs) ⤜ (λ(ta, xcp, h, frs). Predicate.single (ta, (xcp, frs), h))"

abbreviation sc_jvm_start_state_refine :: 
  "addr jvm_prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ 
  (addr, thread_id, heap, (thread_id, (addr jvm_thread_state) × addr released_locks) rm, (thread_id, addr wait_set_status) rm, thread_id rs) state_refine"
where
  "sc_jvm_start_state_refine ≡ 
   sc_start_state_refine (rm_empty ()) rm_update (rm_empty ()) (rs_empty ()) (λC M Ts T (mxs, mxl0, b) vs. (None, [([], Null # vs @ replicate mxl0 undefined_value, C, M, 0)]))"

abbreviation sc_jvm_state_invar :: "addr jvm_prog ⇒ tyP ⇒ (addr,thread_id,addr jvm_thread_state,heap,addr) state set"
where "sc_jvm_state_invar P Φ ≡ {s. sc_execute.correct_state_ts P Φ (thr s) (shr s)}"

lemma eval_sc_mexec:
  "(λt xm ta x'm'. Predicate.eval (sc_mexec P t xm) (ta, x'm')) = 
  (λt ((xcp, frs), h) ta ((xcp', frs'), h'). sc.execute.exec_1 (TYPE(addr jvm_method)) P P t (xcp, h, frs) ta (xcp', h', frs'))"
by(rule ext)+(fastforce intro!: SUP1_I simp add: sc.exec_1_eq')

lemma sc_jvm_start_state_invar: 
  assumes "wf_jvm_prog⇘Φ⇙ P"
  and "sc_wf_start_state P C M vs"
  shows "sc_state_α (sc_jvm_start_state_refine P C M vs) ∈ sc_jvm_state_invar P Φ"
using sc_execute.correct_jvm_state_initial[OF assms]
by(simp add: sc_execute.correct_jvm_state_def)

subsection ‹Round-robin scheduler›

interpretation JVM_rr: 
  sc_round_robin_base
    JVM_final "sc_mexec P" convert_RA Jinja_output
  for P
.

definition sc_rr_JVM_start_state :: "nat ⇒ 'm prog ⇒ thread_id fifo round_robin"
where "sc_rr_JVM_start_state n0 P = JVM_rr.round_robin_start n0 (sc_start_tid P)"

definition exec_JVM_rr ::
  "nat ⇒ addr jvm_prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ 
  (thread_id × (addr, thread_id) obs_event list, 
   (addr, thread_id) locks × ((thread_id, addr jvm_thread_state × addr released_locks) rm × heap) ×
   (thread_id, addr wait_set_status) rm × thread_id rs) tllist"
where
  "exec_JVM_rr n0 P C M vs = JVM_rr.exec P n0 (sc_rr_JVM_start_state n0 P) (sc_jvm_start_state_refine P C M vs)"

interpretation JVM_rr:
  sc_round_robin 
    JVM_final "sc_mexec P" convert_RA Jinja_output
  for P
by(unfold_locales)

lemma JVM_rr:
  assumes "wf_jvm_prog⇘Φ⇙ P"
  shows
  "sc_scheduler 
     JVM_final (sc_mexec P) convert_RA
     (JVM_rr.round_robin P n0) (pick_wakeup_via_sel (λs P. rm_sel s (λ(k,v). P k v))) JVM_rr.round_robin_invar
     (sc_jvm_state_invar P Φ)"
unfolding sc_scheduler_def
apply(rule JVM_rr.round_robin_scheduler)
apply(unfold eval_sc_mexec)
apply(rule sc_execute.mexec_deterministic[OF assms sc_deterministic_heap_ops])
apply(simp add: sc_spurious_wakeups)
done

subsection ‹Random scheduler›

interpretation JVM_rnd: 
  sc_random_scheduler_base
    JVM_final "sc_mexec P" convert_RA Jinja_output
  for P
.

definition sc_rnd_JVM_start_state :: "Random.seed ⇒ random_scheduler"
where "sc_rnd_JVM_start_state seed = seed"

definition exec_JVM_rnd ::
  "Random.seed ⇒ addr jvm_prog ⇒ cname ⇒ mname ⇒ addr val list ⇒ 
  (thread_id × (addr, thread_id) obs_event list,
   (addr, thread_id) locks × ((thread_id, addr jvm_thread_state × addr released_locks) rm × heap) ×
   (thread_id, addr wait_set_status) rm × thread_id rs) tllist"
where "exec_JVM_rnd seed P C M vs = JVM_rnd.exec P (sc_rnd_JVM_start_state seed) (sc_jvm_start_state_refine P C M vs)"

interpretation JVM_rnd:
  sc_random_scheduler
    JVM_final "sc_mexec P" convert_RA Jinja_output
  for P
by(unfold_locales)

lemma JVM_rnd:
  assumes "wf_jvm_prog⇘Φ⇙ P"
  shows 
  "sc_scheduler
    JVM_final (sc_mexec P) convert_RA
    (JVM_rnd.random_scheduler P) (pick_wakeup_via_sel (λs P. rm_sel s (λ(k,v). P k v))) (λ_ _. True)
    (sc_jvm_state_invar P Φ)"
unfolding sc_scheduler_def
apply(rule JVM_rnd.random_scheduler_scheduler)
apply(unfold eval_sc_mexec)
apply(rule sc_execute.mexec_deterministic[OF assms sc_deterministic_heap_ops])
apply(simp add: sc_spurious_wakeups)
done

ML_val ‹@{code exec_JVM_rr}›

ML_val ‹@{code exec_JVM_rnd}›

end