1# 2# Copyright 2017, Data61 3# Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4# ABN 41 687 119 230. 5# 6# This software may be distributed and modified according to the terms of 7# the GNU General Public License version 2. Note that NO WARRANTY is provided. 8# See "LICENSE_GPLv2.txt" for details. 9# 10# @TAG(DATA61_GPL) 11# 12 13cmake_minimum_required(VERSION 3.7.2) 14 15set(configure_string "") 16 17# Set kernel branch 18config_set(KernelIsMCS KERNEL_RT ON) 19 20# Proof based configuration variables 21set(CSPEC_DIR "." CACHE PATH "") 22set(SKIP_MODIFIES ON CACHE BOOL "") 23set(SORRY_BITFIELD_PROOFS OFF CACHE BOOL "") 24find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH) 25set(force FORCE) 26if(KernelVerificationBuild) 27 set(force CLEAR) 28endif() 29mark_as_advanced(${force} CSPEC_DIR SKIP_MODIFIES SORRY_BITFIELD_PROOFS UMM_TYPES) 30# Use a custom target for collecting information during generation that we need during build 31add_custom_target(kernel_config_target) 32# Put our common top level types in 33set_property(TARGET kernel_config_target APPEND PROPERTY TOPLEVELTYPES 34 cte_C tcb_C endpoint_C notification_C asid_pool_C pte_C pde_C user_data_C 35 user_data_device_C 36) 37 38######################## 39# Architecture selection 40######################## 41config_choice(KernelArch ARCH "Architecture to use when building the kernel" 42 "arm;KernelArchARM;ARCH_ARM" 43 "riscv;KernelArchRiscV;ARCH_RISCV" 44 "x86;KernelArchX86;ARCH_X86" 45) 46 47# Set defaults for common variables 48set(KernelHaveFPU OFF) 49 50include(src/arch/arm/config.cmake) 51include(src/arch/riscv/config.cmake) 52include(src/arch/x86/config.cmake) 53 54include(include/32/mode/config.cmake) 55include(include/64/mode/config.cmake) 56include(src/config.cmake) 57 58# Enshrine common variables in the config 59config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}") 60 61# System parameters 62config_string(KernelRootCNodeSizeBits ROOT_CNODE_SIZE_BITS 63 "Root CNode Size (2^n slots) \ 64 The acceptable range is 4-27, based on the kernel-supplied caps.\ 65 The root CNode needs at least enough space to contain up to\ 66 BI_CAP_DYN_START. Note that in practice your root CNode will need\ 67 to be several bits larger than 4 to fit untyped caps and\ 68 cannot be 27 bits as it won't fit in memory." 69 DEFAULT 12 70 UNQUOTE 71) 72 73config_string(KernelBootThreadTimeSlice BOOT_THREAD_TIME_SLICE 74 "Number of milliseconds until the boot thread is preempted." 75 DEFAULT 5 76 UNQUOTE 77) 78config_string(KernelTimeSlice TIME_SLICE 79 "Number of timer ticks until a thread is preempted." 80 DEFAULT 5 81 UNQUOTE 82) 83config_string(KernelRetypeFanOutLimit RETYPE_FAN_OUT_LIMIT 84 "Maximum number of objects that can be created in a single Retype() invocation." 85 DEFAULT 256 86 UNQUOTE 87) 88config_string(KernelMaxNumWorkUnitsPerPreemption MAX_NUM_WORK_UNITS_PER_PREEMPTION 89 "Maximum number of work units (delete/revoke iterations) until the kernel checks for\ 90 pending interrupts (and preempts the currently running syscall if interrupts are pending)." 91 DEFAULT 100 92 UNQUOTE 93) 94config_string(KernelResetChunkBits RESET_CHUNK_BITS 95 "Maximum size in bits of chunks of memory to zero before checking a preemption point." 96 DEFAULT 8 97 UNQUOTE 98) 99config_string(KernelMaxNumBootinfoUntypedCaps MAX_NUM_BOOTINFO_UNTYPED_CAPS 100 "Max number of bootinfo untyped caps" 101 DEFAULT 230 102 UNQUOTE 103) 104config_option(KernelFastpath FASTPATH "Enable IPC fastpath" DEFAULT ON) 105 106config_string(KernelNumDomains NUM_DOMAINS "The number of scheduler domains in the system" DEFAULT 1 UNQUOTE) 107 108find_file(KernelDomainSchedule default_domain.c PATHS src/config CMAKE_FIND_ROOT_PATH_BOTH 109 DOC "A C file providing the symbols ksDomSchedule and ksDomeScheudleLength \ 110 to be linked with the kernel as a scheduling configuration." 111) 112 113config_string(KernelNumPriorities NUM_PRIORITIES 114 "The number of priority levels per domain. Valid range 1-256" 115 DEFAULT 256 116 UNQUOTE 117) 118 119config_string(KernelMaxNumNodes MAX_NUM_NODES "Max number of CPU cores to boot" 120 DEFAULT 1 121 DEPENDS "${KernelNumDomains} EQUAL 1;NOT KernelArchRiscV" 122 UNQUOTE 123) 124 125config_string(KernelStackBits KERNEL_STACK_BITS 126 "This describes the log2 size of the kernel stack. Great care should be taken as\ 127 there is no guard below the stack so setting this too small will cause random\ 128 memory corruption" 129 DEFAULT 12 130 UNQUOTE 131) 132 133config_string(KernelWCETScale KERNEL_WCET_SCALE 134 "Multiplier to scale kernel WCET estimate by. \ 135 The kernel WCET estimate is used to ensure a thread has enough budget \ 136 to get in and out of the kernel. When running in a simulator the WCET \ 137 estimate, which is tuned for hardware, may not be sufficient. This \ 138 option provides a hacky knob that can be fiddled with when running \ 139 inside a simulator." 140 DEFAULT 1 141 UNQUOTE 142) 143 144config_string(KernelFPUMaxRestoresSinceSwitch FPU_MAX_RESTORES_SINCE_SWITCH 145 "This option is a heuristic to attempt to detect when the FPU is no longer in use,\ 146 allowing the kernel to save the FPU state out so that the FPU does not have to be\ 147 enabled/disabled every thread swith. Every time we restore a thread and there is\ 148 active FPU state, we increment this setting and if it exceeds this threshold we\ 149 switch to the NULL state." 150 DEFAULT 64 151 DEPENDS "KernelHaveFPU" UNDEF_DISABLED 152 UNQUOTE 153) 154 155config_option(KernelVerificationBuild VERIFICATION_BUILD 156 "When enabled this configuration option prevents the usage of any other options that\ 157 would compromise the verification story of the kernel. Enabling this option does NOT\ 158 imply you are using a verified kernel." 159 DEFAULT ON 160) 161 162config_option(KernelDebugBuild DEBUG_BUILD 163 "Enable debug facilities (symbols and assertions) in the kernel" 164 DEFAULT ON 165 DEPENDS "NOT KernelVerificationBuild" DEFAULT_DISABLED OFF 166) 167 168config_option(HardwareDebugAPI HARDWARE_DEBUG_API 169 "Builds the kernel with support for a userspace debug API, which can \ 170 allows userspace processes to set breakpoints, watchpoints and to \ 171 single-step through thread execution." 172 DEFAULT OFF 173 DEPENDS "NOT KernelVerificationBuild" 174) 175config_option(KernelPrinting PRINTING 176 "Allow the kernel to print out messages to the serial console during bootup and execution." 177 DEFAULT "${KernelDebugBuild}" 178 DEPENDS "NOT KernelVerificationBuild" DEFAULT_DISABLED OFF 179) 180config_choice(KernelBenchmarks KERNEL_BENCHMARK "Enable benchamrks including logging and tracing info. \ 181 Setting this value > 1 enables a 1MB log buffer and functions for extracting data from it \ 182 at user level. NOTE this is only tested on the sabre and will not work on platforms with < 512mb memory. \ 183 This is not fully implemented for x86. \ 184 none -> No Benchmarking features enabled. \ 185 generic -> Enable global benchmarks config variable with no specific features. \ 186 track_kernel_entries -> Log kernel entries information including timing, number of invocations and arguments for \ 187 system calls, interrupts, user faults and VM faults. \ 188 tracepoints -> Enable manually inserted tracepoints that the kernel will track time consumed between. \ 189 track_utilisation -> Enable the kernel to track each thread's utilisation time." 190 "none;KernelBenchmarksNone;NO_BENCHMARKS" 191 "generic;KernelBenchmarksGeneric;BENCHMARK_GENERIC;NOT KernelVerificationBuild" 192 "track_kernel_entries;KernelBenchmarksTrackKernelEntries;BENCHMARK_TRACK_KERNEL_ENTRIES;NOT KernelVerificationBuild" 193 "tracepoints;KernelBenchmarksTracepoints;BENCHMARK_TRACEPOINTS;NOT KernelVerificationBuild" 194 "track_utilisation;KernelBenchmarksTrackUtilisation;BENCHMARK_TRACK_UTILISATION;NOT KernelVerificationBuild" 195) 196if(NOT (KernelBenchmarks STREQUAL "none")) 197 config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS ON) 198else() 199 config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS OFF) 200endif() 201config_string(KernelMaxNumTracePoints MAX_NUM_TRACE_POINTS 202 "Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data, \ 203 where k is an integer between 0 and this value - 1. The maximum number of \ 204 different trace point identifiers which can be used." 205 DEFAULT 1 206 DEPENDS "NOT KernelVerificationBuild;KernelBenchmarksTracepoints" DEFAULT_DISABLED 0 207 UNQUOTE 208) 209# TODO: this config has no business being in the build system, and should 210# be moved to C headers, but for now must be emulated here for compatibility 211if(KernelBenchmarksTrackKernelEntries OR KernelBenchmarksTracepoints) 212 config_set(KernelBenchmarkUseKernelLogBuffer BENCHMARK_USE_KERNEL_LOG_BUFFER ON) 213else() 214 config_set(KernelBenchmarkUseKernelLogBuffer BENCHMARK_USE_KERNEL_LOG_BUFFER OFF) 215endif() 216 217config_option(KernelIRQReporting IRQ_REPORTING 218 "seL4 does not properly check for and handle spurious interrupts. This can result \ 219 in unnecessary output from the kernel during debug builds. If you are CERTAIN these \ 220 messages are benign then use this config to turn them off." 221 DEFAULT ON 222 DEPENDS "KernelPrinting" DEFAULT_DISABLED OFF 223) 224config_option(KernelColourPrinting COLOUR_PRINTING 225 "In debug mode, seL4 prints diagnostic messages to its serial output describing, \ 226 e.g., the cause of system call errors. This setting determines whether ANSI escape \ 227 codes are applied to colour code these error messages. You may wish to disable this \ 228 setting if your serial output is redirected to a file or pipe." 229 DEFAULT ON 230 DEPENDS "KernelPrinting" DEFAULT_DISABLED OFF 231) 232config_string(KernelUserStackTraceLength USER_STACK_TRACE_LENGTH 233 "On a double fault the kernel can try and print out the users stack to aid \ 234 debugging. This option determines how many words of stack should be printed." 235 DEFAULT 16 236 DEPENDS "KernelPrinting" DEFAULT_DISABLED 0 237 UNQUOTE 238) 239 240config_choice(KernelOptimisation KERNEL_OPT_LEVEL "Select the kernel optimisation level" 241 "-O2;KerenlOptimisationO2;KERNEL_OPT_LEVEL_O2" 242 "-Os;KerenlOptimisationOS;KERNEL_OPT_LEVEL_OS" 243 "-O1;KerenlOptimisationO1;KERNEL_OPT_LEVEL_O1" 244 "-O3;KerenlOptimisationO3;KERNEL_OPT_LEVEL_O3" 245) 246 247config_option(KernelFWholeProgram KERNEL_FWHOLE_PROGRAM 248 "Enable -fwhole-program when linking kernel. This should work modulo gcc bugs, which \ 249 are not uncommon with -fwhole-program. Consider this feature experimental!" 250 DEFAULT OFF 251) 252 253 254config_option(KernelDangerousCodeInjection DANGEROUS_CODE_INJECTION 255 "Adds a system call that allows users to specify code to be run in kernel mode. \ 256 Useful for profiling." 257 DEFAULT OFF 258 DEPENDS "NOT KernelARMHypervisorSupport;NOT KernelVerificationBuild;NOT KernelPlatformHikey;NOT KernelSkimWindow" 259) 260 261config_option(KernelDebugDisablePrefetchers DEBUG_DISABLE_PREFETCHERS 262 "On ia32 platforms, this option disables the L2 hardware prefetcher, the L2 adjacent \ 263 cache line prefetcher, the DCU prefetcher and the DCU IP prefetcher. On the cortex \ 264 a53 this disables the L1 Data prefetcher." 265 DEFAULT OFF 266 DEPENDS "KernelArchX86 OR KernelPlatformHikey" 267) 268 269config_string(KernelWcetScale KERNEL_WCET_SCALE 270 "Multiplier to scale kernel WCET estimate by: the kernel WCET estimate \ 271 is used to ensure a thread has enough budget to get in and out of the \ 272 kernel. When running in a simulator the WCET estimate, which is tuned \ 273 for hardware, may not be sufficient. This option provides a hacky knob \ 274 that can be fiddled with when running inside a simulator." 275 DEFAULT 1 276 UNQUOTE 277) 278 279add_config_library(kernel "${configure_string}") 280