1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11(* 12 * Operations on thread control blocks. 13 *) 14 15theory Tcb_D 16imports Invocations_D CSpace_D 17begin 18 19definition cdl_update_cnode_cap_data :: "cdl_cap \<Rightarrow> word32 \<Rightarrow> cdl_cap" 20where "cdl_update_cnode_cap_data cap data \<equiv> 21 case cap of cdl_cap.CNodeCap oid _ _ sz \<Rightarrow> if data\<noteq>0 then 22 (let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); 23 new_guard = 24 (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) 25 in CNodeCap oid new_guard new_guard_size sz) 26 else cap 27 | _ \<Rightarrow> cap" 28 29definition cdl_same_arch_obj_as :: "cdl_cap \<Rightarrow> cdl_cap \<Rightarrow> bool" 30where "cdl_same_arch_obj_as capa capb \<equiv> 31 case capa of AsidPoolCap x _ \<Rightarrow> ( 32 case capb of AsidPoolCap y _ \<Rightarrow> y = x 33 | _ \<Rightarrow> False) 34 | AsidControlCap \<Rightarrow> ( 35 case capb of AsidControlCap \<Rightarrow> True 36 | _ \<Rightarrow> False) 37 | FrameCap dev ra _ sa _ _ \<Rightarrow> ( 38 case capb of FrameCap dev' rb _ sb _ _ \<Rightarrow> rb = ra \<and> sb = sa \<and> dev = dev' 39 | _ \<Rightarrow> False) 40 | cdl_cap.PageTableCap a _ _ \<Rightarrow> ( 41 case capb of cdl_cap.PageTableCap b _ _ \<Rightarrow> b = a 42 | _ \<Rightarrow> False) 43 | cdl_cap.PageDirectoryCap a _ _ \<Rightarrow> ( 44 case capb of cdl_cap.PageDirectoryCap b _ _ \<Rightarrow> b = a 45 | _ \<Rightarrow> False) 46 | _ \<Rightarrow> False" 47 48definition 49 decode_tcb_invocation :: "cdl_cap \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) list \<Rightarrow> 50 cdl_tcb_intent \<Rightarrow> cdl_tcb_invocation except_monad" 51where 52 "decode_tcb_invocation target slot caps intent \<equiv> case intent of 53 (* Read another thread's registers. *) 54 TcbReadRegistersIntent suspend flags count \<Rightarrow> 55 returnOk (ReadRegisters (cap_object target) suspend 0 0) \<sqinter> throw 56 57 (* Write another thread's registers. *) 58 | TcbWriteRegistersIntent resume flags count regs \<Rightarrow> 59 returnOk (WriteRegisters (cap_object target) resume [0] 0) \<sqinter> throw 60 61 (* Copy registers from one thread to another. *) 62 | TcbCopyRegistersIntent suspend_source resume_target f1 f2 f3 \<Rightarrow> 63 doE 64 (source_cap, _) \<leftarrow> throw_on_none $ get_index caps 0; 65 source_tcb \<leftarrow> ( 66 case source_cap of 67 TcbCap x \<Rightarrow> returnOk x 68 | _ \<Rightarrow> throw); 69 target_tcb \<leftarrow> returnOk $ cap_object target; 70 returnOk (CopyRegisters target_tcb source_tcb suspend_source resume_target f1 f2 0) 71 odE \<sqinter> throw 72 73 (* Suspend the target thread. *) 74 | TcbSuspendIntent \<Rightarrow> 75 returnOk (Suspend (cap_object target)) \<sqinter> throw 76 77 (* Resume the target thread. *) 78 | TcbResumeIntent \<Rightarrow> 79 returnOk (Resume (cap_object target)) \<sqinter> throw 80 81 (* Configure: target, fault_ep, mcp, priority, cspace_root_data, vspace_root_data, buffer *) 82 | TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer \<Rightarrow> 83 doE 84 cspace_root \<leftarrow> throw_on_none $ get_index caps 0; 85 vspace_root \<leftarrow> throw_on_none $ get_index caps 1; 86 buffer_frame \<leftarrow> throw_on_none $ get_index caps 2; 87 cspace_root_cap_ref \<leftarrow> returnOk $ (cdl_update_cnode_cap_data (fst cspace_root) cspace_root_data,snd cspace_root); 88 vspace_root_cap_ref \<leftarrow> returnOk $ vspace_root; 89 buffer_frame_opt \<leftarrow> returnOk $ (if (buffer \<noteq> 0) then Some (reset_mem_mapping (fst buffer_frame), snd buffer_frame) else None); 90 returnOk (ThreadControl (cap_object target) slot (Some fault_ep) 91 (Some cspace_root_cap_ref) (Some vspace_root_cap_ref) (buffer_frame_opt)) 92 odE \<sqinter> throw 93 94 (* Modify a thread's maximum control priority. *) 95 | TcbSetMCPriorityIntent mcp \<Rightarrow> 96 doE 97 auth_cap \<leftarrow> throw_on_none $ get_index caps 0; 98 returnOk (ThreadControl (cap_object target) slot None None None None) 99 odE \<sqinter> throw 100 101 (* Modify a thread's priority. *) 102 | TcbSetPriorityIntent priority \<Rightarrow> 103 doE 104 auth_cap \<leftarrow> throw_on_none $ get_index caps 0; 105 returnOk (ThreadControl (cap_object target) slot None None None None) 106 odE \<sqinter> throw 107 108 (* Modify a thread's mcp and priority at the same time. *) 109 | TcbSetSchedParamsIntent mcp priority \<Rightarrow> 110 doE 111 auth_cap \<leftarrow> throw_on_none $ get_index caps 0; 112 returnOk (ThreadControl (cap_object target) slot None None None None) 113 odE \<sqinter> throw 114 115 (* Modify a thread's IPC buffer. *) 116 | TcbSetIPCBufferIntent buffer \<Rightarrow> 117 doE 118 buffer_frame \<leftarrow> throw_on_none $ get_index caps 0; 119 buffer_frame_opt \<leftarrow> returnOk $ (if (buffer \<noteq> 0) then Some (reset_mem_mapping (fst buffer_frame), snd buffer_frame) else None); 120 returnOk (ThreadControl (cap_object target) slot None None None buffer_frame_opt) 121 odE \<sqinter> throw 122 123 (* Update the various spaces (CSpace/VSpace) of a thread. *) 124 | TcbSetSpaceIntent fault_ep cspace_root_data vspace_root_data \<Rightarrow> 125 doE 126 cspace_root \<leftarrow> throw_on_none $ get_index caps 0; 127 vspace_root \<leftarrow> throw_on_none $ get_index caps 1; 128 cspace_root_cap_ref \<leftarrow> returnOk $ (cdl_update_cnode_cap_data (fst cspace_root) cspace_root_data,snd cspace_root); 129 vspace_root_cap_ref \<leftarrow> returnOk $ vspace_root; 130 returnOk (ThreadControl (cap_object target) slot (Some fault_ep) 131 (Some cspace_root_cap_ref) (Some vspace_root_cap_ref) None) 132 odE \<sqinter> throw 133 | TcbBindNTFNIntent \<Rightarrow> doE 134 (ntfn_cap, _) \<leftarrow> throw_on_none $ get_index caps 0; 135 returnOk (NotificationControl (cap_object target) (Some (cap_object ntfn_cap))) 136 odE \<sqinter> throw 137 | TcbUnbindNTFNIntent \<Rightarrow> returnOk (NotificationControl (cap_object target) None) \<sqinter> throw 138 | TCBSetTLSBaseIntent \<Rightarrow> returnOk (SetTLSBase (cap_object target)) \<sqinter> throw 139 " 140 141 142(* Delete the given slot of a TCB. *) 143 144definition 145 tcb_empty_thread_slot :: "cdl_object_id \<Rightarrow> cdl_cnode_index \<Rightarrow> unit preempt_monad" 146where 147 "tcb_empty_thread_slot target_tcb target_slot \<equiv> doE 148 cap \<leftarrow> liftE $ get_cap (target_tcb,target_slot); 149 whenE (cap \<noteq> NullCap) $ 150 delete_cap (target_tcb, target_slot) 151 odE" 152 153(* Update the given slot of a TCB with a new cap, delete the previous 154 * capability that was in the slot. *) 155 156definition 157 tcb_update_thread_slot :: "cdl_object_id \<Rightarrow> cdl_cap_ref \<Rightarrow> cdl_cnode_index \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) \<Rightarrow> unit preempt_monad" 158where 159 "tcb_update_thread_slot target_tcb tcb_cap_slot target_slot pcap \<equiv> 160 liftE (do 161 thread_cap \<leftarrow> get_cap tcb_cap_slot; 162 when (thread_cap = TcbCap target_tcb) 163 (insert_cap_child (fst pcap) (snd pcap) (target_tcb, target_slot) 164 \<sqinter> insert_cap_sibling (fst pcap) (snd pcap) (target_tcb,target_slot)) 165 od)" 166 167(* Update a thread's CSpace root. *) 168definition 169 tcb_update_cspace_root :: "cdl_object_id \<Rightarrow> cdl_cap_ref \<Rightarrow> cdl_cap \<times> cdl_cap_ref \<Rightarrow> unit preempt_monad" 170where 171 "tcb_update_cspace_root target_tcb tcb_cap_ref croot \<equiv> 172 doE 173 tcb_empty_thread_slot target_tcb tcb_cspace_slot; 174 src_cap \<leftarrow> liftE $ get_cap (snd croot); 175 whenE (is_cnode_cap src_cap \<and> (cap_object src_cap = cap_object (fst croot))) 176 $ tcb_update_thread_slot target_tcb tcb_cap_ref tcb_cspace_slot croot 177 odE" 178 179(* Update a thread's VSpace root. *) 180definition 181 tcb_update_vspace_root :: "cdl_object_id \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) \<Rightarrow> unit preempt_monad" 182where 183 "tcb_update_vspace_root target_tcb tcb_cap_ref vroot \<equiv> 184 doE 185 tcb_empty_thread_slot target_tcb tcb_vspace_slot; 186 src_cap \<leftarrow> liftE $ get_cap (snd vroot); 187 whenE (cdl_same_arch_obj_as (fst vroot) src_cap) 188 $ tcb_update_thread_slot target_tcb tcb_cap_ref tcb_vspace_slot vroot 189 odE" 190 191 192 193(* Modify the TCB's intent to indicate an error during decode. *) 194definition 195 mark_tcb_intent_error :: "cdl_object_id \<Rightarrow> bool \<Rightarrow> unit k_monad" 196where 197 "mark_tcb_intent_error target_tcb has_error \<equiv> 198 update_thread target_tcb (\<lambda>t. (t\<lparr>cdl_tcb_intent := (cdl_tcb_intent t)\<lparr>cdl_intent_error := has_error\<rparr>\<rparr>))" 199 200(* Update a thread's IPC buffer. *) 201 202definition 203 tcb_update_ipc_buffer :: "cdl_object_id \<Rightarrow> cdl_cap_ref \<Rightarrow> (cdl_cap \<times> cdl_cap_ref) \<Rightarrow> unit preempt_monad" 204where 205 "tcb_update_ipc_buffer target_tcb tcb_cap_ref ipc_buffer \<equiv> 206 doE 207 tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot; 208 liftE $ corrupt_tcb_intent target_tcb; 209 src_cap \<leftarrow> liftE $ get_cap (snd ipc_buffer); 210 whenE (cdl_same_arch_obj_as (fst ipc_buffer) src_cap) 211 $ tcb_update_thread_slot target_tcb tcb_cap_ref tcb_ipcbuffer_slot ipc_buffer 212 odE 213" 214 215(* Resume a thread, aborting any pending operation, and revoking 216 * any incoming reply caps. *) 217definition 218 restart :: "cdl_object_id \<Rightarrow> unit k_monad" 219where 220 "restart target_tcb \<equiv> 221 do 222 cap \<leftarrow> KHeap_D.get_cap (target_tcb,tcb_pending_op_slot); 223 when (cap \<noteq> RestartCap \<and> cap\<noteq> RunningCap) 224 (do 225 CSpace_D.cancel_ipc target_tcb; 226 KHeap_D.set_cap (target_tcb,tcb_replycap_slot) (cdl_cap.MasterReplyCap target_tcb); 227 KHeap_D.set_cap (target_tcb,tcb_pending_op_slot) (cdl_cap.RestartCap) 228 od) 229 od" 230 231(* Suspend a thread, aborting any pending operation, and revoking 232 * any incoming reply caps. *) 233definition 234 suspend :: "cdl_object_id \<Rightarrow> unit k_monad" 235where 236 "suspend target_tcb \<equiv> CSpace_D.cancel_ipc target_tcb >>= K (KHeap_D.set_cap (target_tcb,tcb_pending_op_slot) cdl_cap.NullCap)" 237 238definition 239 bind_notification :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad" 240where 241 "bind_notification tcb_id ntfn_id \<equiv> set_cap (tcb_id, tcb_boundntfn_slot) (BoundNotificationCap ntfn_id)" 242 243definition 244 invoke_tcb :: "cdl_tcb_invocation \<Rightarrow> unit preempt_monad" 245where 246 "invoke_tcb params \<equiv> case params of 247 (* Modify a thread's registers. *) 248 WriteRegisters target_tcb resume _ _ \<Rightarrow> 249 liftE $ 250 do 251 corrupt_tcb_intent target_tcb; 252 when resume $ restart target_tcb 253 od 254 255 (* Read a thread's registers. *) 256 | ReadRegisters src_tcb _ _ _ \<Rightarrow> 257 liftE $ suspend src_tcb \<sqinter> return () 258 259 (* Copy registers from one thread to another *) 260 | CopyRegisters target_tcb source_tcb _ _ _ _ _ \<Rightarrow> 261 liftE $ 262 do 263 suspend source_tcb \<sqinter> return (); 264 restart target_tcb \<sqinter> return (); 265 corrupt_tcb_intent target_tcb 266 od 267 268 (* Suspend this thread. *) 269 | Suspend target_tcb \<Rightarrow> 270 liftE $ suspend target_tcb \<sqinter> return () 271 272 (* Resume this thread. *) 273 | Resume target_tcb \<Rightarrow> 274 liftE $ restart target_tcb 275 276 (* Update a thread's options. *) 277 | ThreadControl target_tcb tcb_cap_slot faultep croot vroot ipc_buffer \<Rightarrow> 278 doE 279 case faultep of 280 Some x \<Rightarrow> liftE $ update_thread target_tcb (\<lambda>tcb. tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>) 281 | None \<Rightarrow> returnOk (); 282 283 (* Possibly update CSpace *) 284 case croot of 285 Some x \<Rightarrow> tcb_update_cspace_root target_tcb tcb_cap_slot x 286 | None \<Rightarrow> returnOk (); 287 288 (* Possibly update VSpace *) 289 case vroot of 290 Some x \<Rightarrow> tcb_update_vspace_root target_tcb tcb_cap_slot x 291 | None \<Rightarrow> returnOk (); 292 293 (* Possibly update Ipc Buffer *) 294 case ipc_buffer of 295 Some x \<Rightarrow> tcb_update_ipc_buffer target_tcb tcb_cap_slot x 296 | None \<Rightarrow> (returnOk () \<sqinter> (doE tcb_empty_thread_slot target_tcb tcb_ipcbuffer_slot; 297 liftE $ corrupt_tcb_intent target_tcb odE)) 298 odE 299 | NotificationControl tcb ntfn \<Rightarrow> 300 liftE $ (case ntfn of 301 Some ntfn_id \<Rightarrow> bind_notification tcb ntfn_id 302 | None \<Rightarrow> unbind_notification tcb) 303 | SetTLSBase tcb \<Rightarrow> liftE $ corrupt_tcb_intent tcb" 304 305 306definition 307 decode_domain_invocation :: "(cdl_cap \<times> cdl_cap_ref) list \<Rightarrow> cdl_domain_intent \<Rightarrow> cdl_domain_invocation except_monad" 308where 309 "decode_domain_invocation caps intent \<equiv> case intent of 310 DomainSetIntent d \<Rightarrow> returnOk (SetDomain (cap_object (fst (hd caps))) d) \<sqinter> throw" 311 312definition 313 set_domain :: "cdl_object_id \<Rightarrow> word8 \<Rightarrow> unit k_monad" 314where 315 "set_domain tcb d \<equiv> update_thread tcb (\<lambda>t. (t\<lparr>cdl_tcb_domain := d \<rparr>))" 316 317definition 318 invoke_domain :: "cdl_domain_invocation \<Rightarrow> unit preempt_monad" 319where 320 "invoke_domain params \<equiv> case params of 321 SetDomain tcb d \<Rightarrow> liftE $ set_domain tcb d" 322 323 324end 325