Theory Random_Scheduler

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

section ‹Random scheduler›

theory Random_Scheduler
imports
  Scheduler
begin

type_synonym random_scheduler = Random.seed

abbreviation (input)
  random_scheduler_invar :: "random_scheduler ⇒ 't set ⇒ bool"
where "random_scheduler_invar ≡ λ_ _. True"

locale random_scheduler_base =
  scheduler_ext_base
    final r convert_RA
    thr_α thr_invar thr_lookup thr_update thr_iterate
    ws_α ws_invar ws_lookup ws_update ws_sel
    is_α is_invar is_memb is_ins is_delete
    thr'_α thr'_invar thr'_empty thr'_ins_dj
  for 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 "output" :: "random_scheduler ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"
  and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
  and thr_invar :: "'m_t ⇒ bool"
  and thr_lookup :: "'t ⇒ 'm_t ⇀ ('x × 'l released_locks)"
  and thr_update :: "'t ⇒ 'x × 'l released_locks ⇒ 'm_t ⇒ 'm_t"
  and thr_iterate :: "'m_t ⇒ ('t × ('x × 'l released_locks), 's_t) set_iterator"
  and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
  and ws_invar :: "'m_w ⇒ bool"
  and ws_lookup :: "'t ⇒ 'm_w ⇀ 'w wait_set_status"
  and ws_update :: "'t ⇒ 'w wait_set_status ⇒ 'm_w ⇒ 'm_w"
  and ws_delete :: "'t ⇒ 'm_w ⇒ 'm_w"
  and ws_iterate :: "'m_w ⇒ ('t × 'w wait_set_status, 'm_w) set_iterator"
  and ws_sel :: "'m_w ⇒ ('t × 'w wait_set_status ⇒ bool) ⇀ ('t × 'w wait_set_status)"
  and is_α :: "'s_i ⇒ 't interrupts"
  and is_invar :: "'s_i ⇒ bool"
  and is_memb :: "'t ⇒ 's_i ⇒ bool"
  and is_ins :: "'t ⇒ 's_i ⇒ 's_i"
  and is_delete :: "'t ⇒ 's_i ⇒ 's_i"
  and thr'_α :: "'s_t ⇒ 't set"
  and thr'_invar :: "'s_t ⇒ bool"
  and thr'_empty :: "unit ⇒ 's_t"
  and thr'_ins_dj :: "'t ⇒ 's_t ⇒ 's_t"
  +
  fixes thr'_to_list :: "'s_t ⇒ 't list"
begin

