1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Non-deterministic scheduler functionality.
9*)
10
11chapter "Scheduler"
12
13theory Schedule_A
14imports Arch_A
15begin
16
17context begin interpretation Arch .
18
19requalify_consts
20  arch_switch_to_thread
21  arch_switch_to_idle_thread
22
23end
24
25abbreviation
26  "idle st \<equiv> st = Structures_A.IdleThreadState"
27
28text \<open>Gets the TCB at an address if the thread can be scheduled.\<close>
29definition
30  getActiveTCB :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> tcb option"
31where
32  "getActiveTCB tcb_ref state \<equiv>
33   case (get_tcb tcb_ref state)
34     of None           \<Rightarrow> None
35      | Some tcb       \<Rightarrow> if (runnable $ tcb_state tcb)
36                         then Some tcb else None"
37
38text \<open>Gets all schedulable threads in the system.\<close>
39definition
40  allActiveTCBs :: "(obj_ref set,'z::state_ext) s_monad" where
41  "allActiveTCBs \<equiv> do
42    state \<leftarrow> get;
43    return {x. getActiveTCB x state \<noteq> None}
44   od"
45
46text \<open>Switches the current thread to the specified one.\<close>
47definition
48  switch_to_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
49  "switch_to_thread t \<equiv> do
50     state \<leftarrow> get;
51     assert (get_tcb t state \<noteq> None);
52     arch_switch_to_thread t;
53     do_extended_op (tcb_sched_action (tcb_sched_dequeue) t);
54     modify (\<lambda>s. s \<lparr> cur_thread := t \<rparr>)
55   od"
56
57text \<open>Asserts that a thread is runnable before switching to it.\<close>
58definition guarded_switch_to :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
59"guarded_switch_to thread \<equiv> do ts \<leftarrow> get_thread_state thread;
60                    assert (runnable ts);
61                    switch_to_thread thread
62                 od"
63
64text \<open>Switches to the idle thread.\<close>
65definition
66  switch_to_idle_thread :: "(unit,'z::state_ext) s_monad" where
67  "switch_to_idle_thread \<equiv> do
68     thread \<leftarrow> gets idle_thread;
69     arch_switch_to_idle_thread;
70     modify (\<lambda>s. s \<lparr> cur_thread := thread \<rparr>)
71   od"
72
73class state_ext_sched = state_ext +
74  fixes schedule :: "(unit,'a) s_monad"
75
76definition choose_thread :: "det_ext state \<Rightarrow> (unit \<times> det_ext state) set \<times> bool" where
77"choose_thread \<equiv>
78      do
79        d \<leftarrow> gets cur_domain;
80        queues \<leftarrow> gets (\<lambda>s. ready_queues s d);
81        if (\<forall>prio. queues prio = []) then (switch_to_idle_thread)
82        else (guarded_switch_to (hd (max_non_empty_queue queues)))
83      od"
84
85text \<open>
86  Determine whether given priority is highest among queued ready threads in given domain.
87  Trivially true if no threads are ready.\<close>
88definition
89  is_highest_prio :: "domain \<Rightarrow> priority \<Rightarrow> det_ext state \<Rightarrow> bool"
90where
91  "is_highest_prio d p s \<equiv>
92    (\<forall>prio. ready_queues s d prio = [])
93    \<or> p \<ge> Max {prio. ready_queues s d prio \<noteq> []}"
94
95instantiation  det_ext_ext :: (type) state_ext_sched
96begin
97
98definition
99  "schedule_switch_thread_fastfail ct it ct_prio target_prio \<equiv>
100     if ct \<noteq> it
101     then return (target_prio < ct_prio)
102     else return True"
103
104definition
105  "schedule_choose_new_thread \<equiv> do
106     dom_time \<leftarrow> gets domain_time;
107     when (dom_time = 0) next_domain;
108     choose_thread;
109     set_scheduler_action resume_cur_thread
110   od"
111
112definition
113  "schedule_det_ext_ext \<equiv> do
114     ct \<leftarrow> gets cur_thread;
115     ct_st \<leftarrow> get_thread_state ct;
116     ct_runnable \<leftarrow> return $ runnable ct_st;
117     action \<leftarrow> gets scheduler_action;
118     (case action
119       of resume_cur_thread \<Rightarrow> do
120            id \<leftarrow> gets idle_thread;
121            assert (ct_runnable \<or> ct = id);
122            return ()
123         od
124       | choose_new_thread \<Rightarrow> do
125           when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
126           schedule_choose_new_thread
127         od
128       | switch_thread candidate \<Rightarrow> do
129           when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
130
131           it \<leftarrow> gets idle_thread;
132           target_prio \<leftarrow> ethread_get tcb_priority candidate;
133
134           \<comment> \<open>Infoflow does not like asking about the idle thread's priority or domain.\<close>
135           ct_prio \<leftarrow> ethread_get_when (ct \<noteq> it) tcb_priority ct;
136           \<comment> \<open>When to look at the bitmaps. This optimisation is used in the C fast path,
137              but there we know @{text cur_thread} is not idle.\<close>
138           fastfail \<leftarrow> schedule_switch_thread_fastfail ct it ct_prio target_prio;
139
140           cur_dom \<leftarrow> gets cur_domain;
141           highest \<leftarrow> gets (is_highest_prio cur_dom target_prio);
142           if (fastfail \<and> \<not>highest)
143           then do
144               \<comment> \<open>Candidate is not best candidate, choose a new thread\<close>
145               tcb_sched_action tcb_sched_enqueue candidate;
146               set_scheduler_action choose_new_thread;
147               schedule_choose_new_thread
148             od
149           else if (ct_runnable \<and> ct_prio = target_prio)
150           then do
151               \<comment> \<open>Current thread was runnable and candidate is not strictly better
152                  want current thread to run next, so append the candidate to end of queue
153                  and choose again\<close>
154               tcb_sched_action tcb_sched_append candidate;
155               set_scheduler_action choose_new_thread;
156               schedule_choose_new_thread
157             od
158           else do
159             guarded_switch_to candidate;
160             \<comment> \<open>Duplication assists in wp proof under different scheduler actions\<close>
161             set_scheduler_action resume_cur_thread
162           od
163        od)
164    od"
165
166instance ..
167end
168
169
170instantiation unit :: state_ext_sched
171begin
172
173
174text \<open>
175  The scheduler is heavily underspecified.
176  It is allowed to pick any active thread or the idle thread.
177  If the thread the scheduler picked is the current thread, it
178  may omit the call to @{const switch_to_thread}. Likewise it
179  may omit the call to @{const switch_to_idle_thread} if the
180  idle thread is the current thread.
181\<close>
182definition schedule_unit :: "(unit,unit) s_monad" where
183"schedule_unit \<equiv> (do
184   cur \<leftarrow> gets cur_thread;
185   threads \<leftarrow> allActiveTCBs;
186   thread \<leftarrow> select threads;
187   (if thread = cur then
188     return () \<sqinter> switch_to_thread thread
189   else
190     switch_to_thread thread)
191 od) \<sqinter>
192 (do
193   cur \<leftarrow> gets cur_thread;
194   idl \<leftarrow> gets idle_thread;
195   if idl = cur then
196     return () \<sqinter> switch_to_idle_thread
197   else switch_to_idle_thread
198  od)"
199
200instance ..
201end
202
203
204lemmas schedule_def = schedule_det_ext_ext_def schedule_unit_def
205
206end
207