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