Files
seL4/Kconfig
Kofi Doku Atuah 4b491dcf0c SELFOUR-836: arm-hyp: Config option for saving/loading vs trapping debug state
Provides a configuration option for enabling HDCR.TD* traps, or saving and loading debug
state on VCPU switches. Currently verification only plans to support the trap setting.

As this option complicates all of the #ifdef's related to debug registers even further,
abstractions for enabling/disabling each individual piece of the debug code for different
configuration options are also implemented.

Part of these refactored #ifdef guards was to remove the guards completely from libsel4
around the definitions of the number of breakpoints and watchpoints.
2017-04-03 14:21:27 +10:00

715 lines
22 KiB
Plaintext

#
# 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)
#
config KERNEL_PATH
string
option env="KERNEL_ROOT_PATH"
config ARCH_ARM_V6
bool
default n
config ARCH_ARM_V7A
bool
default n
config ARCH_ARM_V8A
bool
default n
config HAVE_FPU
bool
default n
config KERNEL_MASTER
bool
default y
# Native word size of the current platform. This is primarily intended for use
# in code generators that need to know, at generation-time, the word size of
# the target platform.
config WORD_SIZE
int
default 32 if ARCH_IA32 || ARCH_AARCH32
default 64 if ARCH_X86_64 || ARCH_AARCH64
menu "seL4 System"
choice
prompt "Architecture Type"
default ARCH_X86
help
Select the architecture seL4 will be running on.
config ARCH_X86
select HAVE_FPU
bool "x86"
config ARCH_ARM
bool "ARM"
endchoice
config ARCH_X86_64
bool "64-bit kernel"
default n
depends on ARCH_X86
config ARCH_AARCH64
bool "64-bit kernel"
default n
depends on ARCH_ARM
config ARCH_IA32
bool
default y if !ARCH_X86_64 && ARCH_X86
config ARCH_AARCH32
bool
default y if !ARCH_AARCH64 && ARCH_ARM
# CPU values.
config ARM1136JF_S
bool
default n
config ARM_CORTEX_A7
bool
default n
config ARM_CORTEX_A8
bool
default n
config ARM_CORTEX_A9
bool
default n
config ARM_CORTEX_A15
bool
default n
config ARM_CORTEX_A53
bool
default n
config ARM_CORTEX_A57
bool
default n
config PLAT_EXYNOS54XX
bool
default n
help
Common flag for Exynos 5410 and 5422
config PLAT_IMX6
bool
default n
help
Common flag for Sabre Lite and Wandboard Quad
config PLAT_IMX7
bool
default n
help
Common flag for iMX7 SoC
choice
prompt "Platform Type"
help
Select the platform for the architecture
config PLAT_KZM
bool "KZM iMX.31 (ARMv6, ARM1136JF-S)"
depends on ARCH_AARCH32
select ARM1136JF_S
select ARCH_ARM_V6
help
Support for the KZM platform
config PLAT_OMAP3
bool "OMAP3 (BeagleBoard, ARMv7a, Cortex A8)"
depends on ARCH_AARCH32
select ARM_CORTEX_A8
select ARCH_ARM_V7A
help
Support for platforms based on OMAP3 SoCs.
config PLAT_AM335X
bool "AM335X (BeagleBone, ARMv7a, Cortex A8)"
depends on ARCH_AARCH32
select ARM_CORTEX_A8
select ARCH_ARM_V7A
help
Support for AM335x platform (BeagleBone).
config PLAT_EXYNOS4
bool "EXYNOS4 (ODROID-X, ARMv7a, Cortex A9)"
depends on ARCH_AARCH32
select ARM_CORTEX_A9
select ARCH_ARM_V7A
help
Support for EXYNOS4 platform (ODROID-X).
config PLAT_EXYNOS5410
bool "EXYNOS5410 (ODROID-XU, ARMv7a, Cortex A15)"
depends on ARCH_AARCH32
select PLAT_EXYNOS54XX
select ARM_CORTEX_A15
select ARCH_ARM_V7A
help
Support for EXYNOS5410 platform (ODROID-XU).
config PLAT_EXYNOS5422
bool "EXYNOS5422 (ODROID-XU3, ARMv7a, Cortex A15)"
depends on ARCH_AARCH32
select PLAT_EXYNOS54XX
select ARM_CORTEX_A15
select ARCH_ARM_V7A
help
Support for EXYNOS5422 platform (ODROID-XU3).
config PLAT_EXYNOS5250
bool "EXYNOS5250 (ARNDALE, ARMv7a, Cortex A15)"
depends on ARCH_AARCH32
select ARM_CORTEX_A15
select ARCH_ARM_V7A
help
Support for EXYNOS5250 platform (ARNDALE).
config PLAT_APQ8064
bool "Qualcomm Snapdrogon S4 APQ8064 (Inforce IFC6410, ARMv7a, Cortex A15)"
depends on ARCH_AARCH32
select ARM_CORTEX_A15
select ARCH_ARM_V7A
help
Support for Qualcomm Snapdragon S4 APQ8064 platforms (Inforce IFC6410).
config PLAT_SABRE
bool "iMX6 (Sabre Lite, ARMv7a, Cortex A9)"
depends on ARCH_AARCH32
select ARM_CORTEX_A9
select ARCH_ARM_V7A
select PLAT_IMX6
help
Support for iMX6 platform (Sabre Lite).
config PLAT_WANDQ
bool "iMX6 (Wandboard Quad, ARMv7a, Cortex A9)"
depends on ARCH_AARCH32
select ARM_CORTEX_A9
select ARCH_ARM_V7A
select PLAT_IMX6
help
Support for iMX6 platform (Wandboard Quad).
config PLAT_IMX7_SABRE
bool "iMX7 (Sabre, ARMv7a, Cortex A7)"
depends on ARCH_AARCH32
select ARM_CORTEX_A7
select ARCH_ARM_V7A
select PLAT_IMX7
help
Support for iMX7 Sabre Dual.
config PLAT_ZYNQ7000
bool "Zynq-7000 (Xilinx ZC706, ARMv7a, Cortex A9)"
depends on ARCH_AARCH32
select ARM_CORTEX_A9
select ARCH_ARM_V7A
help
Support for Xilinx Zynq-7000 platforms.
config PLAT_PC99
bool "PC99"
depends on ARCH_X86
help
Support for PC99 based platform
config PLAT_ALLWINNERA20
bool "ALLWINNERA20 (CUBIETRUCK, ARMv7a, Cortex A15)"
depends on ARCH_AARCH32
select ARM_CORTEX_A15
select ARCH_ARM_V7A
help
Support for ALLWINNERA20 platform (CUBIETRUCK).
config PLAT_TK1
bool "Jetson (Tegra K1, ARMv7a, Cortex A15)"
depends on ARCH_AARCH32
select ARM_CORTEX_A15
select ARCH_ARM_V7A
help
Support for Tegra K1 platform
config PLAT_HIKEY
bool "HiKey (Hi6220, ARMv8a, Cortex A53)"
depends on ARCH_ARM
select ARM_CORTEX_A53
select ARCH_ARM_V8A
select HAVE_FPU if ARCH_AARCH64
help
Support for HiKey platform.
config PLAT_BCM2837
bool "Raspberry Pi 3 (BCM2837, ARMv8a, Cortex A53)"
depends on ARCH_AARCH32
select ARM_CORTEX_A53
select ARCH_ARM_V8A
help
Support for Raspberry PI 3 platform.
config PLAT_TX1
bool "Jetson (Tegra X1, ARMv8a, Cortex A57)"
depends on ARCH_AARCH64
select ARM_CORTEX_A57
select ARCH_ARM_V8A
select HAVE_FPU
help
Support for Tegra X1 platform
endchoice
config ARM_HYPERVISOR_SUPPORT
bool "Build as Hypervisor"
depends on ARM_CORTEX_A15
default n
help
Utilise ARM virtualisation extensions to build the kernel as a hypervisor
config ARM_SMMU
bool "Enable SystemMMU for Tegra K1 SoC"
depends on PLAT_TK1
default n
help
Support for TK1 SoC-specific SystemMMU
source "$KERNEL_PATH/src/arch/arm/Kconfig"
source "$KERNEL_PATH/src/plat/pc99/Kconfig"
endmenu
menu "seL4 System Parameters"
config ROOT_CNODE_SIZE_BITS
range 4 27
int "Root CNode Size (2^n slots)"
default 12
help
The acceptable range is 4-27, based on the kernel-supplied caps.
The root CNode needs at least enough space to contain up to
BI_CAP_DYN_START. Note that in practice your root CNode will need
to be several bits larger than 4 to fit untyped caps and
cannot be 27 bits as it won't fit in memory.
config TIMER_TICK_MS
int "Timer tick period in milliseconds"
default 2
help
The number of milliseconds between timer ticks.
config TIME_SLICE
int "Time slice"
default 5
help
Number of timer ticks until a thread is preempted.
config RETYPE_FAN_OUT_LIMIT
int "Retype fan out limit"
default 256
help
Maximum number of objects that can be created in a single Retype()
invocation.
config MAX_NUM_WORK_UNITS_PER_PREEMPTION
int "Max work units per preemption"
default 100
help
Maximum number of work units (delete/revoke iterations) until
the kernel checks for pending interrupts (and preempts the
currently running syscall if interrupts are pending).
config MAX_NUM_BOOTINFO_UNTYPED_CAPS
int "Max number of bootinfo untyped caps"
default 167
config MAX_RMRR_ENTRIES
int "Max number of RMRR entries to support finding in ACPI"
depends on IOMMU
default 32
help
Sets the maximum number of Reserved Memory Region Reporting
structures we support recording from the ACPI tables
config FASTPATH
bool "Enable fastpath"
default y
help
Enable IPC fastpath
config NUM_DOMAINS
int "Number of domains"
default 1
help
The number of scheduler domains in the system
config DOMAIN_SCHEDULE
string "Domain schedule"
help
A C file providing the symbols ksDomSchedule and
ksDomScheduleLength to be linked with the kernel as a scheduling
configuration.
config NUM_PRIORITIES
int "Number of priority levels"
default 256
range 1 256
help
The number of priority levels per domain
config MAX_NUM_NODES
int "Max number of CPU nodes"
depends on NUM_DOMAINS = 1
range 1 256
default 1
help
The number of CPU cores to boot
config CACHE_LN_SZ
int "Cache line size"
depends on ARCH_X86
default 64
help
Define cache line size for the current architecture
config KERNEL_STACK_BITS
int "Kernel stack size bits"
default 12
help
This describes the log2 size of the kernel stack. Great care should
be taken as there is no guard below the stack so setting this too
small will cause random memory corruption
config FPU_MAX_RESTORES_SINCE_SWITCH
int "Max thread restores without switching FPU"
depends on HAVE_FPU
default 64
help
This option is a heuristic to attempt to detect when the FPU is no
longer in use, allowing the kernel to save the FPU state out so that
the FPU does not have to be enabled/disabled every thread swith. Every
time we restore a thread and there is active FPU state, we increment
this setting and if it exceeds this threshold we switch to the NULL
state.
endmenu
menu "Build Options"
config VERIFICATION_BUILD
bool "Disable verification unfriendly features"
default n
help
When enabled this configuration option prevents the usage of any other options that
would compromise the verification story of the kernel. Enabling this option does NOT
imply you are using a verified kernel.
config DEBUG_BUILD
bool "Enable debug facilities"
depends on !VERIFICATION_BUILD
default y
help
Enable debug facilities (symbols and assertions) in the kernel
config PRINTING
bool "Enable kernel printing"
depends on !VERIFICATION_BUILD
default y if DEBUG_BUILD
help
Allow the kernel to print out messages to the serial console during bootup and execution.
config HARDWARE_DEBUG_API
bool "Enable hardware breakpoint and single-stepping API"
depends on !VERIFICATION_BUILD
default n
help
Builds the kernel with support for a userspace debug API, which can
allows userspace processes to set breakpoints, watchpoints and to
single-step through thread execution.
config ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE
bool "Trap, but don't save/restore VCPUs' CP14 accesses"
depends on ARM_HYPERVISOR_SUPPORT && !VERIFICATION_BUILD
default y
help
This allows us to turn off the save and restore of VCPU threads' CP14
context for performance (or other) reasons, we can just turn them off
and trap them instead, and have the VCPUs' accesses to CP14
intercepted and delivered to the VM Monitor as fault messages.
config IRQ_REPORTING
bool "Report spurious or undelivered IRQs"
depends on PRINTING
default y
help
seL4 does not properly check for and handle spurious interrupts
This can result in unnecessary output from the kernel during
debug builds. If you are CERTAIN these messages are benign
then use this config to turn them off
config COLOUR_PRINTING
bool "Print error messages in colour"
depends on PRINTING
default y
help
In debug mode, seL4 prints diagnostic messages to its serial output
describing, e.g., the cause of system call errors. This setting
determines whether ANSI escape codes are applied to colour code
these error messages. You may wish to disable this setting if your
serial output is redirected to a file or pipe.
config USER_STACK_TRACE_LENGTH
int "Stack trace length"
depends on PRINTING
default 16
help
On a double fault the kernel can try and print out the users stack
to aid debugging. This option determines how many words of stack
should be printed
choice
prompt "Compiler optimisation flag"
default OPTIMISATION_O2
help
Select the compiler optimisation level
config OPTIMISATION_Os
bool "-Os"
help
Compiler optimisations tuned for size
config OPTIMISATION_O0
bool "-O0"
help
No optimisation
config OPTIMISATION_O1
bool "-O1"
help
Basic compiler optimisations
config OPTIMISATION_O2
bool "-O2"
help
Aggressive compiler optimisations
config OPTIMISATION_O3
bool "-O3"
help
Enable all optimisations (may increase code size)
endchoice
config DANGEROUS_CODE_INJECTION
bool "Build kernel with support for executing arbitrary code in protected mode"
depends on !ARM_HYPERVISOR_SUPPORT && !VERIFICATION_BUILD
default n
help
Adds a system call that allows users to specify code to be run in kernel
mode. Useful for profiling.
config DANGEROUS_CODE_INJECTION_ON_UNDEF_INSTR
bool "Make undefined instructions execute code in protected mode"
depends on ARCH_ARM_V6 && !VERIFICATION_BUILD
default n
help
Replaces the undefined instruction handler with a call to a function
pointer in r8. This is an alternative mechanism to the code
injection syscall. On ARMv6 the syscall interferes with the caches
and branch predictor in such a way that it is unsuitable for
benchmarking. This option has no effect on non-ARMv6 platforms.
config DEBUG_DISABLE_L2_CACHE
bool "Disable L2 cache"
depends on ARCH_ARM
default n
help
Do not enable the L2 cache on startup for debugging purposes.
config DEBUG_DISABLE_L1_ICACHE
bool "Disable L1 instruction cache"
depends on ARCH_ARM && DEBUG_DISABLE_L2_CACHE
default n
help
Do not enable the L1 instruction cache on startup for debugging purposes.
config DEBUG_DISABLE_L1_DCACHE
bool "Disable L1 data cache"
depends on ARCH_ARM && DEBUG_DISABLE_L2_CACHE
default n
help
Do not enable the L1 data cache on startup for debugging purposes.
config DEBUG_DISABLE_BRANCH_PREDICTION
bool "Disable branch prediction"
depends on ARCH_ARM
default n
help
Do not enable branch prediction (also called program flow control)
on startup. This makes execution time more deterministic at the
expense of dramatically decreasing performance. Primary use is for
debugging.
config DEBUG_DISABLE_PREFETCHERS
bool "Disable prefetchers"
depends on ARCH_X86 || PLAT_HIKEY
default n
help
On ia32 platforms, this option disables the L2 hardware prefetcher, the L2
adjacent cache line prefetcher, the DCU prefetcher and the DCU IP prefetcher.
On the cortex a53 this disables the L1 Data prefetcher.
config ARM_HIKEY_OUTSTANDING_PREFETCHERS
int "Number of outstanding prefetch allowed"
default 5
range 1 7
depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
help
Cortex A53 has an L1 Data prefetcher. This config options allows
the number of outstanding prefetcher to be set from a number from
1 to 7. Note that a setting of 7 maps to 8 and 5 is the reset value.
config ARM_HIKEY_PREFETCHER_STRIDE
int "Number of strides before prefetcher is triggered"
default 2
range 2 3
depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
help
Number of strides before prefetcher is triggered.
Allowed values are 2 and 3. 2 is the reset value
config ARM_HIKEY_PREFETCHER_NPFSTRM
int "Number of indepedent prefetch streams"
default 2
range 1 4
depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
help
Number of indepedent prefetch streams. Allowed values are 1 to 4.
2 is the reset value
config ARM_HIKEY_PREFETCHER_STBPFDIS
bool "Enable prefetch streams initated by STB access"
default y
depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
help
Enable prefetch streams initated by STB access. Enabled is the reset value
config ARM_HIKEY_PREFETCHER_STBPFRS
bool "Prefetcher to initated on a ReadUnique or ReadShared"
default n
depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
help
Sets prefetcher to initated on a ReadUnique (n) or ReadShared (y)
ReadUnique is the reset value
config ENABLE_BENCHMARKS
bool
default n
config ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
bool
depends on BENCHMARK_TRACK_UTILISATION && ARCH_ARM
default y
config BENCHMARK_USE_KERNEL_LOG_BUFFER
bool
depends on BENCHMARK_TRACK_KERNEL_ENTRIES || BENCHMARK_TRACEPOINTS
default y
choice
prompt "Enable benchmarks"
depends on !VERIFICATION_BUILD
default NO_BENCHMARKS
help
Enable benchamrks including logging and tracing info.
Setting this value > 1 enables a 1MB log buffer and functions for extracting data from it
at user level.
NOTE this is only tested on the sabre and will not work on platforms with < 512mb memory.
This is not fully implemented for x86.
config NO_BENCHMARKS
bool "No benchmarking features enabled"
config BENCHMARK_GENERIC
bool "Enable generic benchmarks"
select ENABLE_BENCHMARKS
help
Enable global benchmarks config variable with no specific features
config BENCHMARK_TRACK_KERNEL_ENTRIES
bool "Keep track of kernel entries"
select ENABLE_BENCHMARKS
help
Log kernel entries information including timing, number of invocations and arguments for
system calls, interrupts, user faults and VM faults.
config BENCHMARK_TRACEPOINTS
bool "Use trace points"
select ENABLE_BENCHMARKS
help
Enable manually inserted tracepoints that the kernel will track time consumed between.
config BENCHMARK_TRACK_UTILISATION
bool "Track threads and kernel utilisation time"
select ENABLE_BENCHMARKS
help
Enable the kernel to track each thread's utilisation time.
endchoice
config MAX_NUM_TRACE_POINTS
int "Maximum number of tracepoints"
depends on BENCHMARK_TRACEPOINTS
default 1
help
Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data,
where k is an integer between 0 and this value - 1.
The maximum number of different trace point identifiers which can be used.
endmenu
menu "Errata"
config ARM_ERRATA_430973
bool "Enable workaround for 430973 Cortex-A8 (r1p0..r1p2) erratum"
depends on ARCH_ARM
depends on ARM_CORTEX_A8
default n
help
Enables a workaround for the 430973 Cortex-A8 (r1p0..r1p2) erratum. Error occurs
if code containing ARM/Thumb interworking branch is replaced by different code
at the same virtual address.
config ARM_ERRATA_773022
bool "Enable workaround for 773022 Cortex-A15 (r0p0..r0p4) erratum"
depends on ARCH_ARM
depends on ARM_CORTEX_A15
default y
help
Enables a workaround for the 773022 Cortex-A15 (r0p0..r0p4) erratum. Error occurs
on rare sequences of instructions and results in the loop buffer delivering
incorrect instructions. The work around is to disable the loop buffer
endmenu