# Theory Round_Robin

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

section ‹Round robin scheduler›

theory Round_Robin
imports
Scheduler
begin

text ‹
A concrete scheduler must pick one possible reduction step from the small-step semantics for invidivual threads.
Currently, this is only possible if there is only one such by using @{term Predicate.the}.
›

subsection ‹Concrete schedulers›

subsection ‹Round-robin schedulers›

type_synonym 'queue round_robin = "'queue × nat"
― ‹Waiting queue of threads and remaining number of steps of the first thread until it has to return resources›

where

definition enqueue_new_threads :: "'t list ⇒ ('t,'x,'m) new_thread_action list ⇒ 't list"
where

primrec round_robin_update_state :: "nat ⇒ 't list round_robin ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 't list round_robin"
where
"round_robin_update_state n0 (queue, n) t ta =
(let queue' = enqueue_new_threads queue ⦃ta⦄⇘t⇙
in if n = 0 ∨ Yield ∈ set ⦃ta⦄⇘c⇙ then (rotate1 queue', n0) else (queue', n - 1))"

abbreviation round_robin_step :: "nat ⇒ 't list round_robin ⇒ ('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 't list round_robin) option"
where
"round_robin_step n0 σ s t ≡ step_thread (round_robin_update_state n0 σ t) s t"

