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›

primrec enqueue_new_thread :: "'t list ⇒ ('t,'x,'m) new_thread_action ⇒ 't list"
where 
  "enqueue_new_thread queue (NewThread t x m) = queue @ [t]"
| "enqueue_new_thread queue (ThreadExists t b) = queue"

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

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

context multithreaded_base begin

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"

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

lemma set_enqueue_new_threads: 
  "set (enqueue_new_threads queue ntas) = set queue ∪ {t. ∃x m. NewThread t x m ∈ set ntas}"
apply(induct ntas arbitrary: queue)
apply(auto simp add: enqueue_new_threads_def set_enqueue_new_thread)
done

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

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

lemma distinct_enqueue_new_threads:
  fixes ts :: "('l,'t,'x) thread_info"
  and ntas :: "('t,'x,'m) new_thread_action list"
  assumes "thread_oks ts ntas" "set queue = dom ts" "distinct queue"
  shows "distinct (enqueue_new_threads queue ntas)"
using assms
proof(induct ntas arbitrary: ts queue)
  case Nil thus ?case by(simp add: enqueue_new_threads_def)
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›
  have "distinct (enqueue_new_threads (enqueue_new_thread queue nt) ntas)"
    by(blast intro: Cons.hyps)
  thus ?case by(simp add: enqueue_new_threads_def)
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)
  thus ?case by(simp add: head)
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

context multithreaded_base begin

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))"
by(cases σ)(auto dest: step_thread_Some_NoneD simp add: set_enqueue_new_threads distinct_enqueue_new_threads)

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
apply(frule (1) step_thread_Some_SomeD)
apply(auto split: if_split_asm simp add: split_beta set_enqueue_new_threads deterministic_THE)
apply(auto simp add: actions_ok_iff distinct_enqueue_new_threads)
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σ)"
by(simp_all add: round_robin_reschedule.simps)

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)
  case (head queue)
  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"
    by(simp_all add: round_robin_reschedule_Cons)
  from this(1) have "t ∉ active_threads s" by(rule step_thread_NoneD)
  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)
  case head thus ?case by(simp add: round_robin_reschedule_Cons)
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, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    thus ?thesis by(blast dest: step_thread_Some_NoneD)
  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)
  case head thus ?case by(simp add: round_robin_reschedule_Cons)
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')⌋, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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')⌋, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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)
  case head thus ?case by(simp add: round_robin_reschedule_Cons)
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, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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)
  case head thus ?case by(simp add: round_robin_reschedule_Cons)
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')⌋, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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')⌋, σ')⌋"
      by(simp add: round_robin_reschedule_Cons)
    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))"
  shows "active_threads 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›
    have "t ∉ active_threads s" by(rule step_thread_NoneD)
    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"
      using σ by(auto elim: active_threads.cases)
    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'"
    by(auto simp add: neq_Nil_conv)
  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 by(blast dest: step_thread_Some_NoneD)
  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'"
    by(auto simp add: neq_Nil_conv)
  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'"
    by(auto simp add: neq_Nil_conv)
  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'"
    by(auto simp add: neq_Nil_conv)
  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"

primrec enqueue_new_thread :: "'queue ⇒ ('t,'x,'m) new_thread_action ⇒ 'queue"
where 
  "enqueue_new_thread ts (NewThread t x m) = queue_enqueue t ts"
| "enqueue_new_thread ts (ThreadExists t b) = ts"

definition enqueue_new_threads :: "'queue ⇒ ('t,'x,'m) new_thread_action list ⇒ 'queue"
where
  "enqueue_new_threads = foldl enqueue_new_thread"

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"
by(cases σ)(simp add: round_robin_α_def)

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

lemma enqueue_thread_correct:
  assumes "queue_invar queue"
  shows "queue_α (enqueue_new_thread queue nta) = Round_Robin.enqueue_new_thread (queue_α queue) nta"
  and "queue_invar (enqueue_new_thread queue nta)"
using assms
by(case_tac [!] nta)(simp_all add: queue.enqueue_correct)

lemma enqueue_threads_correct:
  assumes "queue_invar queue"
  shows "queue_α (enqueue_new_threads queue ntas) = Round_Robin.enqueue_new_threads (queue_α queue) ntas"
  and "queue_invar (enqueue_new_threads queue ntas)"
using assms
apply(induct ntas arbitrary: queue)
apply(simp_all add: enqueue_new_threads_def Round_Robin.enqueue_new_threads_def enqueue_thread_correct)
done

lemma round_robin_update_thread_correct:
  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(auto simp add: round_robin_α_def queue_rotate1_correct enqueue_threads_correct del: conjI)
apply(subst (1 2) queue_rotate1_correct)
apply(auto simp add: enqueue_threads_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 σ)
      apply(auto dest: step_thread_Some_NoneD[OF det] step_thread_Some_SomeD[OF det])
      apply(fastforce simp add: α.step_thread_eq_None_conv elim: α.active_threads.cases intro: sym)
      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
      by(subst (asm) round_robin_update_thread_correct) auto
    moreover
    { fix ta :: "('l, 't, 'x, 'm, 'w, 'o) thread_action"
      assume "FWThread.thread_oks (thr_α (thr s)) ⦃ta⦄⇘t⇙"
      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⇙})"
        using invar t' by(cases σ)(auto simp add: queue_rotate1_correct enqueue_threads_correct set_enqueue_new_threads iff del: domIff intro: distinct_enqueue_new_threads) }
    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 head
  { 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)))"
      by(auto simp add: queue.push_correct)
    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›
        by(auto simp add: queue.push_correct round_robin_α_def)
      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)))"
        by(auto simp add: queue.enqueue_correct queue.push_correct)
      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)))"
      by(auto simp add: queue.push_correct)
    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)))"
        by(auto simp add: queue.enqueue_correct queue.push_correct)
      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)))"
      by(auto simp add: queue.push_correct)
    from invar σ Cons have invar'': "round_robin_invar (queue_enqueue t queue', n0) (dom (thr_α (thr s)))"
      by(auto simp add: queue.enqueue_correct)
    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'))"
        by(auto simp add: queue.enqueue_correct)      
      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)))"
    by(simp add: round_robin_invar_correct)
  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}"
by(simp add: round_robin_start_def queue.empty_correct queue.enqueue_correct)

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
  round_robin_base.enqueue_new_thread.simps
  round_robin_base.enqueue_new_threads_def
  round_robin_base.round_robin_update_state.simps
  round_robin_base.round_robin_reschedule.simps
  round_robin_base.round_robin.simps
  round_robin_base.round_robin_start_def

end