1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11(* 12Dummy initial kernel state. Real kernel boot up is more complex. 13*) 14 15chapter "An Initial Kernel State" 16 17theory Init_A 18imports "../Retype_A" 19begin 20 21context Arch begin global_naming X64_A 22 23text {* 24 This is not a specification of true kernel 25 initialisation. This theory describes a dummy initial state only, to 26 show that the invariants and refinement relation are consistent. 27*} 28 29(* 8KiB *) 30definition 31 init_irq_node_ptr :: obj_ref where 32 "init_irq_node_ptr = kernel_base + 0x2000" 33 34(* 4KiB *) 35definition 36 init_global_pml4 :: obj_ref where 37 "init_global_pml4 = kernel_base + 0x4000" 38 39(* 4KiB *) 40definition 41 init_global_pdpt :: obj_ref where 42 "init_global_pdpt = kernel_base + 0x5000" 43 44(* 4KiB *) 45definition 46 init_global_pd :: obj_ref where 47 "init_global_pd = kernel_base + 0x6000" 48 49definition 50 "init_arch_state \<equiv> \<lparr> 51 x64_asid_table = Map.empty, 52 x64_global_pml4 = init_global_pml4, 53 x64_kernel_vspace = 54 \<lambda>ref. if ref \<in> {pptr_base .. pptr_base + mask pml4_shift_bits} 55 then X64VSpaceKernelWindow 56 else X64VSpaceInvalidRegion, 57 x64_global_pts = [], 58 x64_global_pdpts = [init_global_pdpt], 59 x64_global_pds = [init_global_pd], 60 x64_current_cr3 = cr3 0 0, 61 x64_allocated_io_ports = \<lambda>_. False, 62 x64_num_ioapics = 1, 63 x64_irq_state = K IRQFree 64 \<rparr>" 65 66definition [simp]: 67 "global_pml4 \<equiv> (\<lambda>_ :: 9 word. InvalidPML4E) 68 (0x1FF := PDPointerTablePML4E (addrFromPPtr init_global_pdpt) {} {})" 69 70(* The kernel uses huge page mappings in the global PDPT to get a view of all physical memory. 71 The exception is the upper-most PDPT entry, which maps to the global page directory. *) 72definition [simp]: 73 "global_pdpt \<equiv> (\<lambda> i :: 9 word. HugePagePDPTE (ucast i << 30) {} {}) 74 (0x1FF := PageDirectoryPDPTE (addrFromPPtr init_global_pd) {} {})" 75 76(* C kernel initialisation refines this down to small pages for devices, but we'll stop here. *) 77definition [simp]: 78 "global_pd \<equiv> (\<lambda> i :: 9 word. LargePagePDE (0x03FE00 + ucast i << 21) {} {})" 79 80definition 81 "init_kheap \<equiv> 82 (\<lambda>x. if \<exists>irq :: irq. init_irq_node_ptr + (ucast irq << cte_level_bits) = x 83 then Some (CNode 0 (empty_cnode 0)) 84 else None) 85 (idle_thread_ptr \<mapsto> 86 TCB \<lparr> 87 tcb_ctable = NullCap, 88 tcb_vtable = NullCap, 89 tcb_reply = NullCap, 90 tcb_caller = NullCap, 91 tcb_ipcframe = NullCap, 92 tcb_state = IdleThreadState, 93 tcb_fault_handler = replicate word_bits False, 94 tcb_ipc_buffer = 0, 95 tcb_fault = None, 96 tcb_bound_notification = None, 97 tcb_mcpriority = minBound, 98 tcb_arch = init_arch_tcb 99 \<rparr>, 100 init_global_pml4 \<mapsto> ArchObj (PageMapL4 global_pml4), 101 init_global_pdpt \<mapsto> ArchObj (PDPointerTable global_pdpt), 102 init_global_pd \<mapsto> ArchObj (PageDirectory global_pd) 103 )" 104 105definition 106 "init_cdt \<equiv> Map.empty" 107 108definition 109 "init_ioc \<equiv> 110 \<lambda>(a,b). (\<exists>obj. init_kheap a = Some obj \<and> 111 (\<exists>cap. cap_of obj b = Some cap \<and> cap \<noteq> cap.NullCap))" 112 113definition 114 "init_A_st \<equiv> \<lparr> 115 kheap = init_kheap, 116 cdt = init_cdt, 117 is_original_cap = init_ioc, 118 cur_thread = idle_thread_ptr, 119 idle_thread = idle_thread_ptr, 120 machine_state = init_machine_state, 121 interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits), 122 interrupt_states = \<lambda>_. Structures_A.IRQInactive, 123 arch_state = init_arch_state, 124 exst = ext_init 125 \<rparr>" 126 127end 128end 129