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(* 12 Kernel state and kernel monads, imports everything that SEL4.Model needs. 13*) 14 15chapter "Kernel State and Monads" 16 17theory KernelStateData_H 18imports 19 PSpaceStruct_H 20 Structures_H 21 "../machine/$L4V_ARCH/MachineOps" 22 "./$L4V_ARCH/ArchStateData_H" 23begin 24 25context begin interpretation Arch . 26 27requalify_types 28 vmpage_size 29 30end 31 32requalify_types (in Arch) 33 kernel_state 34 35subsection "The Kernel State" 36 37type_synonym ready_queue = "machine_word list" 38translations 39(type) "machine_word list" <= (type) "ready_queue" 40 41text {* We pull a fast one on haskell here ... although Haskell expects 42a KernelMonad which is a StateT monad in KernelData that wraps a MachineMonad, 43we push the extra MachineMonad data into the KernelState. Fortunately the 44update and accessor functions all still work. *} 45 46record kernel_state = 47 ksPSpace :: pspace 48 gsUserPages :: "machine_word \<Rightarrow> vmpage_size option" 49 gsCNodes :: "machine_word \<Rightarrow> nat option" 50 gsUntypedZeroRanges :: "(machine_word \<times> machine_word) set" 51 gsMaxObjectSize :: nat 52 ksDomScheduleIdx :: nat 53 ksDomSchedule :: "(domain \<times> machine_word) list" 54 ksCurDomain :: domain 55 ksDomainTime :: machine_word 56 ksReadyQueues :: "domain \<times> priority \<Rightarrow> ready_queue" 57 ksReadyQueuesL1Bitmap :: "domain \<Rightarrow> machine_word" 58 ksReadyQueuesL2Bitmap :: "domain \<times> nat \<Rightarrow> machine_word" 59 ksCurThread :: machine_word 60 ksIdleThread :: machine_word 61 ksSchedulerAction :: scheduler_action 62 ksInterruptState :: interrupt_state 63 ksWorkUnitsCompleted :: machine_word 64 ksArchState :: Arch.kernel_state 65 ksMachineState :: machine_state 66 67context Arch begin 68context begin global_naming global 69requalify_types KernelStateData_H.kernel_state 70end 71end 72 73type_synonym 'a kernel = "(kernel_state, 'a) nondet_monad" 74 75translations 76 (type) "'c kernel" <= (type) "(kernel_state, 'c) nondet_monad" 77 78subsection "Kernel Functions" 79 80subsubsection "Initial Kernel State" 81 82definition 83 doMachineOp :: "(machine_state, 'a) nondet_monad \<Rightarrow> 'a kernel" 84where 85 "doMachineOp mop \<equiv> do 86 ms \<leftarrow> gets ksMachineState; 87 (r, ms') \<leftarrow> select_f (mop ms); 88 modify (\<lambda>ks. ks \<lparr> ksMachineState := ms' \<rparr>); 89 return r 90 od" 91 92#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue Kernel assert stateAssert findM funArray newKernelState capHasProperty 93#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty 94 95end 96