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 11theory SysInit_SI 12imports 13 "DSpecProofs.Kernel_DP" 14 "Lib.NonDetMonadLemmaBucket" 15begin 16 17definition 18 parse_bootinfo :: "cdl_bootinfo \<Rightarrow> (cdl_cptr list \<times> cdl_cptr list) u_monad" 19where 20 "parse_bootinfo bootinfo \<equiv> do 21 (untyped_start, untyped_end) \<leftarrow> return $ bi_untypes bootinfo; 22 untyped_list \<leftarrow> return [untyped_start .e. (untyped_end - 1)]; 23 24 (free_slot_start, free_slot_end) \<leftarrow> return $ bi_free_slots bootinfo; 25 free_slots \<leftarrow> return [free_slot_start .e. (free_slot_end - 1)]; 26 27 return (untyped_list, free_slots) 28 od" 29 30(* Currently, objects are created in any order. 31 Later versions could create untypes before their children and use the untyped_covers. 32 A refinement will create bigger ones first to remove internal fragmentation. *) 33definition 34 parse_spec :: "cdl_state \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad" 35where 36 "parse_spec spec obj_ids \<equiv> 37 assert (set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)" 38 39(* Create a new object in the next free cnode slot using a given untyped. 40 Return whether or not the operation fails. *) 41definition 42 retype_untyped :: "cdl_cptr \<Rightarrow> cdl_cptr \<Rightarrow> cdl_object_type \<Rightarrow> nat \<Rightarrow> bool u_monad" 43where 44 "retype_untyped free_slot free_untyped type size_bits \<equiv> 45 seL4_Untyped_Retype free_untyped type (of_nat size_bits) 46 seL4_CapInitThreadCNode 0 0 free_slot 1" 47 48definition 49 inc_when :: "bool \<Rightarrow> nat \<Rightarrow> ('s,nat) nondet_monad" 50where 51 "inc_when P x \<equiv> return (if P then Suc x else x)" 52 53lemma inc_when_wp [wp]: 54 "\<lbrace>Q (if B then Suc x else x)\<rbrace> inc_when B x \<lbrace>Q\<rbrace>" 55 by (unfold inc_when_def, wp) 56 57definition 58 update_when :: "bool \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> 'b 59 \<Rightarrow> ('s,('a \<Rightarrow> 'b option)) nondet_monad" 60where 61 "update_when P t a b \<equiv> return (if P then t(a \<mapsto> b) else t)" 62 63lemma update_when_wp [wp]: 64 "\<lbrace>Q (if B then t(a \<mapsto> b) else t)\<rbrace> update_when B t a b \<lbrace>Q\<rbrace>" 65 by (unfold update_when_def, wp) 66 67(* Create the objects in the capDL spec. 68 Caps to new objects are stored in the free slots. *) 69 70definition create_objects :: "cdl_state \<Rightarrow> cdl_object_id list 71 \<Rightarrow> cdl_cptr list \<Rightarrow> cdl_cptr list 72 \<Rightarrow> ((cdl_object_id \<Rightarrow> cdl_cptr option) \<times> cdl_cptr list) u_monad" 73where 74 "create_objects spec obj_ids untyped_cptrs free_cptrs \<equiv> do 75 (obj_id_index, untyped_index, si_caps) \<leftarrow> whileLoop (\<lambda>(obj_id_index, untyped_index, si_caps) _. 76 obj_id_index < length [obj\<leftarrow>obj_ids. real_object_at obj spec] \<and> 77 obj_id_index < length free_cptrs \<and> 78 untyped_index < length untyped_cptrs) 79 (\<lambda>(obj_id_index, untyped_index, si_caps). 80 do 81 obj_id \<leftarrow> return $ [obj\<leftarrow>obj_ids. real_object_at obj spec] ! obj_id_index; 82 free_cptr \<leftarrow> return $ free_cptrs ! obj_id_index; 83 untyped_cptr \<leftarrow> return $ untyped_cptrs ! untyped_index; 84 85 object \<leftarrow> get_spec_object spec obj_id; 86 object_type \<leftarrow> return $ object_type object; 87 object_size \<leftarrow> return $ object_size_bits object; 88 89 fail \<leftarrow> retype_untyped free_cptr untyped_cptr object_type object_size; 90 91 obj_id_index \<leftarrow> inc_when (\<not> fail) obj_id_index; 92 untyped_index \<leftarrow> inc_when fail untyped_index; 93 si_caps \<leftarrow> update_when (\<not> fail) si_caps obj_id free_cptr; 94 return (obj_id_index, untyped_index, si_caps) 95 od) (0, 0, Map.empty); 96 assert (untyped_index \<noteq> length untyped_cptrs); 97 return (si_caps, drop (length [obj\<leftarrow>obj_ids. real_object_at obj spec]) free_cptrs) 98 od" 99 100 101(* This makes the IRQ handler caps. 102 * These caps are then used to set up the IRQs. 103 * We need some predicate to say that they are there. 104 * irq \<mapsto>c IrqHandlerCap cnode_id? 105 *) 106definition create_irq_cap :: "cdl_state \<Rightarrow> (cdl_irq \<times> cdl_cptr) \<Rightarrow> unit u_monad" 107where 108 "create_irq_cap spec \<equiv> \<lambda>(irq, free_cptr). do 109 control_cap \<leftarrow> return seL4_CapIRQControl; 110 root \<leftarrow> return seL4_CapInitThreadCNode; 111 index \<leftarrow> return $ free_cptr; 112 depth \<leftarrow> return (32::word32); 113 114 fail \<leftarrow> seL4_IRQControl_Get control_cap irq root index depth; 115 assert (\<not>fail) 116 od" 117 118definition create_irq_caps :: "cdl_state \<Rightarrow> cdl_cptr list \<Rightarrow> 119 ((cdl_irq \<Rightarrow> cdl_cptr option) \<times> cdl_cptr list) u_monad" 120where 121 "create_irq_caps spec free_cptrs \<equiv> do 122 irqs \<leftarrow> return $ used_irq_list spec; 123 mapM_x (create_irq_cap spec) (zip irqs free_cptrs); 124 si_irq_caps \<leftarrow> return $ map_of (zip irqs free_cptrs); 125 return (si_irq_caps, drop (length irqs) free_cptrs) 126 od" 127 128(* This one installs the caps in the CNodes. 129 * It uses seL4 _IRQHandler_SetEndpoint. 130 * It turns irq_empty to irq_initialised? 131 *) 132definition 133 init_irq :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> 134 (cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_irq \<Rightarrow> unit u_monad" 135where 136 "init_irq spec orig_caps irq_caps irq \<equiv> do 137 irq_handler_cap \<leftarrow> assert_opt $ irq_caps irq; 138 irq_slot \<leftarrow> return $ get_irq_slot irq spec; 139 endpoint_cap \<leftarrow> assert_opt $ opt_cap irq_slot spec; 140 endpoint_cptr \<leftarrow> assert_opt $ orig_caps (cap_object endpoint_cap); 141 142 fail \<leftarrow> seL4_IRQHandler_SetEndpoint irq_handler_cap endpoint_cptr; 143 assert (\<not>fail) 144 od" 145 146definition 147 init_irqs :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> 148 (cdl_irq \<Rightarrow> cdl_cptr option) \<Rightarrow> unit u_monad" 149where 150 "init_irqs spec orig_caps irq_caps \<equiv> do 151 irqs \<leftarrow> return $ bound_irq_list spec; 152 mapM_x (init_irq spec orig_caps irq_caps) irqs 153 od" 154 155 156(* Make a duplicate of a cap in a new free slot. *) 157definition duplicate_cap :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 158 \<Rightarrow> (cdl_object_id \<times> cdl_cptr) \<Rightarrow> unit u_monad" 159where 160 "duplicate_cap spec orig_caps \<equiv> \<lambda>(obj_id, free_slot). do 161 rights \<leftarrow> return $ UNIV; 162 163 dest_root \<leftarrow> return seL4_CapInitThreadCNode; 164 dest_index \<leftarrow> return $ free_slot; 165 dest_depth \<leftarrow> return (32::word32); 166 167 src_root \<leftarrow> return seL4_CapInitThreadCNode; 168 src_index \<leftarrow> assert_opt $ orig_caps obj_id; 169 src_depth \<leftarrow> return (32::word32); 170 171 fail \<leftarrow> seL4_CNode_Copy dest_root dest_index dest_depth 172 src_root src_index src_depth rights; 173 assert (\<not>fail) 174 od" 175 176(* As CNode caps can be moved, referencing the CNodes can be tricky. 177 * Moving capabilities in a particular order would work for all be difficult circular cases, 178 * but just keeping a copy of the caps to all of the CNodes and using the copy is much easier. 179 * 180 * Thread caps are duplicated as the system initialiser needs to have them to start the threads 181 * at the end of initialisation. 182 *) 183definition duplicate_caps :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 184 \<Rightarrow> cdl_object_id list \<Rightarrow> cdl_cptr list 185 \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) u_monad" 186where 187 "duplicate_caps spec orig_caps obj_ids free_slots \<equiv> do 188 obj_ids' \<leftarrow> return [obj_id \<leftarrow> obj_ids. cnode_at obj_id spec \<or> tcb_at obj_id spec]; 189 assert (length obj_ids' \<le> length free_slots); 190 mapM_x (duplicate_cap spec orig_caps) (zip obj_ids' free_slots); 191 return $ map_of $ zip obj_ids' free_slots 192 od" 193 194(* Initialise a single tcb (cspace, vspace and fault_ep). *) 195definition init_tcb :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id \<Rightarrow> unit u_monad" 196where 197 "init_tcb spec orig_caps tcb_id \<equiv> do 198 cdl_tcb \<leftarrow> assert_opt $ opt_thread tcb_id spec; 199 cdl_cspace_root \<leftarrow> assert_opt $ opt_cap (tcb_id, tcb_cspace_slot) spec; 200 cdl_vspace_root \<leftarrow> assert_opt $ opt_cap (tcb_id, tcb_vspace_slot) spec; 201 cdl_ipcbuffer \<leftarrow> assert_opt $ opt_cap (tcb_id, tcb_ipcbuffer_slot) spec; 202 ipcbuf_addr \<leftarrow> return $ tcb_ipc_buffer_address cdl_tcb; 203 priority \<leftarrow> return $ tcb_priority cdl_tcb; 204 205 sel4_tcb \<leftarrow> assert_opt $ orig_caps tcb_id; 206 sel4_cspace_root \<leftarrow> assert_opt $ orig_caps (cap_object cdl_cspace_root); 207 sel4_vspace_root \<leftarrow> assert_opt $ orig_caps (cap_object cdl_vspace_root); 208 sel4_ipcbuffer \<leftarrow> assert_opt $ orig_caps (cap_object cdl_ipcbuffer); 209 sel4_fault_ep \<leftarrow> return $ cdl_tcb_fault_endpoint cdl_tcb; 210 211 sel4_cspace_root_data \<leftarrow> return $ guard_as_rawdata cdl_cspace_root; 212 sel4_vspace_root_data \<leftarrow> return 0; 213 214 fail \<leftarrow> seL4_TCB_Configure sel4_tcb sel4_fault_ep 215 sel4_cspace_root sel4_cspace_root_data 216 sel4_vspace_root sel4_vspace_root_data 217 ipcbuf_addr sel4_ipcbuffer; 218 assert (\<not>fail) 219 od" 220 221(* Set the registers of a single tcb (cspace, vspace and fault_ep). *) 222definition configure_tcb :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id \<Rightarrow> unit u_monad" 223where 224 "configure_tcb spec orig_caps tcb_id \<equiv> do 225 cdl_tcb \<leftarrow> assert_opt $ opt_thread tcb_id spec; 226 sel4_tcb \<leftarrow> assert_opt $ orig_caps tcb_id; 227 ip \<leftarrow> return $ tcb_ip cdl_tcb; 228 sp \<leftarrow> return $ tcb_sp cdl_tcb; 229 regs \<leftarrow> return [ip, sp]; 230 fail \<leftarrow> seL4_TCB_WriteRegisters sel4_tcb False 0 2 regs; 231 assert fail 232 od" 233 234(* Initialise all the tcbs (cspace, vspace and fault_ep). *) 235definition init_tcbs :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad" 236where 237 "init_tcbs spec orig_caps objects \<equiv> do 238 tcb_ids \<leftarrow> return [obj \<leftarrow> objects. tcb_at obj spec]; 239 mapM_x (init_tcb spec orig_caps) tcb_ids; 240 mapM_x (configure_tcb spec orig_caps) tcb_ids 241 od" 242 243 244 245(************************** 246 * VSpace Initialisation. * 247 **************************) 248 249(* Sets the asid for a page directory from the initialiser's asid pool. *) 250definition set_asid :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id 251 \<Rightarrow> unit u_monad" 252where 253 "set_asid spec orig_caps page_id \<equiv> do 254 (* Set asid pool for the page directory. *) 255 sel4_asid_pool \<leftarrow> return seL4_CapInitThreadASIDPool; 256 sel4_page \<leftarrow> assert_opt $ orig_caps page_id; 257 fail \<leftarrow> seL4_ASIDPool_Assign sel4_asid_pool sel4_page; 258 assert (\<not>fail) 259 od" 260 261(* Set the ASIDs for the page directories. *) 262definition init_pd_asids :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad" 263where 264 "init_pd_asids spec orig_caps obj_ids \<equiv> do 265 pd_ids \<leftarrow> return [obj_id \<leftarrow> obj_ids. pd_at obj_id spec]; 266 mapM_x (set_asid spec orig_caps) pd_ids 267 od" 268 269(* Map the right cap into the slot of a page directory or page table. *) 270definition map_page :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id 271 \<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> unit u_monad" 272where 273 "map_page spec orig_caps page_id pd_id rights vaddr \<equiv> do 274 cdl_page \<leftarrow> assert_opt $ opt_object page_id spec; 275 sel4_page \<leftarrow> assert_opt $ orig_caps page_id; 276 sel4_pd \<leftarrow> assert_opt $ orig_caps pd_id; 277 278 vmattribs \<leftarrow> assert_opt $ opt_vmattribs cdl_page; 279 280 if (pt_at page_id spec) then 281 seL4_PageTable_Map sel4_page sel4_pd vaddr vmattribs 282 else if (frame_at page_id spec) then 283 seL4_Page_Map sel4_page sel4_pd vaddr rights vmattribs 284 else 285 fail; 286 return () 287 od" 288 289(* Maps a page directory slot (and all its contents if it's a page table). *) 290definition map_page_directory_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 291 \<Rightarrow> cdl_object_id\<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad" 292where 293 "map_page_directory_slot spec orig_caps pd_id pd_slot \<equiv> do 294 page_cap \<leftarrow> assert_opt $ opt_cap (pd_id, pd_slot) spec; 295 page_id \<leftarrow> return $ cap_object page_cap; 296 297 (* The page table's virtual address is given by the number of slots and how much memory each maps. 298 Each page directory slot maps 10+12 bits of memory (by the page table and page respectively). *) 299 page_vaddr \<leftarrow> return $ of_nat pd_slot << (pt_size + small_frame_size); 300 page_rights \<leftarrow> return (cap_rights page_cap); 301 302 when (page_cap \<noteq> NullCap) 303 (map_page spec orig_caps page_id pd_id page_rights page_vaddr) 304 305 od" 306 307(* Maps a page directory and all its contents. *) 308definition map_page_directory :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id 309 \<Rightarrow> unit u_monad" 310where 311 "map_page_directory spec orig_caps pd_id \<equiv> do 312 pd_slots \<leftarrow> return $ slots_of_list spec pd_id; 313 mapM_x (map_page_directory_slot spec orig_caps pd_id) pd_slots 314 od" 315 316(* Maps a page directory slot. *) 317definition map_page_table_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id 318 \<Rightarrow> cdl_object_id \<Rightarrow> word32 \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad" 319where 320 "map_page_table_slot spec orig_caps pd_id pt_id pt_vaddr pt_slot \<equiv> do 321 frame_cap \<leftarrow> assert_opt $ opt_cap (pt_id, pt_slot) spec; 322 page \<leftarrow> return $ cap_object frame_cap; 323 324 (* The page's virtual address is the page table's virtual address, 325 plus the relative address of the page in the page table. 326 Each page stores 12 bits of memory. *) 327 page_vaddr \<leftarrow> return $ pt_vaddr + (of_nat pt_slot << small_frame_size); 328 page_rights \<leftarrow> return (cap_rights frame_cap); 329 when (frame_cap \<noteq> NullCap) 330 (map_page spec orig_caps page pd_id page_rights page_vaddr) 331 od" 332 333(* Maps a page table's slots. *) 334definition map_page_table_slots :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id 335 \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad" 336where 337 "map_page_table_slots spec orig_caps pd_id pd_slot \<equiv> do 338 page_cap \<leftarrow> assert_opt $ opt_cap (pd_id, pd_slot) spec; 339 page \<leftarrow> return $ cap_object page_cap; 340 page_slots \<leftarrow> return $ slots_of_list spec page; 341 342 (* The page's virtual address is given by the number of slots and how much memory each maps. 343 Each page directory slot maps 10+12 bits of memory (by the page table and page respectively). *) 344 page_vaddr \<leftarrow> return $ of_nat pd_slot << (pt_size + small_frame_size); 345 346 when (fake_pt_cap_at (pd_id, pd_slot) spec) 347 (mapM_x (map_page_table_slot spec orig_caps pd_id page page_vaddr) page_slots) 348 od" 349 350(* Maps a page directory and all its contents. *) 351definition map_page_directory_page_tables :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id 352 \<Rightarrow> unit u_monad" 353where 354 "map_page_directory_page_tables spec orig_caps pd_id \<equiv> do 355 pd_slots \<leftarrow> return $ slots_of_list spec pd_id; 356 mapM_x (map_page_table_slots spec orig_caps pd_id) pd_slots 357 od" 358 359(* Maps page directories and all their contents. *) 360definition init_vspace :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad" 361where 362 "init_vspace spec orig_caps obj_ids \<equiv> do 363 pd_ids \<leftarrow> return [obj_id \<leftarrow> obj_ids. pd_at obj_id spec]; 364 mapM_x (map_page_directory spec orig_caps) pd_ids; 365 mapM_x (map_page_directory_page_tables spec orig_caps) pd_ids 366 od" 367 368(************************** 369 * CSpace Initialisation. * 370 **************************) 371 372datatype init_cnode_mode = Move | Copy 373 374(* initialises a CNode slot with the desired cap, either moving them or copying it. *) 375definition init_cnode_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 376 \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 377 \<Rightarrow> (cdl_irq \<Rightarrow> cdl_cptr option) 378 \<Rightarrow> init_cnode_mode \<Rightarrow> cdl_object_id 379 \<Rightarrow> cdl_cnode_index \<Rightarrow> bool u_monad" 380where 381 "init_cnode_slot spec orig_caps dup_caps irq_caps mode cnode_id cnode_slot \<equiv> do 382 target_cap \<leftarrow> assert_opt (opt_cap (cnode_id, cnode_slot) spec); 383 target_cap_obj \<leftarrow> return (cap_object target_cap); 384 target_cap_irq \<leftarrow> return (cap_irq target_cap); 385 386 target_cap_rights \<leftarrow> return (cap_rights target_cap); 387 388 (* for endpoint this is the badge, for cnodes, this is the (encoded) guard *) 389 target_cap_data \<leftarrow> return (cap_data target_cap); 390 391 is_ep_cap \<leftarrow> return (ep_related_cap target_cap); 392 is_irqhandler_cap \<leftarrow> return (is_irqhandler_cap target_cap); 393 394 (* Any original caps (which includes IRQ Hander caps) are moved, not copied. *) 395 move_cap \<leftarrow> return (original_cap_at (cnode_id, cnode_slot) spec); 396 397 dest_obj \<leftarrow> get_spec_object spec cnode_id; 398 dest_size \<leftarrow> return (object_size_bits dest_obj); 399 400 (* Use a copy of the cap to reference the destination, 401 in case the original has already been moved. *) 402 dest_root \<leftarrow> assert_opt (dup_caps cnode_id); 403 dest_index \<leftarrow> return (of_nat cnode_slot); 404 dest_depth \<leftarrow> return (of_nat dest_size); 405 406 (* Use an original cap to reference the object to copy. *) 407 src_root \<leftarrow> return seL4_CapInitThreadCNode; 408 src_index \<leftarrow> assert_opt (if is_irqhandler_cap 409 then irq_caps target_cap_irq 410 else orig_caps target_cap_obj); 411 src_depth \<leftarrow> return (32::word32); 412 413 (* If it's a NullCap, then there's no need to do anything. 414 * If it's a cap that wants to be moved, and we want to move the cap, move (mutate) it. 415 * If it's a cap that wants to be copied, and we want to copy it, then copy (mint) it. 416 *) 417 if (target_cap = NullCap) then 418 return True 419 else if (mode = Move \<and> move_cap) then ( 420 if (is_ep_cap \<or> is_irqhandler_cap) then 421 (seL4_CNode_Move dest_root dest_index dest_depth src_root src_index src_depth) 422 else 423 (seL4_CNode_Mutate dest_root dest_index dest_depth src_root src_index src_depth target_cap_data) 424 ) 425 else if (mode = Copy \<and> \<not> move_cap) then 426 seL4_CNode_Mint dest_root dest_index dest_depth src_root src_index src_depth target_cap_rights target_cap_data 427 else 428 return True 429 od" 430 431(* Initialises a CNode with it's desired caps, either moving them or copying them. *) 432definition init_cnode :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 433 \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 434 \<Rightarrow> (cdl_irq \<Rightarrow> cdl_cptr option) 435 \<Rightarrow> init_cnode_mode \<Rightarrow> cdl_object_id \<Rightarrow> unit u_monad" 436where 437 "init_cnode spec orig_caps dup_caps irq_caps mode cnode_id \<equiv> do 438 cnode_slots \<leftarrow> return $ slots_of_list spec cnode_id; 439 mapM_x (init_cnode_slot spec orig_caps dup_caps irq_caps mode cnode_id) cnode_slots 440 od" 441 442(* Initialises CNodes with their desired caps in two passes. 443 First pass copies caps, the second moves them. *) 444definition init_cspace :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 445 \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) 446 \<Rightarrow> (cdl_irq \<Rightarrow> cdl_cptr option) 447 \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad" 448where 449 "init_cspace spec orig_caps dup_caps irq_caps obj_ids \<equiv> do 450 cnode_ids \<leftarrow> return [obj_id \<leftarrow> obj_ids. cnode_at obj_id spec]; 451 mapM_x (init_cnode spec orig_caps dup_caps irq_caps Copy) cnode_ids; 452 mapM_x (init_cnode spec orig_caps dup_caps irq_caps Move) cnode_ids 453 od" 454 455(* Initialise a single tcb (cspace, vspace and fault_ep). *) 456definition start_thread :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id \<Rightarrow> unit u_monad" 457where 458 "start_thread spec dup_caps tcb_id \<equiv> do 459 sel4_tcb \<leftarrow> assert_opt $ dup_caps tcb_id; 460 fail \<leftarrow> seL4_TCB_Resume sel4_tcb; 461 assert fail 462 od" 463 464definition start_threads :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id list 465 \<Rightarrow> unit u_monad" 466where 467 "start_threads spec orig_caps obj_ids \<equiv> do 468 tcbs \<leftarrow> return [obj_id \<leftarrow> obj_ids. is_waiting_thread_at obj_id spec]; 469 mapM_x (start_thread spec orig_caps) tcbs 470 od" 471 472definition init_system :: "cdl_state \<Rightarrow> cdl_bootinfo \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad" 473where 474 "init_system spec bootinfo obj_ids \<equiv> do 475 (untyped_cptrs, free_cptrs) \<leftarrow> parse_bootinfo bootinfo; 476 477 (orig_caps, free_cptrs) \<leftarrow> create_objects spec obj_ids untyped_cptrs free_cptrs; 478 (irq_caps, free_cptrs) \<leftarrow> create_irq_caps spec free_cptrs; 479 dup_caps \<leftarrow> duplicate_caps spec orig_caps obj_ids free_cptrs; 480 481 init_irqs spec orig_caps irq_caps; 482 init_pd_asids spec orig_caps obj_ids; 483 init_vspace spec orig_caps obj_ids; 484 init_tcbs spec orig_caps obj_ids; 485 init_cspace spec orig_caps dup_caps irq_caps obj_ids; 486 start_threads spec dup_caps obj_ids 487 od" 488 489end 490