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