9f99e77c38
This commit adds support for saving/restoring an additional register that exists on ARM MPCore platforms. As this register is user wrieable, as well as readable, it must saved and restored by the kernel to prevent gross information channels.
633 lines
19 KiB
Text
633 lines
19 KiB
Text
#
|
|
# 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 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
|
|
|
|
menu "seL4 System"
|
|
|
|
choice
|
|
prompt "Architecture Type"
|
|
default ARCH_X86
|
|
help
|
|
Select the architecture seL4 will be running on.
|
|
|
|
config ARCH_X86
|
|
bool "x86"
|
|
|
|
config ARCH_ARM
|
|
bool "ARM"
|
|
endchoice
|
|
|
|
config ARCH_X86_64
|
|
bool "64-bit kernel"
|
|
default n
|
|
depends on ARCH_X86
|
|
|
|
config ARCH_IA32
|
|
bool
|
|
default y if !ARCH_X86_64 && ARCH_X86
|
|
|
|
config ARCH_AARCH32
|
|
bool
|
|
default y if 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_ARM
|
|
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_ARM
|
|
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_ARM
|
|
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_ARM
|
|
select ARM_CORTEX_A9
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for EXYNOS4 platform (ODROID-X).
|
|
|
|
config PLAT_EXYNOS5410
|
|
bool "EXYNOS5410 (ODROID-XU, ARMv7a, Cortex A15)"
|
|
select PLAT_EXYNOS54XX
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A15
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for EXYNOS5410 platform (ODROID-XU).
|
|
|
|
config PLAT_EXYNOS5422
|
|
bool "EXYNOS5422 (ODROID-XU3, ARMv7a, Cortex A15)"
|
|
select PLAT_EXYNOS54XX
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A15
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for EXYNOS5422 platform (ODROID-XU3).
|
|
|
|
config PLAT_EXYNOS5250
|
|
bool "EXYNOS5250 (ARNDALE, ARMv7a, Cortex A15)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A15
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for EXYNOS5250 platform (ARNDALE).
|
|
|
|
config PLAT_APQ8064
|
|
bool "Qualcomm Snapdrogon S4 APQ8064 (Inforce IFC6410, ARMv7a, Cortex A15)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A15
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for Qualcomm Snapdragon S4 APQ8064 platforms (Inforce IFC6410).
|
|
|
|
config PLAT_SABRE
|
|
bool "iMX6 (Sabre Lite, ARMv7a, Cortex A9)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A9
|
|
select ARCH_ARM_V7A
|
|
select PLAT_IMX6
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for iMX6 platform (Sabre Lite).
|
|
|
|
config PLAT_WANDQ
|
|
bool "iMX6 (Wandboard Quad, ARMv7a, Cortex A9)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A9
|
|
select ARCH_ARM_V7A
|
|
select PLAT_IMX6
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for iMX6 platform (Wandboard Quad).
|
|
|
|
config PLAT_IMX7_SABRE
|
|
bool "iMX7 (Sabre, ARMv7a, Cortex A7)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A7
|
|
select ARCH_ARM_V7A
|
|
select PLAT_IMX7
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for iMX7 Sabre Dual.
|
|
|
|
config PLAT_ZYNQ7000
|
|
bool "Zynq-7000 (Xilinx ZC706, ARMv7a, Cortex A9)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A9
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
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_ARM
|
|
select ARM_CORTEX_A15
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for ALLWINNERA20 platform (CUBIETRUCK).
|
|
|
|
config PLAT_TK1
|
|
bool "Jetson (Tegra K1, ARMv7a, Cortex A15)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A15
|
|
select ARCH_ARM_V7A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for Tegra K1 platform
|
|
|
|
config PLAT_HIKEY
|
|
bool "HiKey (ARMv8a, Cortex A57)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A57
|
|
select ARCH_ARM_V8A
|
|
select ARCH_ARM_MPCORE
|
|
help
|
|
Support for HiKey platform.
|
|
|
|
config PLAT_BCM2837
|
|
bool "Raspberry Pi 3 (BCM2837, ARMv7a, Cortex A53)"
|
|
depends on ARCH_ARM
|
|
select ARM_CORTEX_A53
|
|
select ARCH_ARM_V7A
|
|
help
|
|
Support for Raspberry PI 3 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"
|
|
default 64
|
|
help
|
|
Define cache line size for the current architecture
|
|
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 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_IA32
|
|
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.
|
|
Currently unimplemented on other platforms.
|
|
|
|
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
|