1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8The TCB and thread related specifications. 9*) 10 11chapter "Threads and TCBs" 12 13theory Tcb_A 14imports TcbAcc_A Schedule_A ArchTcb_A 15begin 16 17context begin interpretation Arch . 18 19requalify_consts 20 arch_activate_idle_thread 21 sanitise_register 22 arch_get_sanitise_register_info 23 arch_post_modify_registers 24 25end 26 27section "Activating Threads" 28 29text \<open>Threads that are active always have a master Reply capability to 30themselves stored in their reply slot. This is so that a derived Reply 31capability can be generated immediately if they wish to issue one. This function 32sets up a new master Reply capability if one does not exist.\<close> 33definition 34 "setup_reply_master thread \<equiv> do 35 old_cap <- get_cap (thread, tcb_cnode_index 2); 36 when (old_cap = NullCap) $ do 37 set_original (thread, tcb_cnode_index 2) True; 38 set_cap (ReplyCap thread True {AllowGrant, AllowWrite}) (thread, tcb_cnode_index 2) 39 od 40 od" 41 42text \<open>Reactivate a thread if it is not already running.\<close> 43definition 44 restart :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where 45 "restart thread \<equiv> do 46 state \<leftarrow> get_thread_state thread; 47 when (\<not> runnable state \<and> \<not> idle state) $ do 48 cancel_ipc thread; 49 setup_reply_master thread; 50 set_thread_state thread Restart; 51 do_extended_op (tcb_sched_action (tcb_sched_enqueue) thread); 52 do_extended_op (possible_switch_to thread) 53 od 54 od" 55 56text \<open>This action is performed at the end of a system call immediately before 57control is restored to a used thread. If it needs to be restarted then its 58program counter is set to the operation it was performing rather than the next 59operation. The idle thread is handled specially.\<close> 60definition 61 activate_thread :: "(unit,'z::state_ext) s_monad" where 62 "activate_thread \<equiv> do 63 thread \<leftarrow> gets cur_thread; 64 state \<leftarrow> get_thread_state thread; 65 (case state 66 of Running \<Rightarrow> return () 67 | Restart \<Rightarrow> (do 68 pc \<leftarrow> as_user thread getRestartPC; 69 as_user thread $ setNextPC pc; 70 set_thread_state thread Running 71 od) 72 | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread 73 | _ \<Rightarrow> fail) 74 od" 75 76section "Thread Message Formats" 77 78definition 79 load_word_offs :: "obj_ref \<Rightarrow> nat \<Rightarrow> (machine_word,'z::state_ext) s_monad" where 80 "load_word_offs ptr offs \<equiv> 81 do_machine_op $ loadWord (ptr + of_nat (offs * word_size))" 82definition 83 load_word_offs_word :: "obj_ref \<Rightarrow> data \<Rightarrow> (machine_word,'z::state_ext) s_monad" where 84 "load_word_offs_word ptr offs \<equiv> 85 do_machine_op $ loadWord (ptr + (offs * word_size))" 86 87text \<open>Copy message registers from one thread to another.\<close> 88definition 89 copy_mrs :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> obj_ref \<Rightarrow> 90 obj_ref option \<Rightarrow> length_type \<Rightarrow> (length_type,'z::state_ext) s_monad" where 91 "copy_mrs sender sbuf receiver rbuf n \<equiv> 92 do 93 hardware_mrs \<leftarrow> return $ take (unat n) msg_registers; 94 mapM (\<lambda>r. do 95 v \<leftarrow> as_user sender $ getRegister r; 96 as_user receiver $ setRegister r v 97 od) hardware_mrs; 98 buf_mrs \<leftarrow> case (sbuf, rbuf) of 99 (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. do 100 v \<leftarrow> load_word_offs sb_ptr x; 101 store_word_offs rb_ptr x v 102 od) 103 [length msg_registers + 1 ..< Suc (unat n)] 104 | _ \<Rightarrow> return []; 105 return $ min n $ nat_to_len $ length hardware_mrs + length buf_mrs 106 od" 107 108text \<open>The ctable and vtable slots of the TCB.\<close> 109definition 110 get_tcb_ctable_ptr :: "obj_ref \<Rightarrow> cslot_ptr" where 111 "get_tcb_ctable_ptr tcb_ref \<equiv> (tcb_ref, tcb_cnode_index 0)" 112 113definition 114 get_tcb_vtable_ptr :: "obj_ref \<Rightarrow> cslot_ptr" where 115 "get_tcb_vtable_ptr tcb_ref \<equiv> (tcb_ref, tcb_cnode_index 1)" 116 117text \<open>Optionally update the tcb at an address.\<close> 118definition 119 option_update_thread :: "obj_ref \<Rightarrow> ('a \<Rightarrow> tcb \<Rightarrow> tcb) \<Rightarrow> 'a option \<Rightarrow> (unit,'z::state_ext) s_monad" where 120 "option_update_thread thread fn \<equiv> case_option (return ()) (\<lambda>v. thread_set (fn v) thread)" 121 122text \<open>Check that a related capability is at an address. This is done before 123calling @{const cap_insert} to avoid a corner case where the would-be parent of 124the cap to be inserted has been moved or deleted.\<close> 125definition 126 check_cap_at :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> (unit,'z::state_ext) s_monad \<Rightarrow> (unit,'z::state_ext) s_monad" where 127 "check_cap_at cap slot m \<equiv> do 128 cap' \<leftarrow> get_cap slot; 129 when (same_object_as cap cap') m 130 od" 131 132 133text \<open>Helper function for binding notifications\<close> 134definition 135 bind_notification :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" 136where 137 "bind_notification tcbptr ntfnptr \<equiv> do 138 ntfn \<leftarrow> get_notification ntfnptr; 139 ntfn' \<leftarrow> return $ ntfn_set_bound_tcb ntfn (Some tcbptr); 140 set_notification ntfnptr ntfn'; 141 set_bound_notification tcbptr $ Some ntfnptr 142 od" 143 144text \<open>TCB capabilities confer authority to perform seven actions. A thread can 145request to yield its timeslice to another, to suspend or resume another, to 146reconfigure another thread, or to copy register sets into, out of or between 147other threads.\<close> 148fun 149 invoke_tcb :: "tcb_invocation \<Rightarrow> (data list,'z::state_ext) p_monad" 150where 151 "invoke_tcb (Suspend thread) = liftE (do suspend thread; return [] od)" 152| "invoke_tcb (Resume thread) = liftE (do restart thread; return [] od)" 153 154| "invoke_tcb (ThreadControl target slot faultep mcp priority croot vroot buffer) 155 = doE 156 liftE $ option_update_thread target (tcb_fault_handler_update o K) faultep; 157 liftE $ case mcp of None \<Rightarrow> return() 158 | Some (newmcp, _) \<Rightarrow> set_mcpriority target newmcp; 159 (case croot of None \<Rightarrow> returnOk () 160 | Some (new_cap, src_slot) \<Rightarrow> doE 161 cap_delete (target, tcb_cnode_index 0); 162 liftE $ check_cap_at new_cap src_slot 163 $ check_cap_at (ThreadCap target) slot 164 $ cap_insert new_cap src_slot (target, tcb_cnode_index 0) 165 odE); 166 (case vroot of None \<Rightarrow> returnOk () 167 | Some (new_cap, src_slot) \<Rightarrow> doE 168 cap_delete (target, tcb_cnode_index 1); 169 liftE $ check_cap_at new_cap src_slot 170 $ check_cap_at (ThreadCap target) slot 171 $ cap_insert new_cap src_slot (target, tcb_cnode_index 1) 172 odE); 173 (case buffer of None \<Rightarrow> returnOk () 174 | Some (ptr, frame) \<Rightarrow> doE 175 cap_delete (target, tcb_cnode_index 4); 176 liftE $ thread_set (\<lambda>t. t \<lparr> tcb_ipc_buffer := ptr \<rparr>) target; 177 liftE $ case frame of None \<Rightarrow> return () 178 | Some (new_cap, src_slot) \<Rightarrow> 179 check_cap_at new_cap src_slot 180 $ check_cap_at (ThreadCap target) slot 181 $ cap_insert new_cap src_slot (target, tcb_cnode_index 4); 182 cur \<leftarrow> liftE $ gets cur_thread; 183 liftE $ when (target = cur) (do_extended_op reschedule_required) 184 odE); 185 liftE $ case priority 186 of None \<Rightarrow> return() 187 | Some (prio, _) \<Rightarrow> do_extended_op (set_priority target prio); 188 returnOk [] 189 odE" 190 191| "invoke_tcb (CopyRegisters dest src suspend_source resume_target transfer_frame transfer_integer transfer_arch) = 192 (liftE $ do 193 when suspend_source $ suspend src; 194 when resume_target $ restart dest; 195 when transfer_frame $ do 196 mapM_x (\<lambda>r. do 197 v \<leftarrow> as_user src $ getRegister r; 198 as_user dest $ setRegister r v 199 od) frame_registers; 200 pc \<leftarrow> as_user dest getRestartPC; 201 as_user dest $ setNextPC pc 202 od; 203 when transfer_integer $ 204 mapM_x (\<lambda>r. do 205 v \<leftarrow> as_user src $ getRegister r; 206 as_user dest $ setRegister r v 207 od) gpRegisters; 208 cur \<leftarrow> gets cur_thread; 209 arch_post_modify_registers cur dest; 210 when (dest = cur) (do_extended_op reschedule_required); 211 return [] 212 od)" 213 214| "invoke_tcb (ReadRegisters src suspend_source n arch) = 215 (liftE $ do 216 when suspend_source $ suspend src; 217 self \<leftarrow> gets cur_thread; 218 regs \<leftarrow> return (take (unat n) $ frame_registers @ gp_registers); 219 as_user src $ mapM getRegister regs 220 od)" 221 222| "invoke_tcb (WriteRegisters dest resume_target values arch) = 223 (liftE $ do 224 self \<leftarrow> gets cur_thread; 225 b \<leftarrow> arch_get_sanitise_register_info dest; 226 as_user dest $ do 227 zipWithM (\<lambda>r v. setRegister r (sanitise_register b r v)) 228 (frameRegisters @ gpRegisters) values; 229 pc \<leftarrow> getRestartPC; 230 setNextPC pc 231 od; 232 arch_post_modify_registers self dest; 233 when resume_target $ restart dest; 234 when (dest = self) (do_extended_op reschedule_required); 235 return [] 236 od)" 237 238| "invoke_tcb (NotificationControl tcb (Some ntfnptr)) = 239 (liftE $ do 240 bind_notification tcb ntfnptr; 241 return [] 242 od)" 243 244| "invoke_tcb (NotificationControl tcb None) = 245 (liftE $ do 246 unbind_notification tcb; 247 return [] 248 od)" 249 250| "invoke_tcb (SetTLSBase tcb tls_base) = 251 (liftE $ do 252 as_user tcb $ setRegister tlsBaseRegister tls_base; 253 cur \<leftarrow> gets cur_thread; 254 when (tcb = cur) (do_extended_op reschedule_required); 255 return [] 256 od)" 257 258definition 259 set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where 260 "set_domain tptr new_dom \<equiv> do 261 cur \<leftarrow> gets cur_thread; 262 tcb_sched_action tcb_sched_dequeue tptr; 263 thread_set_domain tptr new_dom; 264 ts \<leftarrow> get_thread_state tptr; 265 when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr); 266 when (tptr = cur) reschedule_required 267 od" 268 269definition invoke_domain:: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad" 270where 271 "invoke_domain thread domain \<equiv> 272 liftE (do do_extended_op (set_domain thread domain); return [] od)" 273 274text \<open>Get all of the message registers, both from the sending thread's current 275register file and its IPC buffer.\<close> 276definition 277 get_mrs :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> message_info \<Rightarrow> 278 (message list,'z::state_ext) s_monad" where 279 "get_mrs thread buf info \<equiv> do 280 context \<leftarrow> thread_get (arch_tcb_get_registers o tcb_arch) thread; 281 cpu_mrs \<leftarrow> return (map context msg_registers); 282 buf_mrs \<leftarrow> case buf 283 of None \<Rightarrow> return [] 284 | Some pptr \<Rightarrow> mapM (\<lambda>x. load_word_offs pptr x) 285 [length msg_registers + 1 ..< Suc msg_max_length]; 286 return (take (unat (mi_length info)) $ cpu_mrs @ buf_mrs) 287 od" 288 289end 290