Theory Scheduler
section ‹Abstract scheduler›
theory Scheduler
imports
State_Refinement
"../Framework/FWProgressAux"
"../Framework/FWLTS"
"../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"
primrec thread_ok :: "'m_t ⇒ ('t,'x,'m) new_thread_action ⇒ bool"
where
"thread_ok ts (NewThread t x m) = free_thread_id ts t"
| "thread_ok ts (ThreadExists t b) = (b ≠ free_thread_id ts t)"
text ‹
We use @{term "redT_updT"} in ‹thread_ok› instead of @{term "redT_updT'"} like in theory @{theory JinjaThreads.FWThread}.
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.
›
primrec thread_oks :: "'m_t ⇒ ('t,'x,'m) new_thread_action list ⇒ bool"
where
"thread_oks ts [] = True"
| "thread_oks ts (ta#tas) = (thread_ok ts ta ∧ thread_oks (redT_updT ts ta) tas)"
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⇙ ∧
thread_oks (thr s) ⦃ta⦄⇘t⇙ ∧
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 free_thread_id_correct [simp]:
"thr_invar ts ⟹ free_thread_id ts = FWThread.free_thread_id (thr_α ts)"
by(auto simp add: free_thread_id_def fun_eq_iff thr.lookup_correct intro: free_thread_id.intros)
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)
lemma thread_ok_correct [simp]:
"thr_invar ts ⟹ thread_ok ts nta ⟷ FWThread.thread_ok (thr_α ts) nta"
by(cases nta) simp_all
lemma thread_oks_correct [simp]:
"thr_invar ts ⟹ thread_oks ts ntas ⟷ FWThread.thread_oks (thr_α ts) ntas"
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"
by(simp add: wset_actions_ok_def FWWait.wset_actions_ok_def ws.lookup_correct)
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"
by(induct ctas)(simp_all add: cond_action_oks_def assms)
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"
by(cases ia)(auto simp add: is.memb_correct)
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"
by(auto simp add: actions_ok_def)
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⌋"
by(auto)(simp_all add: ws.update_correct) }
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'"
by(auto simp add: ws.update_correct) }
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)
qed(simp_all add: ws.update_correct ws.delete_correct map_upd_eq_restrict)
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')"
using assms unfolding wset_thread_ok_conv_dom
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)
lemma (in multithreaded_base) red_in_active_threads:
assumes "s -t▹ta→ s'"
shows "t ∈ active_threads s"
using assms
by cases(auto intro: active_threads.intros)
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)+
from wstok α.redT_preserves_wset_thread_ok[OF 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
from α.redT_preserves_wset_thread_ok[OF redT] ‹wset_thread_ok (ws_α (wset s)) (thr_α (thr s))›
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
lemma active_threads_correct [simp]:
assumes "state_invar s"
shows "thr'_α (active_threads s) = α.active_threads (state_α s)" (is "?thesis1")
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 ())"
by(auto simp add: thr'.empty_correct s elim: α.active_threads.cases)
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"
context multithreaded_base begin
definition step_thread ::
"(('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)"
lemma step_thread_NoneD:
"step_thread update_state s t = None ⟹ t ∉ active_threads s"
unfolding step_thread_def
by(fastforce simp add: split_beta elim!: active_threads.cases split: if_split_asm)
lemma inactive_step_thread_eq_NoneI:
"t ∉ active_threads s ⟹ step_thread update_state s t = None"
unfolding step_thread_def
by(fastforce simp add: split_beta split: if_split_asm intro: active_threads.intros)
lemma step_thread_eq_None_conv:
"step_thread update_state s t = None ⟷ t ∉ active_threads s"
by(blast dest: step_thread_NoneD intro: inactive_step_thread_eq_NoneI)
lemma step_thread_eq_Some_activeD:
"step_thread update_state s t = ⌊(t', taxmσ')⌋
⟹ t' = t ∧ t ∈ active_threads s"
unfolding step_thread_def
by(fastforce split: if_split_asm simp add: split_beta intro: active_threads.intros)
declare actions_ok_iff [simp del]
declare actions_ok.cases [rule del]
lemma step_thread_Some_NoneD:
"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)"
unfolding step_thread_def
by(auto split: if_split_asm simp add: split_beta elim!: neq_no_wait_locksE)
lemma step_thread_Some_SomeD:
"⟦ 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"
unfolding step_thread_def
by(auto simp add: split_beta deterministic_THE split: if_split_asm)
end
context scheduler_base_aux begin
definition step_thread ::
"(('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(simp add: singleI aok)
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
lemma step_thread_correct:
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)"
proof(cases "step_thread update_state s t")
case None
with invar show ?thesis
apply (auto simp add: thr.lookup_correct α.step_thread_def step_thread_def ws.lookup_correct
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
by(auto simp add: thr.lookup_correct ws.lookup_correct α.step_thread_def step_thread_def split_beta split: if_split_asm)
moreover {
let ?ta = "(K$ [], [], [], [], [], convert_RA (snd (the (thr_lookup t (thr s)))))"
assume "?tso ?ta ⟶ ?inv ?ta"
hence ?thesis2 using None rrs
by(auto simp add: thr.lookup_correct ws.lookup_correct α.step_thread_def step_thread_def split_beta split: if_split_asm) }
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
by (auto simp add: thr.lookup_correct ws.lookup_correct α.step_thread_def step_thread_def
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
by(auto simp add: thr.lookup_correct ws.lookup_correct α.step_thread_def step_thread_def split_beta α.deterministic_THE[OF det, where s="state_α s", simplified] deterministic_THE2[OF det] holds_eq split: if_split_asm)(auto simp add: α.actions_ok_iff)
}
ultimately show ?thesis by blast
qed
qed
thus ?thesis1 "(⋀ta. ?tso ta ⟹ ?inv ta) ⟹ ?thesis2" by blast+
qed
lemma step_thread_eq_None_conv:
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]
by(simp add: map_option.id α.step_thread_eq_None_conv)
lemma step_thread_Some_NoneD:
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']
by(fastforce simp add: map_option.id dest: α.step_thread_Some_NoneD[OF sym])
lemma step_thread_Some_SomeD:
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']
by(auto simp add: map_option.id dest: α.step_thread_Some_SomeD[OF det sym])
end
subsection ‹Code Generator setup›
lemmas [code] =
scheduler_base_aux.free_thread_id_def
scheduler_base_aux.redT_updT.simps
scheduler_base_aux.redT_updTs_def
scheduler_base_aux.thread_ok.simps
scheduler_base_aux.thread_oks.simps
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
scheduler_base_aux.step_thread_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] =
scheduler_ext_base.active_threads.simps
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