For ongoing verification of seL4 on AArch64. This config has SMMU and
hypervisor support enabled. AArch64 also implies FPU support is on.
The target board for now is the TX2, which has an SMMU.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove all support for ARMv6 architectures now that all platforms and
CPUs that use this architecture have been removed.
Signed-off-by: Kent McLeod <kent@kry10.com>
Verify that KernelArch and KernelWordSize have been correctly
set after including the platform cmake files.
Signed-off-by: Ben Leslie <benno@brkawy.com>
seL4Config.cmake is responsible for generating a valid
CMAKE_TOOLCHAIN_FILE and setting up platform config options at the start
of the build. The CMAKE_TOOLCHAIN_FILE variable has to be set before the
first cmake `project()` function is processed to take effect.
Previously this file was required to be imported in a CMake script
before the kernel's CMakeLists.txt could be processed. This prevented
the main CMakeLists.txt file from being used without an additional
configuration file:
cmake -G Ninja -C ../configs/ARM_verified.cmake ../
Now it is possible to do:
cmake -G Ninja -DKernelPlatform=imx6 -DKernelARMPlatform=sabre ../
This should make it easier to invoke CMake for building kernel
configurations from other build environments.
Because this file is now imported in the Kernel's CMakeLists.txt
context, there is no longer a requirement to save all the intermediate
settings into the cache and then read them out again.
Signed-off-by: Kent McLeod <kent@kry10.com>
This adds basic support for the ARM Cortex A55 cpu core as is used in
the Amlogic S905x3 that is found in the ODroid C4.
Signed-off-by: Curtis Millar <curtis@curtism.me>
KernelAArch64SErrorIgnore needs to be saved into the cache in
seL4Config.cmake if it is set by any platform's config.cmake.
Signed-off-by: Kent McLeod <kent@kry10.com>
Don't create CONFIG_ARCH_AARCH32 on every platform and architecture.
Remove KernelSel4ArmHypAarch32.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
As this variable bounds both the period and the budget and the period
itself bounds the budget, the name for this variable would be more
appropriately named 'MAX_PERIOD'
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
the function is not always passed the TIMER_PRECISION argument. If it is
not, we should not set the global varaible.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
For RISC-V platforms that do not provide machine instructions to count
leading and trailing zeros, this commit includes more efficient library
functions. For verification, we expose the bodies of the functions to
the proofs.
Kernel config options `CLZ_BUILTIN` and `CTZ_BUILTIN` allow selection of
whether compiler builtin functions should be used. These are only
supported on platforms where the builtin compiles to inline assembly. By
default, the options are on for all platforms except RISC-V.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The A35 core is available on some recent ARMv8 SOCs (such as the
NXP i.MX8X family).
This change enables building for the A35, however no platforms
currently target the A35. It is an enabler for future platform
support additions.
Signed-off-by: Ben Leslie <benno@brkawy.com>
Remove unused cases and add break in switch statements.
Add conditions to sel4arch.xml.
Change guard in capdl printing to correct TK1_SMMU.
Set KernelArmSMMU default to off.
Add types to aarch32 syscall_stub_gen.py.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
Adding the master control caps that are used to create transaction
and context banks caps. This commit includes the internal kernel
structure that required to manage any created transaction and
context bank caps.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
We need to bound the time the user provides to configure scheduling
contexts to avoid malicious or erraneous overflows of the scheduling
math. Make the max period/budget 1 hour.
1 hour is sufficiently small that it will fit in a 32-bit error message.
1 week is sufficiently small for 64-bit platforms.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
Without FORCE being added to `set` in declare_seL4_arch for
KernelSel4Arch, the set command doesn't seem to persist as the variable
must be already initialised in some cases. In this part of the script
processing, a platform has already been selected and is setting its seL4
arch and so using FORCE seems appropriate anyway.
This leverages #!/usr/bin/env -S cmake -P to invoke a cmake
configuration file as a script that configures and builds a kernel in
the current directory with the configuration that was invoked. It is a
quick way for producing a kernel.elf or kernel_all_pp.c input file to
verification for a particular config.
The toolchain file given to CMake is required to be immutable after
first build configuration. CMake caches certain build flags based on
this assumption. We now throw an error if the platform configuration
changes in a way that changes this toolchain file.
If CMAKE_TOOLCHAIN_FILE is unset in seL4Config.cmake then generate one
that selects the correct toolchain based on configured kernel arch
settings.
This means that initialising a build goes from:
`cmake -DCMAKE_TOOLCHAIN_FILE=gcc.cmake -DAARCH32=ON -G Ninja -C
../configs/ARM_verified.cmake ..`
to:
`cmake -G Ninja -C ../configs/ARM_verified.cmake ..`
gcc.cmake is modified to be used as an input to configure_file.
@KernelArch@ and other @@ arguments will be replaced with the
configuration settings. The file will still work if passed directly to
cmake via -DCMAKE_TOOLCHAIN_FILE=gcc.cmake without being templated.
This does not implement the timers for any platforms, but
provides the generic arm arch, and aarch32/aarch64 infrastructure for
tickless timer drivers.
This is the first part of the seL4 MCS. This commit:
* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.
This switches between master and mcs configurations.
This also adds a build system variable KernelPlatformSupportsMCS that
can be used to error on platforms that don't support MCS due to
unimplemented functionality.
The physical address range supported by each aarch64 platform is defined
by which Arm CPUs it has. We therefore configure KernelArmPASizeBits*
based on which CPU is selected.
Correctly defined the macros to translate between virtual and hardware
IRQs such that PPIs can be properly handled on gic_v2. It is now
possible to create a per-core handler for PPIs on platforms using this
GIC.
Allow projects that use the kernel as a subproject to configure the
kernel in -C scripts.
CMake supports providing a script via -C upon first initialisation of a
build directory. This script is expected to populate the configuration
cache for the rest of the build to depend on. This is how standalone
kernel builds are currently configured. However in buildsystems that add
the kernel as a subproject, it was up to the application to modify
configuration properties before or after the kernel was imported. This
lead to circular dependencies where properties were changed by a module
later in the build, but this then invalidated properties that were set
based on the first property's original value. This lead to running CMake
multiple times in order for settings to reach a stable state.
We now assume that most shared system configuration occurs in initial -C
settings evaluation. seL4Config.cmake is a configuration module that the
kernel exports that allows a configuration script to set kernel platform
and architecture settings in a way that doesn't introduce circular
dependencies.
seL4Config can be imported into other configuration files. This should
make it easier for a full system configuration script to query and
configure kernel configuration values without introducing circular
dependencies on configuration properties.
TLS_BASE virtual register is replaced with FS_BASE and GS_BASE virtual
registers.
The FS_BASE and GS_BASE virtual registers are moved to the end of the
context so they need not be considered in the kernel exit and entry
implementation.
Removed tracking of ES, DS, FS, and GS segment selectors on kernel entry
and exit.
ES and DS are clobbered on kernel entry with the RPL 3 selector for a
DPL 3 linear data segment.
FS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with FS_BASE as the base. This is done on exit to reload the value from
the GDT.
GS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with GS_BASE as the base. This is done on exit to reload the value from
the GDT.
Kernel entry and exit code is refactored, simplified, and improved in
light of the above changes.
x64: update verified config to use fsgsbase instr
The verification platform for x64 relies on the fsgsbase instruction.
Instead of processing each platform CMake file during the arch's
config.cmake file, we process all of the platform CMake files first.
This is primarily motivated by wanting to move platform configuration
into a config file that is processed via a -C argument to the initial
build initialisation command.
Now a platform config is responsible for setting the kernel architecture
and it's own platform/arch specific config settings. Where previously a
platform was chosen in an arch specific way via either setting
KernelARMPlatform or KernelX86Sel4Arch or KernelRiscVPlatform, a
platform can now be set by KernelPlatform. In cases where a platform may
further parameterise its configuration it is free to choose its own
config options to query. Platforms that support multiple seL4
architectures should use KernelSel4Arch to query this. Platforms that
provide sub platforms such as exynos5 and subplatforms exynos5250,
exynos5410 and exynos5422 can be selected by specifying
KernelPlatform=exynos5, KernelARMPlatform=exynos5410 for example.
This matches the name with the L4V_ARCH variable in the verification tools and will
allow, as additional configurations are added, selecting the correct configuration
directly based on the configured L4V_ARCH from those tools.
