The seL4 microkernel https://sel4.systems/

config.cmake 10KB

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