# Theory Scheduler

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

section ‹Abstract scheduler›

theory Scheduler
imports
State_Refinement
"../Framework/FWProgressAux"
"../Framework/FWLTS"
(*"../../Collections/spec/SetSpec"
"../../Collections/spec/MapSpec"
"../../Collections/spec/ListSpec"*)
"../Basic/JT_ICF"

begin

text ‹
Define an unfold operation that puts everything into one function to avoid duplicate evaluation.
›

definition unfold_tllist' :: "('a ⇒ 'b × 'a + 'c) ⇒ 'a ⇒ ('b, 'c) tllist"
where [code del]:
"unfold_tllist' f =
unfold_tllist (λa. ∃c. f a = Inr c) (projr ∘ f) (fst ∘ projl ∘ f) (snd ∘ projl ∘ f)"

lemma unfold_tllist' [code]:
"unfold_tllist' f a =
(case f a of Inr c ⇒ TNil c | Inl (b, a') ⇒ TCons b (unfold_tllist' f a'))"
by(rule tllist.expand)(auto simp add: unfold_tllist'_def split: sum.split_asm)

type_synonym
('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'s) scheduler =
"'s ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 's) option"

locale scheduler_spec_base =
state_refine_base
final r convert_RA
thr_α thr_invar
ws_α ws_invar
is_α is_invar
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 schedule :: "('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'s) scheduler"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
and thr_invar :: "'m_t ⇒ bool"
and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
and ws_invar :: "'m_w ⇒ bool"
and is_α :: "'s_i ⇒ 't interrupts"
and is_invar :: "'s_i ⇒ bool"

locale scheduler_spec =
scheduler_spec_base
final r convert_RA
schedule σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
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 schedule :: "('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'s) scheduler"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
and thr_invar :: "'m_t ⇒ bool"
and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
and ws_invar :: "'m_w ⇒ bool"
and is_α :: "'s_i ⇒ 't interrupts"
and is_invar :: "'s_i ⇒ bool"
+
fixes invariant :: "('l,'t,'x,'m,'w) state set"
assumes schedule_NoneD:
"⟦ schedule σ s = None; state_invar s; σ_invar σ (dom (thr_α (thr s))); state_α s ∈ invariant ⟧
⟹ α.active_threads (state_α s) = {}"
and schedule_Some_NoneD:
"⟦ schedule σ s = ⌊(t, None, σ')⌋; state_invar s; σ_invar σ (dom (thr_α (thr s))); state_α s ∈ invariant ⟧
⟹ ∃x ln n. thr_α (thr s) t = ⌊(x, ln)⌋ ∧ ln \$ n > 0 ∧ ¬ waiting (ws_α (wset s) t) ∧ may_acquire_all (locks s) t ln"
and schedule_Some_SomeD:
"⟦ schedule σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋; state_invar s; σ_invar σ (dom (thr_α (thr s))); state_α s ∈ invariant ⟧
⟹ ∃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"
and schedule_invar_None:
"⟦ schedule σ s = ⌊(t, None, σ')⌋; state_invar s; σ_invar σ (dom (thr_α (thr s))); state_α s ∈ invariant ⟧
⟹ σ_invar σ' (dom (thr_α (thr s)))"
and schedule_invar_Some:
"⟦ schedule σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋; state_invar s; σ_invar σ (dom (thr_α (thr s))); state_α s ∈ invariant ⟧
⟹ σ_invar σ' (dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})"

locale pick_wakeup_spec_base =
state_refine_base
final r convert_RA
thr_α thr_invar
ws_α ws_invar
is_α is_invar
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 pick_wakeup :: "'s ⇒ 't ⇒ 'w ⇒ 'm_w ⇒ 't option"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
and thr_invar :: "'m_t ⇒ bool"
and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
and ws_invar :: "'m_w ⇒ bool"
and is_α :: "'s_i ⇒ 't interrupts"
and is_invar :: "'s_i ⇒ bool"

locale pick_wakeup_spec =
pick_wakeup_spec_base
final r convert_RA
pick_wakeup σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
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 pick_wakeup :: "'s ⇒ 't ⇒ 'w ⇒ 'm_w ⇒ 't option"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
and thr_α :: "'m_t ⇒ ('l,'t,'x) thread_info"
and thr_invar :: "'m_t ⇒ bool"
and ws_α :: "'m_w ⇒ ('w,'t) wait_sets"
and ws_invar :: "'m_w ⇒ bool"
and is_α :: "'s_i ⇒ 't interrupts"
and is_invar :: "'s_i ⇒ bool"
+
assumes pick_wakeup_NoneD:
"⟦ pick_wakeup σ t w ws = None; ws_invar ws; σ_invar σ T; dom (ws_α ws) ⊆ T; t ∈ T ⟧
⟹ InWS w ∉ ran (ws_α ws)"
and pick_wakeup_SomeD:
"⟦ pick_wakeup σ t w ws = ⌊t'⌋; ws_invar ws; σ_invar σ T; dom (ws_α ws) ⊆ T; t ∈ T ⟧
⟹ ws_α ws t' = ⌊InWS w⌋"

locale scheduler_base_aux =
state_refine_base
final r convert_RA
thr_α thr_invar
ws_α ws_invar
is_α is_invar
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 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 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"
begin

definition free_thread_id :: "'m_t ⇒ 't ⇒ bool"
where "free_thread_id ts t ⟷ thr_lookup t ts = None"

fun redT_updT :: "'m_t ⇒ ('t,'x,'m) new_thread_action ⇒ 'm_t"
where
"redT_updT ts (NewThread t' x m) = thr_update t' (x, no_wait_locks) ts"
| "redT_updT ts _ = ts"

definition redT_updTs :: "'m_t ⇒ ('t,'x,'m) new_thread_action list ⇒ 'm_t"
where "redT_updTs = foldl redT_updT"

where

text ‹
This fixes @{typ "'x"} in the @{typ "('t,'x,'m) new_thread_action list"} type, but avoids @{term "undefined"},
which raises an exception during execution in the generated code.
›

where

definition wset_actions_ok :: "'m_w ⇒ 't ⇒ ('t,'w) wait_set_action list ⇒ bool"
where
"wset_actions_ok ws t was ⟷
ws_lookup t ws =
(if Notified ∈ set was then ⌊PostWS WSNotified⌋
else if WokenUp ∈ set was then ⌊PostWS WSWokenUp⌋
else None)"

primrec cond_action_ok :: "('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 't ⇒ 't conditional_action ⇒ bool"
where
"⋀ln. cond_action_ok s t (Join T) =
(case thr_lookup T (thr s)
of None ⇒ True
| ⌊(x, ln)⌋ ⇒ t ≠ T ∧ final x ∧ ln = no_wait_locks ∧ ws_lookup T (wset s) = None)"
| "cond_action_ok s t Yield = True"

definition cond_action_oks :: "('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 't ⇒ 't conditional_action list ⇒ bool"
where
"cond_action_oks s t cts = list_all (cond_action_ok s t) cts"

primrec redT_updI :: "'s_i ⇒ 't interrupt_action ⇒ 's_i"
where
"redT_updI is (Interrupt t) = is_ins t is"
| "redT_updI is (ClearInterrupt t) = is_delete t is"
| "redT_updI is (IsInterrupted t b) = is"

primrec redT_updIs :: "'s_i ⇒ 't interrupt_action list ⇒ 's_i"
where
"redT_updIs is [] = is"
| "redT_updIs is (ia # ias) = redT_updIs (redT_updI is ia) ias"

primrec interrupt_action_ok :: "'s_i ⇒ 't interrupt_action ⇒ bool"
where
"interrupt_action_ok is (Interrupt t) = True"
| "interrupt_action_ok is (ClearInterrupt t) = True"
| "interrupt_action_ok is (IsInterrupted t b) = (b = (is_memb t is))"

primrec interrupt_actions_ok :: "'s_i ⇒ 't interrupt_action list ⇒ bool"
where
"interrupt_actions_ok is [] = True"
| "interrupt_actions_ok is (ia # ias) ⟷ interrupt_action_ok is ia ∧ interrupt_actions_ok (redT_updI is ia) ias"

definition actions_ok :: "('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o') thread_action ⇒ bool"
where
"actions_ok s t ta ⟷
lock_ok_las (locks s) t ⦃ta⦄⇘l⇙ ∧
cond_action_oks s t ⦃ta⦄⇘c⇙ ∧
wset_actions_ok (wset s) t ⦃ta⦄⇘w⇙ ∧
interrupt_actions_ok (interrupts s) ⦃ta⦄⇘i⇙"

end

locale scheduler_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
+
scheduler_spec_base
final r convert_RA
schedule σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
+
pick_wakeup_spec_base
final r convert_RA
pick_wakeup σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
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 schedule :: "('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'s) scheduler"
and "output" :: "'s ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"
and pick_wakeup :: "'s ⇒ 't ⇒ 'w ⇒ 'm_w ⇒ 't option"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
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 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"
begin

primrec exec_updW :: "'s ⇒ 't ⇒ 'm_w ⇒ ('t,'w) wait_set_action ⇒ 'm_w"
where
"exec_updW σ t ws (Notify w) =
(case pick_wakeup σ t w ws
of None  ⇒ ws
| Some t ⇒ ws_update t (PostWS WSNotified) ws)"
| "exec_updW σ t ws (NotifyAll w) =
ws_iterate ws (λ_. True) (λ(t, w') ws'. if w' = InWS w then ws_update t (PostWS WSNotified) ws' else ws')
ws"
| "exec_updW σ t ws (Suspend w) = ws_update t (InWS w) ws"
| "exec_updW σ t ws (WakeUp t') =
(case ws_lookup t' ws of ⌊InWS w⌋ ⇒ ws_update t' (PostWS WSWokenUp) ws | _ ⇒ ws)"
| "exec_updW σ t ws Notified = ws_delete t ws"
| "exec_updW σ t ws WokenUp = ws_delete t ws"

definition exec_updWs :: "'s ⇒ 't ⇒ 'm_w ⇒ ('t,'w) wait_set_action list ⇒ 'm_w"
where "exec_updWs σ t = foldl (exec_updW σ t)"

definition exec_upd ::
"'s ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'x ⇒ 'm
⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine"
where [simp]:
"exec_upd σ s t ta x' m' =
(redT_updLs (locks s) t ⦃ta⦄⇘l⇙,
(thr_update t (x', redT_updLns (locks s) t (snd (the (thr_lookup t (thr s)))) ⦃ta⦄⇘l⇙) (redT_updTs (thr s) ⦃ta⦄⇘t⇙), m'),
exec_updWs σ t (wset s) ⦃ta⦄⇘w⇙, redT_updIs (interrupts s) ⦃ta⦄⇘i⇙)"

definition execT ::
"'s ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine
⇒ ('s × 't × ('l,'t,'x,'m,'w,'o) thread_action × ('l,'t,'m,'m_t,'m_w,'s_i) state_refine) option"
where
"execT σ s =
(do {
(t, tax'm', σ') ← schedule σ s;
case tax'm' of
None ⇒
(let (x, ln) = the (thr_lookup t (thr s));
ta = (K\$ [], [], [], [], [], convert_RA ln);
s' = (acquire_all (locks s) t ln, (thr_update t (x, no_wait_locks) (thr s), shr s), wset s, interrupts s)
in ⌊(σ', t, ta, s')⌋)
| ⌊(ta, x', m')⌋ ⇒ ⌊(σ', t, ta, exec_upd σ s t ta x' m')⌋
})"

primrec exec_step ::
"'s × ('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒
('s × 't × ('l,'t,'x,'m,'w,'o) thread_action) × 's × ('l,'t,'m,'m_t,'m_w,'s_i) state_refine + ('l,'t,'m,'m_t,'m_w,'s_i) state_refine"
where
"exec_step (σ, s) =
(case execT σ s of
None ⇒ Inr s
| Some (σ', t, ta, s') ⇒ Inl ((σ, t, ta), σ', s'))"

declare exec_step.simps [simp del]

definition exec_aux ::
"'s × ('l,'t,'m,'m_t,'m_w,'s_i) state_refine
⇒ ('s × 't × ('l,'t,'x,'m,'w,'o) thread_action, ('l,'t,'m,'m_t,'m_w,'s_i) state_refine) tllist"
where
"exec_aux σs = unfold_tllist' exec_step σs"

definition exec :: "'s ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ ('q, ('l,'t,'m,'m_t,'m_w,'s_i) state_refine) tllist"
where
"exec σ s = tmap the id (tfilter undefined (λq. q ≠ None) (tmap (λ(σ, t, ta). output σ t ta) id (exec_aux (σ, s))))"

end

text ‹
Implement ‹pick_wakeup› by ‹map_sel'›
›

definition pick_wakeup_via_sel ::
"('m_w ⇒ ('t ⇒ 'w wait_set_status ⇒ bool) ⇀ 't × 'w wait_set_status)
⇒ 's ⇒ 't ⇒ 'w ⇒ 'm_w ⇒ 't option"
where "pick_wakeup_via_sel ws_sel σ t w ws = map_option fst (ws_sel ws (λt w'. w' = InWS w))"

lemma pick_wakeup_spec_via_sel:
assumes sel: "map_sel' ws_α ws_invar ws_sel"
shows "pick_wakeup_spec (pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))) σ_invar ws_α ws_invar"
proof -
interpret ws: map_sel' ws_α ws_invar ws_sel by(rule sel)
show ?thesis
by(unfold_locales)(auto simp add: pick_wakeup_via_sel_def ran_def dest: ws.sel'_noneD ws.sel'_SomeD)
qed

locale scheduler_ext_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 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_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 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"
begin

abbreviation pick_wakeup :: "'s ⇒ 't ⇒ 'w ⇒ 'm_w ⇒ 't option"
where "pick_wakeup ≡ pick_wakeup_via_sel (λs P. ws_sel s (λ(k,v). P k v))"

fun active_threads :: "('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 's_t"
where
"active_threads (ls, (ts, m), ws, is) =
thr_iterate ts (λ_. True)
(λ(t, (x, ln)) ts'. if ln = no_wait_locks
then if Predicate.holds
(do {
(ta, _) ← r t (x, m);
Predicate.if_pred (actions_ok (ls, (ts, m), ws, is) t ta)
})
then thr'_ins_dj t ts'
else ts'
else if ¬ waiting (ws_lookup t ws) ∧ may_acquire_all ls t ln then thr'_ins_dj t ts' else ts')
(thr'_empty ())"

end

locale scheduler_aux =
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
+
thr: finite_map thr_α thr_invar +
thr: map_lookup thr_α thr_invar thr_lookup +
thr: map_update thr_α thr_invar thr_update +
ws: map ws_α ws_invar +
ws: map_lookup ws_α ws_invar ws_lookup +
"is": set is_α is_invar +
"is": set_memb is_α is_invar is_memb +
"is": set_ins is_α is_invar is_ins +
"is": set_delete is_α is_invar 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 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 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"
begin

lemma redT_updT_correct [simp]:
assumes "thr_invar ts"
shows "thr_α (redT_updT ts nta) = FWThread.redT_updT (thr_α ts) nta"
and "thr_invar (redT_updT ts nta)"
by(case_tac [!] nta)(simp_all add: thr.update_correct assms)

lemma redT_updTs_correct [simp]:
assumes  "thr_invar ts"
shows "thr_α (redT_updTs ts ntas) = FWThread.redT_updTs (thr_α ts) ntas"
and "thr_invar (redT_updTs ts ntas)"
using assms
by(induct ntas arbitrary: ts)(simp_all add: redT_updTs_def)

by(cases nta) simp_all

by(induct ntas arbitrary: ts) simp_all

lemma wset_actions_ok_correct [simp]:
"ws_invar ws ⟹ wset_actions_ok ws t was ⟷ FWWait.wset_actions_ok (ws_α ws) t was"

lemma cond_action_ok_correct [simp]:
"state_invar s ⟹ cond_action_ok s t cta ⟷ α.cond_action_ok (state_α s) t cta"
by(cases s,cases cta)(auto simp add: thr.lookup_correct ws.lookup_correct)

lemma cond_action_oks_correct [simp]:
assumes "state_invar s"
shows "cond_action_oks s t ctas ⟷ α.cond_action_oks (state_α s) t ctas"

lemma redT_updI_correct [simp]:
assumes "is_invar is"
shows "is_α (redT_updI is ia) = FWInterrupt.redT_updI (is_α is) ia"
and "is_invar (redT_updI is ia)"
using assms
by(case_tac [!] ia)(auto simp add: is.ins_correct is.delete_correct)

lemma redT_updIs_correct [simp]:
assumes "is_invar is"
shows "is_α (redT_updIs is ias) = FWInterrupt.redT_updIs (is_α is) ias"
and "is_invar (redT_updIs is ias)"
using assms
by(induct ias arbitrary: "is")(auto)

lemma interrupt_action_ok_correct [simp]:
"is_invar is ⟹ interrupt_action_ok is ia ⟷ FWInterrupt.interrupt_action_ok (is_α is) ia"

lemma interrupt_actions_ok_correct [simp]:
"is_invar is ⟹ interrupt_actions_ok is ias ⟷ FWInterrupt.interrupt_actions_ok (is_α is) ias"
by(induct ias arbitrary:"is") simp_all

lemma actions_ok_correct [simp]:
"state_invar s ⟹ actions_ok s t ta ⟷ α.actions_ok (state_α s) t ta"

end

locale scheduler =
scheduler_base
final r convert_RA
schedule "output" pick_wakeup σ_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
+
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
+
scheduler_spec
final r convert_RA
schedule σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
invariant
+
pick_wakeup_spec
final r convert_RA
pick_wakeup σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
+
ws: map_update ws_α ws_invar ws_update +
ws: map_delete ws_α ws_invar ws_delete +
ws: map_iteratei ws_α ws_invar ws_iterate
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 schedule :: "('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'s) scheduler"
and "output" :: "'s ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"
and pick_wakeup :: "'s ⇒ 't ⇒ 'w ⇒ 'm_w ⇒ 't option"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
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 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 invariant :: "('l,'t,'x,'m,'w) state set"
+
assumes invariant: "invariant3p α.redT invariant"
begin

lemma exec_updW_correct:
assumes invar: "ws_invar ws" "σ_invar σ T" "dom (ws_α ws) ⊆ T" "t ∈ T"
shows "redT_updW t (ws_α ws) wa (ws_α (exec_updW σ t ws wa))" (is "?thesis1")
and "ws_invar (exec_updW σ t ws wa)" (is "?thesis2")
proof -
from invar have "?thesis1 ∧ ?thesis2"
proof(cases wa)
case [simp]: (Notify w)
show ?thesis
proof(cases "pick_wakeup σ t w ws")
case (Some t')
hence "ws_α ws t' = ⌊InWS w⌋" using invar by(rule pick_wakeup_SomeD)
with Some show ?thesis using invar by(auto simp add: ws.update_correct)
next
case None
hence "InWS w ∉ ran (ws_α ws)" using invar by(rule pick_wakeup_NoneD)
with None show ?thesis using invar by(auto simp add: ran_def)
qed
next
case [simp]: (NotifyAll w)
let ?f = "λ(t, w') ws'. if w' = InWS w then ws_update t (PostWS WSNotified) ws' else ws'"
let ?I = "λT ws'. (∀k. if k∉T ∧ ws_α ws k = ⌊InWS w⌋ then ws_α ws' k = ⌊PostWS WSNotified⌋ else ws_α ws' k = ws_α ws k) ∧ ws_invar ws'"
from invar have "?I (dom (ws_α ws)) ws" by(auto simp add: ws.lookup_correct)
with ‹ws_invar ws› have "?I {} (ws_iterate ws (λ_. True) ?f ws)"
proof(rule ws.iterate_rule_P[where I="?I"])
fix t w' T ws'
assume t: "t ∈ T" and w': "ws_α ws t = ⌊w'⌋"
and T: "T ⊆ dom (ws_α ws)" and I: "?I T ws'"
{ fix t'
assume "t' ∉ T - {t}" "ws_α ws t' = ⌊InWS w⌋"
with t I w' invar have "ws_α (?f (t, w') ws') t' = ⌊PostWS WSNotified⌋"
moreover {
fix t'
assume "t' ∈ T - {t} ∨ ws_α ws t' ≠ ⌊InWS w⌋"
with t I w' invar have "ws_α (?f (t,w') ws') t' = ws_α ws t'"
moreover
have "ws_invar (?f (t, w') ws')" using I by(simp add: ws.update_correct)
ultimately show "?I (T - {t}) (?f (t, w') ws')" by safe simp
qed
hence "ws_α (ws_iterate ws (λ_. True) ?f ws) = (λt. if ws_α ws t = ⌊InWS w⌋ then ⌊PostWS WSNotified⌋ else ws_α ws t)"
and "ws_invar (ws_iterate ws (λ_. True) ?f ws)" by(simp_all add: fun_eq_iff)
thus ?thesis by simp
next
case WakeUp thus ?thesis using assms
by(auto simp add: ws.lookup_correct ws.update_correct split: wait_set_status.split)
thus ?thesis1 ?thesis2 by simp_all
qed

lemma exec_updWs_correct:
assumes "ws_invar ws" "σ_invar σ T" "dom (ws_α ws) ⊆ T" "t ∈ T"
shows "redT_updWs t (ws_α ws) was (ws_α (exec_updWs σ t ws was))" (is "?thesis1")
and "ws_invar (exec_updWs σ t ws was)" (is "?thesis2")
proof -
from ‹ws_invar ws› ‹dom (ws_α ws) ⊆ T›
have "?thesis1 ∧ ?thesis2"
proof(induct was arbitrary: ws)
case Nil thus ?case by(auto simp add: exec_updWs_def redT_updWs_def)
next
case (Cons wa was)
let ?ws' = "exec_updW σ t ws wa"
from ‹ws_invar ws› ‹σ_invar σ T› ‹dom (ws_α ws) ⊆ T› ‹t ∈ T›
have invar': "ws_invar ?ws'" and red: "redT_updW t (ws_α ws) wa (ws_α ?ws')"
by(rule exec_updW_correct)+
have "dom (ws_α ?ws') ⊆ T"
proof
fix t' assume "t' ∈ dom (ws_α ?ws')"
with red have "t' ∈ dom (ws_α ws) ∨ t = t'"
by(auto dest!: redT_updW_Some_otherD split: wait_set_status.split_asm)
with ‹dom (ws_α ws) ⊆ T› ‹t ∈ T› show "t' ∈ T" by auto
qed
with invar' have "redT_updWs t (ws_α ?ws') was (ws_α (exec_updWs σ t ?ws' was)) ∧ ws_invar (exec_updWs σ t ?ws' was)"
by(rule Cons.hyps)
thus ?case using red
by(auto simp add: exec_updWs_def redT_updWs_def intro: rtrancl3p_step_converse)
qed
thus ?thesis1 ?thesis2 by simp_all
qed

lemma exec_upd_correct:
assumes "state_invar s" "σ_invar σ (dom (thr_α (thr s)))" "t ∈ (dom (thr_α (thr s)))"
and "wset_thread_ok (ws_α (wset s)) (thr_α (thr s))"
shows "redT_upd (state_α s) t ta x' m' (state_α (exec_upd σ s t ta x' m'))"
and "state_invar (exec_upd σ s t ta x' m')"
by(auto simp add: thr.update_correct thr.lookup_correct intro: exec_updWs_correct)

lemma execT_None:
assumes invar: "state_invar s" "σ_invar σ (dom (thr_α (thr s)))" "state_α s ∈ invariant"
and exec: "execT σ s = None"
shows "α.active_threads (state_α s) = {}"
using assms
by(cases "schedule σ s")(fastforce simp add: execT_def thr.lookup_correct dest: schedule_Some_NoneD schedule_NoneD)+

lemma execT_Some:
assumes invar: "state_invar s" "σ_invar σ (dom (thr_α (thr s)))" "state_α s ∈ invariant"
and wstok: "wset_thread_ok (ws_α (wset s)) (thr_α (thr s))"
and exec: "execT σ s = ⌊(σ', t, ta, s')⌋"
shows "α.redT (state_α s) (t, ta) (state_α s')" (is "?thesis1")
and "state_invar s'" (is "?thesis2")
and "σ_invar σ' (dom (thr_α (thr s')))" (is "?thesis3")
proof -
note [simp del] = redT_upd_simps exec_upd_def

have "?thesis1 ∧ ?thesis2 ∧ ?thesis3"
proof(cases "fst (snd (the (schedule σ s)))")
case None
with exec invar have schedule: "schedule σ s = ⌊(t, None, σ')⌋"
and ta: "ta = (K\$ [], [], [], [], [], convert_RA (snd (the (thr_α (thr s) t))))"
and s': "s' = (acquire_all (locks s) t (snd (the (thr_α (thr s) t))), (thr_update t (fst (the (thr_α (thr s) t)), no_wait_locks) (thr s), shr s), wset s, interrupts s)"
by(auto simp add: execT_def bind_eq_Some_conv thr.lookup_correct split_beta split del: option.split_asm)
from schedule_Some_NoneD[OF schedule invar]

obtain x ln n where t: "thr_α (thr s) t = ⌊(x, ln)⌋"
and "0 < ln \$ n" "¬ waiting (ws_α (wset s) t)" "may_acquire_all (locks s) t ln" by blast
hence ?thesis1 using ta s' invar by(auto intro: α.redT.redT_acquire simp add: thr.update_correct)
moreover from invar s' have "?thesis2" by(simp add: thr.update_correct)
moreover from t s' invar have "dom (thr_α (thr s')) = dom (thr_α (thr s))" by(auto simp add: thr.update_correct)
hence "?thesis3" using invar schedule by(auto intro: schedule_invar_None)
ultimately show ?thesis by simp
next
case (Some taxm)
with exec invar obtain x' m'
where schedule: "schedule σ s = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and s': "s' = exec_upd σ s t ta x' m'"
by(cases taxm)(fastforce simp add: execT_def bind_eq_Some_conv split del: option.split_asm)
from schedule_Some_SomeD[OF schedule invar]
obtain x where t: "thr_α (thr s) t = ⌊(x, no_wait_locks)⌋"
and "Predicate.eval (r t (x, shr s)) (ta, x', m')"
and aok: "α.actions_ok (state_α s) t ta" by blast
with s' have ?thesis1 using invar wstok
by(fastforce intro: α.redT.intros exec_upd_correct)
moreover from invar s' t wstok have ?thesis2 by(auto intro: exec_upd_correct)
moreover {
from schedule invar
have "σ_invar σ' (dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})"
by(rule schedule_invar_Some)
also have "dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙} = dom (thr_α (thr s'))"
using invar s' aok t
by(auto simp add: exec_upd_def thr.lookup_correct thr.update_correct simp del: split_paired_Ex)(fastforce dest: redT_updTs_new_thread intro: redT_updTs_Some1 redT_updTs_new_thread_ts simp del: split_paired_Ex)+
finally have "σ_invar σ' (dom (thr_α (thr s')))" . }
ultimately show ?thesis by simp
qed
thus ?thesis1 ?thesis2 ?thesis3 by simp_all
qed

lemma exec_step_into_redT:
assumes invar: "state_invar s" "σ_invar σ (dom (thr_α (thr s)))" "state_α s ∈ invariant"
and wstok: "wset_thread_ok (ws_α (wset s)) (thr_α (thr s))"
and exec: "exec_step (σ, s) = Inl ((σ'', t, ta), σ', s')"
shows "α.redT (state_α s) (t, ta) (state_α s')" "σ'' = σ"
and "state_invar s'" "σ_invar σ' (dom (thr_α (thr s')))" "state_α s' ∈ invariant"
proof -
from exec have execT: "execT σ s = ⌊(σ', t, ta, s')⌋"
and q: "σ'' = σ" by(auto simp add: exec_step.simps split_beta)
from invar wstok execT show red: "α.redT (state_α s) (t, ta) (state_α s')"
and invar': "state_invar s'" "σ_invar σ' (dom (thr_α (thr s')))" "σ'' = σ"
by(rule execT_Some)+(rule q)
from invariant red ‹state_α s ∈ invariant›
show "state_α s' ∈ invariant" by(rule invariant3pD)
qed

lemma exec_step_InrD:
assumes "state_invar s" "σ_invar σ (dom (thr_α (thr s)))" "state_α s ∈ invariant"
and "exec_step (σ, s) = Inr s'"
shows "α.active_threads (state_α s) = {}"
and "s' = s"
using assms
by(auto simp add: exec_step_def dest: execT_None)

assumes "s -t▹ta→ s'"
using assms

lemma exec_aux_into_Runs:
assumes "state_invar s" "σ_invar σ (dom (thr_α (thr s)))" "state_α s ∈ invariant"
and "wset_thread_ok (ws_α (wset s)) (thr_α (thr s))"
shows "α.mthr.Runs (state_α s) (lmap snd (llist_of_tllist (exec_aux (σ, s))))" (is ?thesis1)
and "tfinite (exec_aux (σ, s)) ⟹ state_invar (terminal (exec_aux (σ, s)))" (is "_ ⟹ ?thesis2")
proof -
from assms show ?thesis1
proof(coinduction arbitrary: σ s)
case (Runs σ s)
note invar = ‹state_invar s› ‹σ_invar σ (dom (thr_α (thr s)))› ‹state_α s ∈ invariant›
and wstok = ‹wset_thread_ok (ws_α (wset s)) (thr_α (thr s))›
show ?case
proof(cases "exec_aux (σ, s)")
case (TNil s')
hence "α.active_threads (state_α s) = {}" "s' = s"
by(auto simp add: exec_aux_def unfold_tllist' split: sum.split_asm dest: exec_step_InrD[OF invar])
hence ?Stuck using TNil by(auto dest: α.red_in_active_threads)
thus ?thesis ..
next
case (TCons σtta ttls')
then obtain t ta σ' s' σ''
where [simp]: "σtta = (σ'', t, ta)"
and [simp]: "ttls' = exec_aux (σ', s')"
and step: "exec_step (σ, s) = Inl ((σ'', t, ta), σ', s')"
unfolding exec_aux_def by(subst (asm) (2) unfold_tllist')(fastforce split: sum.split_asm)
from invar wstok step
have redT: "α.redT (state_α s) (t, ta) (state_α s')"
and [simp]: "σ'' = σ"
and invar': "state_invar s'" "σ_invar σ' (dom (thr_α (thr s')))" "state_α s' ∈ invariant"
by(rule exec_step_into_redT)+
have "wset_thread_ok (ws_α (wset s')) (thr_α (thr s'))" by simp
with invar' redT TCons have ?Step by(auto simp del: split_paired_Ex)
thus ?thesis ..
qed
qed
next
assume "tfinite (exec_aux (σ, s))"
thus "?thesis2" using assms
proof(induct "exec_aux (σ, s)" arbitrary: σ s rule: tfinite_induct)
case TNil thus ?case
by(auto simp add: exec_aux_def unfold_tllist' split_beta split: sum.split_asm dest: exec_step_InrD)
next
case (TCons σtta ttls)
from ‹TCons σtta ttls = exec_aux (σ, s)›
obtain σ'' t ta σ' s'
where [simp]: "σtta = (σ'', t, ta)"
and ttls: "ttls = exec_aux (σ', s')"
and step: "exec_step (σ, s) = Inl ((σ'', t, ta), σ', s')"
unfolding exec_aux_def by(subst (asm) (2) unfold_tllist')(fastforce split: sum.split_asm)
note ttls moreover
from ‹state_invar s› ‹σ_invar σ (dom (thr_α (thr s)))› ‹state_α s ∈ invariant› ‹wset_thread_ok (ws_α (wset s)) (thr_α (thr s))› step
have [simp]: "σ'' = σ"
and invar': "state_invar s'" "σ_invar σ' (dom (thr_α (thr s')))" "state_α s' ∈ invariant"
and redT: "α.redT (state_α s) (t, ta) (state_α s')"
by(rule exec_step_into_redT)+
note invar' moreover
have "wset_thread_ok (ws_α (wset s')) (thr_α (thr s'))" by simp
ultimately have "state_invar (terminal (exec_aux (σ', s')))" by(rule TCons)
with ‹TCons σtta ttls = exec_aux (σ, s)›[symmetric]
show ?case unfolding ttls by simp
qed
qed

end

locale scheduler_ext_aux =
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
+
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
+
thr: map_iteratei thr_α thr_invar thr_iterate +
ws: map_update ws_α ws_invar ws_update +
ws: map_sel' ws_α ws_invar ws_sel +
thr': finite_set thr'_α thr'_invar +
thr': set_empty thr'_α thr'_invar thr'_empty +
thr': set_ins_dj thr'_α thr'_invar 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 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_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"
begin

assumes "state_invar s"
and "thr'_invar (active_threads s)" (is "?thesis2")
proof -
obtain ls ts m ws "is" where s: "s = (ls, (ts, m), ws, is)" by(cases s) fastforce
let ?f = "λ(t, (x, ln)) TS. if ln = no_wait_locks
then if Predicate.holds (do { (ta, _) ← r t (x, m); Predicate.if_pred (actions_ok (ls, (ts, m), ws, is) t ta) })
then thr'_ins_dj t TS else TS
else if ¬ waiting (ws_lookup t ws) ∧ may_acquire_all ls t ln then thr'_ins_dj t TS else TS"
let ?I = "λT TS. thr'_invar TS ∧ thr'_α TS ⊆ dom (thr_α ts) - T ∧ (∀t. t ∉ T ⟶ t ∈ thr'_α TS ⟷ t ∈ α.active_threads (state_α s))"

from assms s have "thr_invar ts" by simp
moreover have "?I (dom (thr_α ts)) (thr'_empty ())"
ultimately have "?I {} (thr_iterate ts (λ_. True) ?f (thr'_empty ()))"
proof(rule thr.iterate_rule_P[where I="?I"])
fix t xln T TS
assume tT: "t ∈ T"
and tst: "thr_α ts t = ⌊xln⌋"
and Tdom: "T ⊆ dom (thr_α ts)"
and I: "?I T TS"
obtain x ln where xln: "xln = (x, ln)" by(cases xln)
from tT I have t: "t ∉ thr'_α TS" by blast

from I have invar: "thr'_invar TS" ..
hence "thr'_invar (?f (t, xln) TS)" using t
unfolding xln by(auto simp add: thr'.ins_dj_correct)
moreover from I have "thr'_α TS ⊆ dom (thr_α ts) - T" by blast
hence "thr'_α (?f (t, xln) TS) ⊆ dom (thr_α ts) - (T - {t})"
using invar tst t by(auto simp add: xln thr'.ins_dj_correct)
moreover
{
fix t'
assume t': "t' ∉ T - {t}"
have "t' ∈ thr'_α (?f (t, xln) TS) ⟷ t' ∈ α.active_threads (state_α s)" (is "?lhs ⟷ ?rhs")
proof(cases "t' = t")
case True
show ?thesis
proof
assume ?lhs
with True xln invar tst ‹state_invar s› t show ?rhs
by(fastforce simp add: holds_eq thr'.ins_dj_correct s split_beta ws.lookup_correct split: if_split_asm elim!: bindE if_predE intro: α.active_threads.intros)
next
assume ?rhs
with True xln invar tst ‹state_invar s› t show ?lhs
by(fastforce elim!: α.active_threads.cases simp add: holds_eq s thr'.ins_dj_correct ws.lookup_correct elim!: bindE if_predE intro: bindI if_predI)
qed
next
case False
with t' have "t' ∉ T" by simp
with I have "t' ∈ thr'_α TS ⟷ t' ∈ α.active_threads (state_α s)" by blast
thus ?thesis using xln False invar t by(auto simp add: thr'.ins_dj_correct)
qed
}
ultimately show "?I (T - {t}) (?f (t, xln) TS)" by blast
qed
thus "?thesis1" "?thesis2" by(auto simp add: s)
qed

end

locale scheduler_ext =
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
+
scheduler_spec
final r convert_RA
schedule σ_invar
thr_α thr_invar
ws_α ws_invar
is_α is_invar
invariant
+
ws: map_delete ws_α ws_invar ws_delete +
ws: map_iteratei ws_α ws_invar ws_iterate
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 schedule :: "('l,'t,'x,'m,'w,'o,'m_t,'m_w,'s_i,'s) scheduler"
and "output" :: "'s ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"
and σ_invar :: "'s ⇒ 't set ⇒ bool"
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_empty :: "unit ⇒ 'm_w"
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 invariant :: "('l,'t,'x,'m,'w) state set"
+
assumes invariant: "invariant3p α.redT invariant"

sublocale scheduler_ext <
pick_wakeup_spec
final r convert_RA
pick_wakeup σ_invar
thr_α thr_invar
ws_α ws_invar
by(rule pick_wakeup_spec_via_sel)(unfold_locales)

sublocale scheduler_ext <
scheduler
final r convert_RA
schedule "output" "pick_wakeup" σ_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
invariant
by(unfold_locales)(rule invariant)

subsection ‹Schedulers for deterministic small-step semantics›

text ‹
The default code equations for @{term Predicate.the} impose the type class constraint ‹eq›
on the predicate elements. For the semantics, which contains the heap, there might be no such
instance, so we use new constants for which other code equations can be used.
These do not add the type class constraint, but may fail more often with non-uniqueness exception.
›

definition singleton2 where [simp]: "singleton2 = Predicate.singleton"
definition the_only2 where [simp]: "the_only2 = Predicate.the_only"
definition the2 where [simp]: "the2 = Predicate.the"

"(('l,'t,'x,'m,'w,'o) thread_action ⇒ 's) ⇒ ('l,'t,'x,'m,'w) state ⇒ 't
⇒ ('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 's) option"
where
"⋀ln. step_thread update_state s t =
(case thr s t of
⌊(x, ln)⌋ ⇒
if ln = no_wait_locks then
if ∃ta x' m'. t ⊢ (x, shr s) -ta→ (x', m') ∧ actions_ok s t ta then
let
(ta, x', m') = THE (ta, x', m'). t ⊢ (x, shr s) -ta→ (x', m') ∧ actions_ok s t ta
in
⌊(t, ⌊(ta, x', m')⌋, update_state ta)⌋
else
None
else if may_acquire_all (locks s) t ln ∧ ¬ waiting (wset s t) then
⌊(t, None, update_state (K\$ [], [], [], [], [], convert_RA ln))⌋
else
None
| None ⇒ None)"

"step_thread update_state s t = ⌊(t', taxmσ')⌋
⟹ t' = t ∧ t ∈ active_threads s"

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

"step_thread update_state s t' = ⌊(t, None, σ')⌋
⟹ ∃x ln n. thr s t = ⌊(x, ln)⌋ ∧ ln \$ n > 0 ∧ ¬ waiting (wset s t) ∧ may_acquire_all (locks s) t ln ∧ σ' = update_state (K\$ [], [], [], [], [], convert_RA ln)"
by(auto split: if_split_asm simp add: split_beta elim!: neq_no_wait_locksE)

"⟦ deterministic I; step_thread update_state s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋; s ∈ I ⟧
⟹ ∃x. thr s t = ⌊(x, no_wait_locks)⌋ ∧ t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s t ta ∧ σ' = update_state ta"
by(auto simp add: split_beta deterministic_THE split: if_split_asm)

end

context scheduler_base_aux begin

"(('l,'t,'x,'m,'w,'o) thread_action ⇒ 's) ⇒ ('l,'t,'m,'m_t,'m_w,'s_i) state_refine ⇒ 't ⇒
('t × (('l,'t,'x,'m,'w,'o) thread_action × 'x × 'm) option × 's) option"
where
"⋀ln. step_thread update_state s t =
(case thr_lookup t (thr s) of
⌊(x, ln)⌋ ⇒
if ln = no_wait_locks then
let
reds = do {
(ta, x', m') ← r t (x, shr s);
if actions_ok s t ta then Predicate.single (ta, x', m') else bot
}
in
if Predicate.holds (reds ⤜ (λ_. Predicate.single ())) then
let
(ta, x', m') = the2 reds
in
⌊(t, ⌊(ta, x', m')⌋, update_state ta)⌋
else
None
else if may_acquire_all (locks s) t ln ∧ ¬ waiting (ws_lookup t (wset s)) then
⌊(t, None, update_state (K\$ [], [], [], [], [],convert_RA ln))⌋
else
None
| None ⇒ None)"

end

context scheduler_aux begin

lemma deterministic_THE2:
assumes "α.deterministic I"
and tst: "thr_α (thr s) t = ⌊(x, no_wait_locks)⌋"
and red: "Predicate.eval (r t (x, shr s)) (ta, x', m')"
and aok: "α.actions_ok (state_α s) t ta"
and I: "state_α s ∈ I"
shows "Predicate.the (r t (x, shr s) ⤜ (λ(ta, x', m'). if α.actions_ok (state_α s) t ta then Predicate.single (ta, x', m') else bot)) = (ta, x', m')"
proof -
show ?thesis unfolding the_def
apply(rule the_equality)
apply(rule bindI[OF red])
apply(erule bindE)
apply(clarsimp split: if_split_asm)
apply(drule (1) α.deterministicD[OF ‹α.deterministic I›, where s="state_α s", simplified, OF red _ tst aok])
apply(rule I)
apply simp
done
qed

assumes det: "α.deterministic I"
and invar: "σ_invar σ (dom (thr_α (thr s)))" "state_invar s" "state_α s ∈ I"
shows
"map_option (apsnd (apsnd σ_α)) (step_thread update_state s t) = α.step_thread (σ_α ∘ update_state) (state_α s) t" (is ?thesis1)
and "(⋀ta. FWThread.thread_oks (thr_α (thr s)) ⦃ta⦄⇘t⇙ ⟹ σ_invar (update_state ta) (dom (thr_α (thr s)) ∪ {t. ∃x m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙})) ⟹ case_option True (λ(t, taxm, σ). σ_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⇙})) (step_thread update_state s t)"
(is "(⋀ta. ?tso ta ⟹ ?inv ta) ⟹ ?thesis2")
proof -
have "?thesis1 ∧ ((∀ta. ?tso ta ⟶ ?inv ta) ⟶ ?thesis2)"
case None
with invar show ?thesis
split_beta holds_eq split: if_split_asm cong del: image_cong_simp)
apply metis
apply metis
done
next
case (Some a)
then obtain t' taxm σ'
where rrs: "step_thread update_state s t = ⌊(t', taxm, σ')⌋" by(cases a) auto
show ?thesis
proof(cases "taxm")
case None
with rrs invar have ?thesis1
moreover {
let ?ta = "(K\$ [], [], [], [], [], convert_RA (snd (the (thr_lookup t (thr s)))))"
assume "?tso ?ta ⟶ ?inv ?ta"
hence ?thesis2 using None rrs
ultimately show ?thesis by blast
next
case (Some a)
with rrs obtain ta x' m'
where rrs: "step_thread update_state s t =  ⌊(t', ⌊(ta, x', m')⌋, σ')⌋"
by(cases a) fastforce
with invar have ?thesis1
split_beta α.deterministic_THE [OF det, where s="state_α s", simplified]
deterministic_THE2[OF det] holds_eq split: if_split_asm
cong del: image_cong_simp) blast+
moreover {
assume "?tso ta ⟶ ?inv ta"
hence ?thesis2 using rrs invar
}
ultimately show ?thesis by blast
qed
qed
thus ?thesis1 "(⋀ta. ?tso ta ⟹ ?inv ta) ⟹ ?thesis2" by blast+
qed

assumes det: "α.deterministic I"
and invar: "state_invar s" "state_α s ∈ I"
shows "step_thread update_state s t = None ⟷ t ∉ α.active_threads (state_α s)"
using assms step_thread_correct(1)[OF det _ invar(1), of "λ_ _. True", of id update_state t]

assumes det: "α.deterministic I"
and step: "step_thread update_state s t' = ⌊(t, None, σ')⌋"
and invar: "state_invar s" "state_α s ∈ I"
shows "∃x ln n. thr_α (thr s) t = ⌊(x, ln)⌋ ∧ ln \$ n > 0 ∧ ¬ waiting (ws_α (wset s) t) ∧ may_acquire_all (locks s) t ln ∧ σ' = update_state (K\$ [], [], [], [], [], convert_RA ln)"
using assms step_thread_correct(1)[OF det _ invar(1), of "λ_ _. True", of id update_state t']

assumes det: "α.deterministic I"
and step: "step_thread update_state s t' = ⌊(t, ⌊(ta, x', m')⌋, σ')⌋"
and invar: "state_invar s" "state_α s ∈ I"
shows "∃x. thr_α (thr s) t = ⌊(x, no_wait_locks)⌋ ∧ Predicate.eval (r t (x, shr s)) (ta, x', m') ∧ actions_ok s t ta ∧ σ' = update_state ta"
using assms step_thread_correct(1)[OF det _ invar(1), of "λ_ _. True", of id update_state t']

end

subsection ‹Code Generator setup›

lemmas [code] =
scheduler_base_aux.redT_updT.simps
scheduler_base_aux.redT_updTs_def
scheduler_base_aux.wset_actions_ok_def
scheduler_base_aux.cond_action_ok.simps
scheduler_base_aux.cond_action_oks_def
scheduler_base_aux.redT_updI.simps
scheduler_base_aux.redT_updIs.simps
scheduler_base_aux.interrupt_action_ok.simps
scheduler_base_aux.interrupt_actions_ok.simps
scheduler_base_aux.actions_ok_def

lemmas [code] =
scheduler_base.exec_updW.simps
scheduler_base.exec_updWs_def
scheduler_base.exec_upd_def
scheduler_base.execT_def
scheduler_base.exec_step.simps
scheduler_base.exec_aux_def
scheduler_base.exec_def

lemmas [code] =

lemma singleton2_code [code]:
"singleton2 dfault (Predicate.Seq f) =
(case f () of
Predicate.Empty ⇒ dfault ()
| Predicate.Insert x P ⇒
if Predicate.is_empty P then x else Code.abort (STR ''singleton2 not unique'') (λ_. singleton2 dfault (Predicate.Seq f))
| Predicate.Join P xq ⇒
if Predicate.is_empty P then
the_only2 dfault xq
else if Predicate.null xq then singleton2 dfault P else Code.abort (STR ''singleton2 not unique'') (λ_. singleton2 dfault (Predicate.Seq f)))"
unfolding singleton2_def the_only2_def
by(auto simp only: singleton_code Code.abort_def split: seq.split if_split)

lemma the_only2_code [code]:
"the_only2 dfault Predicate.Empty = Code.abort (STR ''the_only2 empty'') dfault"
"the_only2 dfault (Predicate.Insert x P) =
(if Predicate.is_empty P then x else Code.abort (STR ''the_only2 not unique'') (λ_. the_only2 dfault (Predicate.Insert x P)))"
"the_only2 dfault (Predicate.Join P xq) =
(if Predicate.is_empty P then
the_only2 dfault xq
else if Predicate.null xq then
singleton2 dfault P
else
Code.abort (STR ''the_only2 not unique'') (λ_. the_only2 dfault (Predicate.Join P xq)))"
unfolding singleton2_def the_only2_def by simp_all

lemma the2_eq [code]:
"the2 A = singleton2 (λx. Code.abort (STR ''not_unique'') (λ_. the2 A)) A"
unfolding the2_def singleton2_def by(rule the_eq)

end
```