partial_function (option) round_robin_reschedule :: "'t ⇒
't list ⇒ nat ⇒ ('l,'t,'x,'m,'w) state ⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 't list round_robin) option"
where
"round_robin_reschedule t0 queue n0 s =
(let
t = hd queue;
queue' = tl queue
in
if t = t0 then
None
else
case round_robin_step n0 (t # queue', n0) s t of
None ⇒ round_robin_reschedule t0 (queue' @ [t]) n0 s
| ⌊ttaxmσ⌋ ⇒ ⌊ttaxmσ⌋)"

fun round_robin :: "nat ⇒ 't list round_robin ⇒ ('l,'t,'x,'m,'w) state ⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 't list round_robin) option"
where
"round_robin n0 ([], n) s = None"
| "round_robin n0 (t # queue, n) s =
(case round_robin_step n0 (t # queue, n) s t of
⌊ttaxmσ⌋ ⇒ ⌊ttaxmσ⌋
| None ⇒ round_robin_reschedule t (queue @ [t]) n0 s)"

end

primrec round_robin_invar :: "'t list round_robin ⇒ 't set ⇒ bool"
where "round_robin_invar (queue, n) T ⟷ set queue = T ∧ distinct queue"

"set (enqueue_new_thread queue nta) = set queue ∪ {t. ∃x m. nta = NewThread t x m}"
by(cases nta) auto

"set (enqueue_new_threads queue ntas) = set queue ∪ {t. ∃x m. NewThread t x m ∈ set ntas}"
apply(induct ntas arbitrary: queue)
done

"enqueue_new_thread queue nta = [] ⟷ queue = [] ∧ (∃t b. nta = ThreadExists t b)"
by(cases nta) simp_all

"enqueue_new_threads queue ntas = [] ⟷ queue = [] ∧ set ntas ⊆ {ThreadExists t b|t b. True}"
apply(induct ntas arbitrary: queue)
done

and ntas :: "('t,'x,'m) new_thread_action list"
assumes "thread_oks ts ntas" "set queue = dom ts" "distinct queue"
using assms
proof(induct ntas arbitrary: ts queue)
next
case (Cons nt ntas)
from ‹thread_oks ts (nt # ntas)›
have "thread_ok ts nt" and "thread_oks (redT_updT ts nt) ntas" by simp_all
from ‹thread_ok ts nt› ‹set queue = dom ts› ‹distinct queue›
have "set (enqueue_new_thread queue nt) = dom (redT_updT ts nt) ∧ distinct (enqueue_new_thread queue nt)"
by(cases nt)(auto)
with ‹thread_oks (redT_updT ts nt) ntas›
by(blast intro: Cons.hyps)
qed

lemma round_robin_reschedule_induct [consumes 1, case_names head rotate]:
assumes major: "t0 ∈ set queue"
and head: "⋀queue. P (t0 # queue)"
and rotate: "⋀queue t. ⟦ t ≠ t0; t0 ∈ set queue; P (queue @ [t]) ⟧ ⟹ P (t # queue)"
shows "P queue"
using major
proof(induct n≡"length (takeWhile (λx. x≠t0) queue)" arbitrary: queue)
case 0
then obtain queue' where "queue = t0 # queue'"
by(cases queue)(auto split: if_split_asm)
next
case (Suc n)
then obtain t queue' where [simp]: "queue = t # queue'"
and t: "t ≠ t0" and n: "n = length (takeWhile (λx. x ≠ t0) queue')"
and t0: "t0 ∈ set queue'"
by(cases queue)(auto split: if_split_asm)
from n t0 have "n = length (takeWhile (λx. x ≠ t0) (queue' @ [t]))" by(simp)
moreover from t0 have "t0 ∈ set (queue' @ [t])" by simp
ultimately have "P (queue' @ [t])" by(rule Suc.hyps)
with t t0 show ?case by(simp add: rotate)
qed

declare actions_ok_iff [simp del]
declare actions_ok.cases [rule del]

lemma round_robin_step_invar_None:
"⟦ round_robin_step n0 σ s t' = ⌊(t, None, σ')⌋; round_robin_invar σ (dom (thr s)) ⟧
⟹ round_robin_invar σ' (dom (thr s))"

lemma round_robin_step_invar_Some:
"⟦ deterministic I; round_robin_step n0 σ s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋; round_robin_invar σ (dom (thr s)); s ∈ I ⟧
⟹ round_robin_invar σ' (dom (thr s) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})"
apply(cases σ)
apply clarsimp
done

lemma round_robin_reschedule_Cons:
"round_robin_reschedule t0 (t0 # queue) n0 s = None"
"t ≠ t0 ⟹ round_robin_reschedule t0 (t # queue) n0 s =
(case round_robin_step n0 (t # queue, n0) s t of
None ⇒ round_robin_reschedule t0 (queue @ [t]) n0 s
| Some ttaxmσ ⇒ Some ttaxmσ)"

lemma round_robin_reschedule_NoneD:
assumes rrr: "round_robin_reschedule t0 queue n0 s = None"
and t0: "t0 ∈ set queue"
shows "set (takeWhile (λt'. t' ≠ t0) queue) ∩ active_threads s = {}"
using t0 rrr
proof(induct queue rule: round_robin_reschedule_induct)
thus ?case by simp
next
case (rotate queue t)
from ‹round_robin_reschedule t0 (t # queue) n0 s = None› ‹t ≠ t0›
have "round_robin_step n0 (t # queue, n0) s t = None"
and "round_robin_reschedule t0 (queue @ [t]) n0 s = None"
moreover from ‹round_robin_reschedule t0 (queue @ [t]) n0 s = None›
have "set (takeWhile (λt'. t' ≠ t0) (queue @ [t])) ∩ active_threads s = {}"
by(rule rotate.hyps)
moreover have "takeWhile (λt'. t' ≠ t0) (queue @ [t]) = takeWhile (λt'. t' ≠ t0) queue"
using ‹t0 ∈ set queue› by simp
ultimately show ?case using ‹t ≠ t0› by simp
qed

lemma round_robin_reschedule_Some_NoneD:
assumes rrr: "round_robin_reschedule t0 queue n0 s = ⌊(t, None, σ')⌋"
and t0: "t0 ∈ set queue"
shows "∃x ln n. thr s t = ⌊(x, ln)⌋ ∧ ln \$ n > 0 ∧ ¬ waiting (wset s t) ∧ may_acquire_all (locks s) t ln"
using t0 rrr
proof(induct queue rule: round_robin_reschedule_induct)
next
case (rotate queue t')
show ?case
proof(cases "round_robin_step n0 (t' # queue, n0) s t'")
case None
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, None, σ')⌋› ‹t' ≠ t0›
have "round_robin_reschedule t0 (queue @ [t']) n0 s = ⌊(t, None, σ')⌋"
thus ?thesis by(rule rotate.hyps)
next
case (Some a)
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, None, σ')⌋› ‹t' ≠ t0›
have "round_robin_step n0 (t' # queue, n0) s t' = ⌊(t, None, σ')⌋"
qed
qed

lemma round_robin_reschedule_Some_SomeD:
assumes "deterministic I"
and rrr: "round_robin_reschedule t0 queue n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and t0: "t0 ∈ set queue"
and I: "s ∈ I"
shows "∃x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s t ta"
using t0 rrr
proof(induct queue rule: round_robin_reschedule_induct)
next
case (rotate queue t')
show ?case
proof(cases "round_robin_step n0 (t' # queue, n0) s t'")
case None
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋› ‹t' ≠ t0›
have "round_robin_reschedule t0 (queue @ [t']) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
thus ?thesis by(rule rotate.hyps)
next
case (Some a)
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋› ‹t' ≠ t0›
have "round_robin_step n0 (t' # queue, n0) s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
thus ?thesis using I by(blast dest: step_thread_Some_SomeD[OF ‹deterministic I›])
qed
qed

lemma round_robin_reschedule_invar_None:
assumes rrr: "round_robin_reschedule t0 queue n0 s = ⌊(t, None, σ')⌋"
and invar: "round_robin_invar (queue, n0) (dom (thr s))"
and t0: "t0 ∈ set queue"
shows "round_robin_invar σ' (dom (thr s))"
using t0 rrr invar
proof(induct queue rule: round_robin_reschedule_induct)
next
case (rotate queue t')
show ?case
proof(cases "round_robin_step n0 (t' # queue, n0) s t'")
case None
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, None, σ')⌋› ‹t' ≠ t0›
have "round_robin_reschedule t0 (queue @ [t']) n0 s = ⌊(t, None, σ')⌋"
moreover from ‹round_robin_invar (t' # queue, n0) (dom (thr s))›
have "round_robin_invar (queue @ [t'], n0) (dom (thr s))" by simp
ultimately show ?thesis by(rule rotate.hyps)
next
case (Some a)
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, None, σ')⌋› ‹t' ≠ t0›
have "round_robin_step n0 (t' # queue, n0) s t' = ⌊(t, None, σ')⌋"
thus ?thesis using ‹round_robin_invar (t' # queue, n0) (dom (thr s))›
by(rule round_robin_step_invar_None)
qed
qed

lemma round_robin_reschedule_invar_Some:
assumes "deterministic I"
and rrr: "round_robin_reschedule t0 queue n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and invar: "round_robin_invar (queue, n0) (dom (thr s))"
and t0: "t0 ∈ set queue"
and "s ∈ I"
shows "round_robin_invar σ' (dom (thr s) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})"
using t0 rrr invar
proof(induct queue rule: round_robin_reschedule_induct)
next
case (rotate queue t')
show ?case
proof(cases "round_robin_step n0 (t' # queue, n0) s t'")
case None
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋› ‹t' ≠ t0›
have "round_robin_reschedule t0 (queue @ [t']) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
moreover from ‹round_robin_invar (t' # queue, n0) (dom (thr s))›
have "round_robin_invar (queue @ [t'], n0) (dom (thr s))" by simp
ultimately show ?thesis by(rule rotate.hyps)
next
case (Some a)
with ‹round_robin_reschedule t0 (t' # queue) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋› ‹t' ≠ t0›
have "round_robin_step n0 (t' # queue, n0) s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
thus ?thesis using ‹round_robin_invar (t' # queue, n0) (dom (thr s))› ‹s ∈ I›
by(rule round_robin_step_invar_Some[OF ‹deterministic I›])
qed
qed

lemma round_robin_NoneD:
assumes rr: "round_robin n0 σ s = None"
and invar: "round_robin_invar σ (dom (thr s))"
proof -
obtain queue n where σ: "σ = (queue, n)" by(cases σ)
show ?thesis
proof(cases queue)
case Nil
thus ?thesis using invar σ by(fastforce elim: active_threads.cases)
next
case (Cons t queue')
with rr σ have "round_robin_step n0 (t # queue', n) s t = None"
and "round_robin_reschedule t (queue' @ [t]) n0 s = None" by simp_all
from ‹round_robin_step n0 (t # queue', n) s t = None›
moreover from ‹round_robin_reschedule t (queue' @ [t]) n0 s = None›
have "set (takeWhile (λx. x ≠ t) (queue' @ [t])) ∩ active_threads s = {}"
by(rule round_robin_reschedule_NoneD) simp
moreover from invar σ Cons
have "takeWhile (λx. x ≠ t) (queue' @ [t]) = queue'"
by(subst takeWhile_append2) auto
moreover from invar have "active_threads s ⊆ set queue"
ultimately show ?thesis using Cons by auto
qed
qed

lemma round_robin_Some_NoneD:
assumes rr: "round_robin n0 σ s = ⌊(t, None, σ')⌋"
shows "∃x ln n. thr s t = ⌊(x, ln)⌋ ∧ ln \$ n > 0 ∧ ¬ waiting (wset s t) ∧ may_acquire_all (locks s) t ln"
proof -
obtain queue n where σ: "σ = (queue, n)" by(cases σ)
with rr have "queue ≠ []" by clarsimp
then obtain t' queue' where queue: "queue = t' # queue'"
show ?thesis
proof(cases "round_robin_step n0 (t' # queue', n) s t'")
case (Some a)
with rr queue σ have "round_robin_step n0 (t' # queue', n) s t' = ⌊(t, None, σ')⌋" by simp
next
case None
with rr queue σ have "round_robin_reschedule t' (queue' @ [t']) n0 s = ⌊(t, None, σ')⌋" by simp
thus ?thesis by(rule round_robin_reschedule_Some_NoneD)simp
qed
qed

lemma round_robin_Some_SomeD:
assumes "deterministic I"
and rr: "round_robin n0 σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and "s ∈ I"
shows "∃x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s t ta"
proof -
obtain queue n where σ: "σ = (queue, n)" by(cases σ)
with rr have "queue ≠ []" by clarsimp
then obtain t' queue' where queue: "queue = t' # queue'"
show ?thesis
proof(cases "round_robin_step n0 (t' # queue', n) s t'")
case (Some a)
with rr queue σ have "round_robin_step n0 (t' # queue', n) s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋" by simp
thus ?thesis using ‹s ∈ I› by(blast dest: step_thread_Some_SomeD[OF ‹deterministic I›])
next
case None
with rr queue σ have "round_robin_reschedule t' (queue' @ [t']) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋" by simp
thus ?thesis by(rule round_robin_reschedule_Some_SomeD[OF ‹deterministic I›])(simp_all add: ‹s ∈ I›)
qed
qed

lemma round_robin_invar_None:
assumes rr: "round_robin n0 σ s = ⌊(t, None, σ')⌋"
and invar: "round_robin_invar σ (dom (thr s))"
shows "round_robin_invar σ' (dom (thr s))"
proof -
obtain queue n where σ: "σ = (queue, n)" by(cases σ)
with rr have "queue ≠ []" by clarsimp
then obtain t' queue' where queue: "queue = t' # queue'"
show ?thesis
proof(cases "round_robin_step n0 (t' # queue', n) s t'")
case (Some a)
with rr queue σ have "round_robin_step n0 (t' # queue', n) s t' = ⌊(t, None, σ')⌋" by simp
thus ?thesis using invar unfolding σ queue by(rule round_robin_step_invar_None)
next
case None
with rr queue σ have "round_robin_reschedule t' (queue' @ [t']) n0 s = ⌊(t, None, σ')⌋" by simp
moreover from invar queue σ have "round_robin_invar (queue' @ [t'], n0) (dom (thr s))" by simp
ultimately show ?thesis by(rule round_robin_reschedule_invar_None) simp
qed
qed

lemma round_robin_invar_Some:
assumes "deterministic I"
and rr: "round_robin n0 σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and invar: "round_robin_invar σ (dom (thr s))" "s ∈ I"
shows "round_robin_invar σ' (dom (thr s) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})"
proof -
obtain queue n where σ: "σ = (queue, n)" by(cases σ)
with rr have "queue ≠ []" by clarsimp
then obtain t' queue' where queue: "queue = t' # queue'"
show ?thesis
proof(cases "round_robin_step n0 (t' # queue', n) s t'")
case (Some a)
with rr queue σ have "round_robin_step n0 (t' # queue', n) s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋" by simp
thus ?thesis using invar unfolding σ queue by(rule round_robin_step_invar_Some[OF ‹deterministic I›])
next
case None
with rr queue σ have "round_robin_reschedule t' (queue' @ [t']) n0 s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋" by simp
moreover from invar queue σ
have "round_robin_invar (queue' @ [t'], n0) (dom (thr s))" by simp
ultimately show ?thesis by(rule round_robin_reschedule_invar_Some[OF ‹deterministic I›])(simp_all add: ‹s ∈ I›)
qed
qed

end

locale round_robin_base =
scheduler_base_aux
final r convert_RA
thr_α thr_invar thr_lookup thr_update
ws_α ws_invar ws_lookup
is_α is_invar is_memb is_ins is_delete
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" :: "'queue round_robin ⇒ '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 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"
+
fixes queue_α :: "'queue ⇒ 't list"
and queue_invar :: "'queue ⇒ bool"
and queue_empty :: "unit ⇒ 'queue"
and queue_isEmpty :: "'queue ⇒ bool"
and queue_enqueue :: "'t ⇒ 'queue ⇒ 'queue"
and queue_dequeue :: "'queue ⇒ 't × 'queue"
and queue_push :: "'t ⇒ 'queue ⇒ 'queue"
begin

definition queue_rotate1 :: "'queue ⇒ 'queue"
where "queue_rotate1 = case_prod queue_enqueue ∘ queue_dequeue"

where

where

primrec round_robin_update_state :: "nat ⇒ 'queue round_robin ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'queue round_robin"
where
"round_robin_update_state n0 (queue, n) t ta =
(let queue' = enqueue_new_threads queue ⦃ta⦄⇘t⇙
in if n = 0 ∨ Yield ∈ set ⦃ta⦄⇘c⇙ then (queue_rotate1 queue', n0) else (queue', n - 1))"

abbreviation round_robin_step ::
"nat ⇒ 'queue round_robin ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 't
⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 'queue round_robin) option"
where
"round_robin_step n0 σ s t ≡ step_thread (round_robin_update_state n0 σ t) s t"

partial_function (option) round_robin_reschedule ::
"'t ⇒ 'queue ⇒ nat ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine
⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 'queue round_robin) option"
where
"round_robin_reschedule t0 queue n0 s =
(let
(t, queue') = queue_dequeue queue
in
if t = t0 then
None
else
case round_robin_step n0 (queue_push t queue', n0) s t of
None ⇒ round_robin_reschedule t0 (queue_enqueue t queue') n0 s
| ⌊ttaxmσ⌋ ⇒ ⌊ttaxmσ⌋)"

primrec round_robin :: "nat ⇒ ('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'queue round_robin) scheduler"
where
"round_robin n0 (queue, n) s =
(if queue_isEmpty queue then None
else
let
(t, queue') = queue_dequeue queue
in
(case round_robin_step n0 (queue_push t queue', n) s t of
⌊ttaxmσ⌋ ⇒ ⌊ttaxmσ⌋
| None ⇒ round_robin_reschedule t (queue_enqueue t queue') n0 s))"

primrec round_robin_invar :: "'queue round_robin ⇒ 't set ⇒ bool"
where "round_robin_invar (queue, n) T ⟷ queue_invar queue ∧ Round_Robin.round_robin_invar (queue_α queue, n) T"

definition round_robin_α :: "'queue round_robin ⇒ 't list round_robin"
where "round_robin_α = apfst queue_α"

definition round_robin_start :: "nat ⇒ 't ⇒ 'queue round_robin"
where "round_robin_start n0 t = (queue_enqueue t (queue_empty ()), n0)"

lemma round_robin_invar_correct:
"round_robin_invar σ T ⟹ Round_Robin.round_robin_invar (round_robin_α σ) T"

end

locale round_robin =
round_robin_base
final r convert_RA "output"
thr_α thr_invar thr_lookup thr_update
ws_α ws_invar ws_lookup ws_update ws_delete ws_iterate ws_sel
is_α is_invar is_memb is_ins is_delete
queue_α queue_invar queue_empty queue_isEmpty queue_enqueue queue_dequeue queue_push
+
scheduler_aux
final r convert_RA
thr_α thr_invar thr_lookup thr_update
ws_α ws_invar ws_lookup
is_α is_invar is_memb is_ins is_delete
+
ws: map_update ws_α ws_invar ws_update +
ws: map_delete ws_α ws_invar ws_delete +
ws: map_iteratei ws_α ws_invar ws_iterate +
ws: map_sel' ws_α ws_invar ws_sel +
queue: list queue_α queue_invar +
queue: list_empty queue_α queue_invar queue_empty +
queue: list_isEmpty queue_α queue_invar queue_isEmpty +
queue: list_enqueue queue_α queue_invar queue_enqueue +
queue: list_dequeue queue_α queue_invar queue_dequeue +
queue: list_push queue_α queue_invar queue_push
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" :: "'queue round_robin ⇒ '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 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 queue_α :: "'queue ⇒ 't list"
and queue_invar :: "'queue ⇒ bool"
and queue_empty :: "unit ⇒ 'queue"
and queue_isEmpty :: "'queue ⇒ bool"
and queue_enqueue :: "'t ⇒ 'queue ⇒ 'queue"
and queue_dequeue :: "'queue ⇒ 't × 'queue"
and queue_push :: "'t ⇒ 'queue ⇒ 'queue"
begin

lemma queue_rotate1_correct:
assumes "queue_invar queue" "queue_α queue ≠ []"
shows "queue_α (queue_rotate1 queue) = rotate1 (queue_α queue)"
and "queue_invar (queue_rotate1 queue)"
using assms
apply(auto simp add: queue_rotate1_def split_beta queue.dequeue_correct queue.enqueue_correct)
by(cases "queue_α queue") simp_all

assumes "queue_invar queue"
using assms

assumes "queue_invar queue"
using assms
apply(induct ntas arbitrary: queue)
done

assumes "round_robin_invar σ T" "t' ∈ T"
shows "round_robin_α (round_robin_update_state n0 σ t ta) = Round_Robin.round_robin_update_state n0 (round_robin_α σ) t ta"
using assms
apply(cases σ)
apply(subst (1 2) queue_rotate1_correct)
done

lemma round_robin_step_correct:
assumes det: "α.deterministic I"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
shows
"map_option (apsnd (apsnd round_robin_α)) (round_robin_step n0 σ s t) =
α.round_robin_step n0 (round_robin_α σ) (state_α s) t" (is ?thesis1)
and "case_option True (λ(t, taxm, σ). round_robin_invar σ (case taxm of None ⇒ dom (thr_α (thr s)) | Some (ta, x', m') ⇒ dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})) (round_robin_step n0 σ s t)"
(is ?thesis2)
proof -
have "?thesis1 ∧ ?thesis2"
proof(cases "dom (thr_α (thr s)) = {}")
case True
thus ?thesis using invar
apply(cases σ)
done
next
case False
then obtain t' where t': "t' ∈ dom (thr_α (thr s))" by blast
hence ?thesis1
using step_thread_correct(1)[of I round_robin_invar σ s round_robin_α "round_robin_update_state n0 σ t" t, OF det invar]
unfolding o_def using invar
moreover
{ fix ta :: "('l, 't, 'x, 'm, 'w, 'o) thread_action"
moreover from t' invar have "queue_α (fst σ) ≠ []" by(cases σ) auto
ultimately have "round_robin_invar (round_robin_update_state n0 σ t ta) (dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})"
from step_thread_correct(2)[OF det, of round_robin_invar σ s "round_robin_update_state n0 σ t" t, OF invar this]
have ?thesis2 using t' invar by simp
ultimately show ?thesis by blast
qed
thus ?thesis1 ?thesis2 by blast+
qed

lemma round_robin_reschedule_correct:
assumes det: "α.deterministic I"
and invar: "round_robin_invar (queue, n) (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
and t0: "t0 ∈ set (queue_α queue)"
shows "map_option (apsnd (apsnd round_robin_α)) (round_robin_reschedule t0 queue n0 s) =
α.round_robin_reschedule t0 (queue_α queue) n0 (state_α s)"
and "case_option True (λ(t, taxm, σ). round_robin_invar σ (case taxm of None ⇒ dom (thr_α (thr s)) | Some (ta, x', m') ⇒ dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})) (round_robin_reschedule t0 queue n0 s)"
using t0 invar
proof(induct "queue_α queue" arbitrary: queue n rule: round_robin_reschedule_induct)
{ case 1 thus ?case using head[symmetric]
by(subst round_robin_reschedule.simps)(subst α.round_robin_reschedule.simps, clarsimp simp add: split_beta queue.dequeue_correct)
next
case 2 thus ?case using head[symmetric]
by(subst round_robin_reschedule.simps)(clarsimp simp add: split_beta queue.dequeue_correct) }
next
case (rotate αqueue' t)
obtain t' queue' where queue': "queue_dequeue queue = (t', queue')" by(cases "queue_dequeue queue")
note [simp] = ‹t # αqueue' = queue_α queue›[symmetric]
{ case 1
with queue' have [simp]: "t' = t" "αqueue' = queue_α queue'" "queue_invar queue'" by(auto elim: queue.removelE)
from 1 queue' have invar': "round_robin_invar (queue_push t queue', n0) (dom (thr_α (thr s)))"
show ?case
proof(cases "round_robin_step n0 (queue_push t queue', n0) s t")
case Some thus ?thesis
using queue' ‹t ≠ t0› round_robin_step_correct[OF det invar' ‹state_invar s›, of n0 t] invar' ‹state_α s ∈ I›
by(subst round_robin_reschedule.simps)(subst α.round_robin_reschedule.simps, auto simp add: round_robin_α_def queue.push_correct)
next
case None
hence αNone: "α.round_robin_step n0 (queue_α (queue_push t queue'), n0) (state_α s) t = None"
using round_robin_step_correct[OF det invar' ‹state_invar s›, of n0 t] invar' ‹state_α s ∈ I›
have "αqueue' @ [t] = queue_α (queue_enqueue t queue')" by(simp add: queue.enqueue_correct)
moreover from invar'
have "round_robin_invar (queue_enqueue t queue', n0) (dom (thr_α (thr s)))"
ultimately
have "map_option (apsnd (apsnd round_robin_α)) (round_robin_reschedule t0 (queue_enqueue t queue') n0 s) =
α.round_robin_reschedule t0 (queue_α (queue_enqueue t queue')) n0 (state_α s)"
using ‹state_invar s› ‹state_α s ∈ I› by(rule rotate.hyps)
thus ?thesis using None αNone ‹t ≠ t0› invar' queue'
by(subst round_robin_reschedule.simps)(subst α.round_robin_reschedule.simps, auto simp add: queue.enqueue_correct queue.push_correct)
qed
next
case 2
with queue' have [simp]: "t' = t" "αqueue' = queue_α queue'" "queue_invar queue'" by(auto elim: queue.removelE)
from 2 queue' have invar': "round_robin_invar (queue_push t queue', n0) (dom (thr_α (thr s)))"
show ?case
proof(cases "round_robin_step n0 (queue_push t queue', n0) s t")
case Some thus ?thesis
using queue' ‹t ≠ t0› round_robin_step_correct[OF det invar' ‹state_invar s›, of n0 t] invar' ‹state_α s ∈ I›
by(subst round_robin_reschedule.simps)(auto simp add: round_robin_α_def queue.push_correct)
next
case None
have "αqueue' @ [t] = queue_α (queue_enqueue t queue')" by(simp add: queue.enqueue_correct)
moreover from invar'
have "round_robin_invar (queue_enqueue t queue', n0) (dom (thr_α (thr s)))"
ultimately
have "case_option True (λ(t, taxm, σ). round_robin_invar σ (case_option (dom (thr_α (thr s))) (λ(ta, x', m'). dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙}) taxm)) (round_robin_reschedule t0 (queue_enqueue t queue') n0 s)"
using ‹state_invar s› ‹state_α s ∈ I› by(rule rotate.hyps)
thus ?thesis using None ‹t ≠ t0› invar' queue'
by(subst round_robin_reschedule.simps)(auto simp add: queue.enqueue_correct queue.push_correct)
qed
}
qed

lemma round_robin_correct:
assumes det: "α.deterministic I"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
shows "map_option (apsnd (apsnd round_robin_α)) (round_robin n0 σ s) =
α.round_robin n0 (round_robin_α σ) (state_α s)"
(is ?thesis1)
and "case_option True (λ(t, taxm, σ). round_robin_invar σ (case taxm of None ⇒ dom (thr_α (thr s)) | Some (ta, x', m') ⇒ dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})) (round_robin n0 σ s)"
(is ?thesis2)
proof -
obtain queue n where σ: "σ = (queue, n)" by(cases σ)
have "?thesis1 ∧ ?thesis2"
proof(cases "queue_α queue")
case Nil thus ?thesis using invar σ
by(auto simp add: split_beta queue.isEmpty_correct round_robin_α_def)
next
case (Cons t αqueue')
with invar σ obtain queue'
where [simp]: "queue_dequeue queue = (t, queue')" "αqueue' = queue_α queue'" "queue_invar queue'"
by(auto elim: queue.removelE)
from invar σ Cons have invar': "round_robin_invar (queue_push t queue', n) (dom (thr_α (thr s)))"
from invar σ Cons have invar'': "round_robin_invar (queue_enqueue t queue', n0) (dom (thr_α (thr s)))"
show ?thesis
proof(cases "round_robin_step n0 (queue_push t queue', n) s t")
case Some
with σ Cons invar show ?thesis
using round_robin_step_correct[OF det invar' ‹state_invar s›, of n0 t]
by(auto simp add: queue.isEmpty_correct queue.push_correct round_robin_α_def)
next
case None
from invar σ Cons have "t ∈ set (queue_α (queue_enqueue t queue'))"
from round_robin_reschedule_correct[OF det invar'' ‹state_invar s›, OF ‹state_α s ∈ I› this, of n0] None σ Cons invar
round_robin_step_correct[OF det invar' ‹state_invar s›, of n0 t]
show ?thesis by(auto simp add: queue.isEmpty_correct queue.push_correct round_robin_α_def queue.enqueue_correct)
qed
qed
thus ?thesis1 ?thesis2 by simp_all
qed

lemma round_robin_scheduler_spec:
assumes det: "α.deterministic I"
shows "scheduler_spec final r (round_robin n0) round_robin_invar thr_α thr_invar ws_α ws_invar is_α is_invar I"
proof
fix σ s
assume rr: "round_robin n0 σ s = None"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
from round_robin_correct[OF det, OF invar, of n0] rr
have "α.round_robin n0 (round_robin_α σ) (state_α s) = None" by simp
moreover from invar have "Round_Robin.round_robin_invar (round_robin_α σ) (dom (thr (state_α s)))"
ultimately show "α.active_threads (state_α s) = {}" by(rule α.round_robin_NoneD)
next
fix σ s t σ'
assume rr: "round_robin n0 σ s = ⌊(t, None, σ')⌋"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
from round_robin_correct[OF det, OF invar, of n0] rr
have rr': "α.round_robin n0 (round_robin_α σ) (state_α s) = ⌊(t, None, round_robin_α σ')⌋" by simp
then show "∃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(rule α.round_robin_Some_NoneD[where s="state_α s", unfolded state_α_conv])
next
fix σ s t ta x' m' σ'
assume rr: "round_robin n0 σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
from round_robin_correct[OF det, OF invar, of n0] rr
have rr': "α.round_robin n0 (round_robin_α σ) (state_α s) = ⌊(t, ⌊(ta, x', m')⌋, round_robin_α σ')⌋" by simp
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"
using ‹state_α s ∈ I› by(rule α.round_robin_Some_SomeD[OF det, where s="state_α s", unfolded state_α_conv])
next
fix σ s t σ'
assume rr: "round_robin n0 σ s = ⌊(t, None, σ')⌋"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
from round_robin_correct[OF det, OF invar, of n0] rr
show "round_robin_invar σ' (dom (thr_α (thr s)))" by simp
next
fix σ s t ta x' m' σ'
assume rr: "round_robin n0 σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and invar: "round_robin_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
from round_robin_correct[OF det, OF invar, of n0] rr
show "round_robin_invar σ' (dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})" by simp
qed

lemma round_robin_start_invar:
"round_robin_invar (round_robin_start n0 t0) {t0}"

end

sublocale round_robin_base <
scheduler_base
final r convert_RA
"round_robin n0" "output" "pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))" round_robin_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 round_robin <
pick_wakeup_spec
final r convert_RA
"pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))" round_robin_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
by(rule pick_wakeup_spec_via_sel)(unfold_locales)

context round_robin begin

lemma round_robin_scheduler:
assumes det: "α.deterministic I"
shows
"scheduler
final r convert_RA
(round_robin n0) (pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))) round_robin_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
"round_robin n0" round_robin_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
I
using det by(rule round_robin_scheduler_spec)

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

end

lemmas [code] =
round_robin_base.queue_rotate1_def