# 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
(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 {
})"

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

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)]

assumes "next_thread seed active = Some (t, seed')"
and "thr'_invar active" "random_scheduler_invar seed T"
shows "t ∈ thr'_α active"
using assms

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"
thus "α.active_threads (state_α s) = {}" using rr invar
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"
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"
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] =