definition next_thread :: "random_scheduler ⇒ 's_t ⇒ ('t × random_scheduler) option"
where
  "next_thread seed active = 
  (let ts = thr'_to_list active
   in if ts = [] then None else Some (Random.select (thr'_to_list active) seed))"

definition random_scheduler :: "('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,random_scheduler) scheduler"
where
  "random_scheduler seed s =
   (do {
      (t, seed') ← next_thread seed (active_threads s);
      step_thread (λta. seed') s t
   })"

end

locale random_scheduler =
  random_scheduler_base
    final r convert_RA "output"
    thr_α thr_invar thr_lookup thr_update thr_iterate
    ws_α ws_invar ws_lookup ws_update ws_delete ws_iterate ws_sel
    is_α is_invar is_memb is_ins is_delete
    thr'_α thr'_invar thr'_empty thr'_ins_dj thr'_to_list
  +
  scheduler_ext_aux
    final r convert_RA
    thr_α thr_invar thr_lookup thr_update thr_iterate
    ws_α ws_invar ws_lookup ws_update ws_sel
    is_α is_invar is_memb is_ins is_delete
    thr'_α thr'_invar thr'_empty thr'_ins_dj
  +
  ws: map_delete ws_α ws_invar ws_delete +
  ws: map_iteratei ws_α ws_invar ws_iterate +
  thr': set_to_list thr'_α thr'_invar thr'_to_list 
  for 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 "output" :: "random_scheduler ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"
  and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
  and thr_invar :: "'m_t ⇒ bool"
  and thr_lookup :: "'t ⇒ 'm_t ⇀ ('x × 'l released_locks)"
  and thr_update :: "'t ⇒ 'x × 'l released_locks ⇒ 'm_t ⇒ 'm_t"
  and thr_iterate :: "'m_t ⇒ ('t × ('x × 'l released_locks), 's_t) set_iterator"
  and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
  and ws_invar :: "'m_w ⇒ bool"
  and ws_lookup :: "'t ⇒ 'm_w ⇀ 'w wait_set_status"
  and ws_update :: "'t ⇒ 'w wait_set_status ⇒ 'm_w ⇒ 'm_w"
  and ws_delete :: "'t ⇒ 'm_w ⇒ 'm_w"
  and ws_iterate :: "'m_w ⇒ ('t × 'w wait_set_status, 'm_w) set_iterator"
  and ws_sel :: "'m_w ⇒ ('t × 'w wait_set_status ⇒ bool) ⇀ ('t × 'w wait_set_status)"
  and is_α :: "'s_i ⇒ 't interrupts"
  and is_invar :: "'s_i ⇒ bool"
  and is_memb :: "'t ⇒ 's_i ⇒ bool"
  and is_ins :: "'t ⇒ 's_i ⇒ 's_i"
  and is_delete :: "'t ⇒ 's_i ⇒ 's_i"
  and thr'_α :: "'s_t ⇒ 't set"
  and thr'_invar :: "'s_t ⇒ bool"
  and thr'_empty :: "unit ⇒ 's_t"
  and thr'_ins_dj :: "'t ⇒ 's_t ⇒ 's_t"
  and thr'_to_list :: "'s_t ⇒ 't list"
begin

lemma next_thread_eq_None_iff:
  assumes "thr'_invar active" "random_scheduler_invar seed T"
  shows "next_thread seed active = None ⟷ thr'_α active = {}"
using thr'.to_list_correct[OF assms(1)]
by(auto simp add: next_thread_def neq_Nil_conv)

lemma next_thread_eq_SomeD:
  assumes "next_thread seed active = Some (t, seed')"
  and "thr'_invar active" "random_scheduler_invar seed T"
  shows "t ∈ thr'_α active"
using assms
by(auto simp add: next_thread_def thr'.to_list_correct split: if_split_asm dest: select[of _ seed])

lemma random_scheduler_spec:
  assumes det: "α.deterministic I"
  shows "scheduler_spec final r random_scheduler random_scheduler_invar thr_α thr_invar ws_α ws_invar is_α is_invar I"
proof
  fix σ s
  assume rr: "random_scheduler σ s = None"
    and invar: "random_scheduler_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
  from invar(2) have "thr'_invar (active_threads s)" by(rule active_threads_correct)
  thus "α.active_threads (state_α s) = {}" using rr invar
    by(auto simp add: random_scheduler_def Option_bind_eq_None_conv next_thread_eq_None_iff step_thread_eq_None_conv[OF det] dest: next_thread_eq_SomeD)
next
  fix σ s t σ'
  assume rr: "random_scheduler σ s = ⌊(t, None, σ')⌋"
    and invar: "random_scheduler_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
  thus "∃x ln n. thr_α (thr s) t = ⌊(x, ln)⌋ ∧ 0 < ln $ n ∧ ¬ waiting (ws_α (wset s) t) ∧ may_acquire_all (locks s) t ln"
    by(fastforce simp add: random_scheduler_def bind_eq_Some_conv dest: step_thread_Some_NoneD[OF det])
next
  fix σ s t ta x' m' σ'
  assume rr: "random_scheduler σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
    and invar: "random_scheduler_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
  thus "∃x. thr_α (thr s) t = ⌊(x, no_wait_locks)⌋ ∧ Predicate.eval (r t (x, shr s)) (ta, x', m') ∧ α.actions_ok (state_α s) t ta"
    by(auto simp add: random_scheduler_def bind_eq_Some_conv dest: step_thread_Some_SomeD[OF det])
qed simp_all

end

sublocale random_scheduler_base <
  scheduler_base
    final r convert_RA
    "random_scheduler" "output" "pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))" random_scheduler_invar
    thr_α thr_invar thr_lookup thr_update
    ws_α ws_invar ws_lookup ws_update ws_delete ws_iterate
    is_α is_invar is_memb is_ins is_delete
  for n0 .

sublocale random_scheduler <
  pick_wakeup_spec
    final r convert_RA
    "pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))" random_scheduler_invar
    thr_α thr_invar
    ws_α ws_invar
    is_α is_invar
by(rule pick_wakeup_spec_via_sel)(unfold_locales)

context random_scheduler begin

lemma random_scheduler_scheduler:
  assumes det: "α.deterministic I"
  shows 
  "scheduler
     final r convert_RA
     random_scheduler (pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))) random_scheduler_invar
     thr_α thr_invar thr_lookup thr_update 
     ws_α ws_invar ws_lookup ws_update ws_delete ws_iterate
     is_α is_invar is_memb is_ins is_delete
     I"
proof -
  interpret scheduler_spec
      final r convert_RA
      random_scheduler random_scheduler_invar
      thr_α thr_invar
      ws_α ws_invar
      is_α is_invar
      I
    using det by(rule random_scheduler_spec)

  show ?thesis by(unfold_locales)(rule α.deterministic_invariant3p[OF det])
qed

end

subsection ‹Code generator setup›

lemmas [code] =
  random_scheduler_base.next_thread_def
  random_scheduler_base.random_scheduler_def

end