2014-07-14 19:32:44 +00:00
|
|
|
(*
|
|
|
|
|
* Copyright 2014, General Dynamics C4 Systems
|
|
|
|
|
*
|
|
|
|
|
* This software may be distributed and modified according to the terms of
|
|
|
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
|
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
|
|
|
*
|
|
|
|
|
* @TAG(GD_GPL)
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
header "Initialisation"
|
|
|
|
|
|
|
|
|
|
theory KernelInit_H
|
|
|
|
|
imports
|
|
|
|
|
KI_Decls_H
|
|
|
|
|
ArchRetype_H
|
|
|
|
|
Retype_H
|
|
|
|
|
Config_H
|
|
|
|
|
begin
|
|
|
|
|
|
2014-08-09 05:59:24 +00:00
|
|
|
#INCLUDE_HASKELL SEL4/Kernel/Init.lhs bodies_only NOT isAligned funArray newKernelState distinct rangesBy InitData doKernelOp runInit
|
2014-07-14 19:32:44 +00:00
|
|
|
|
2014-07-17 16:22:50 +00:00
|
|
|
consts
|
|
|
|
|
newKSDomSchedule :: "(domain \<times> machine_word) list"
|
|
|
|
|
newKSDomScheduleIdx :: nat
|
|
|
|
|
newKSCurDomain :: domain
|
|
|
|
|
newKSDomainTime :: machine_word
|
|
|
|
|
|
2014-07-14 19:32:44 +00:00
|
|
|
definition
|
|
|
|
|
newKernelState :: "machine_word \<Rightarrow> kernel_state"
|
|
|
|
|
where
|
|
|
|
|
"newKernelState arg \<equiv> \<lparr>
|
|
|
|
|
ksPSpace= newPSpace,
|
|
|
|
|
gsUserPages= (\<lambda>x. None),
|
|
|
|
|
gsCNodes= (\<lambda>x. None),
|
2014-07-17 16:22:50 +00:00
|
|
|
ksDomScheduleIdx = newKSDomScheduleIdx,
|
|
|
|
|
ksDomSchedule = newKSDomSchedule,
|
|
|
|
|
ksCurDomain = newKSCurDomain,
|
|
|
|
|
ksDomainTime = newKSDomainTime,
|
2014-07-14 19:32:44 +00:00
|
|
|
ksReadyQueues= const [],
|
|
|
|
|
ksCurThread= error [],
|
|
|
|
|
ksIdleThread= error [],
|
|
|
|
|
ksSchedulerAction= ResumeCurrentThread,
|
|
|
|
|
ksInterruptState= error [],
|
|
|
|
|
ksWorkUnitsCompleted= 0,
|
|
|
|
|
ksArchState= fst (ArchStateData_H.newKernelState arg),
|
|
|
|
|
ksMachineState= init_machine_state
|
|
|
|
|
\<rparr>"
|
|
|
|
|
|
|
|
|
|
end
|
