There are platforms/archs that don't support the Kernel Hardware Debug
API and they can now advertise that by setting
KernelHardwareDebugAPIUnsupported.
This prevents accidental declaration of properties or configurations
that are for the incorrect architecture selected. This was previously
required as the variables KernelWordSize and KernelArch were defined in
each arch specific cmake.config file. Now that they are defined in
advance it is possible to exclude the other imports.
This does not implement the timers for any platforms, but
provides the generic arm arch, and aarch32/aarch64 infrastructure for
tickless timer drivers.
This changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.
seL4_SchedControl_Configure now takes microseconds, not ticks.
This commit is plat-independant - the platform and arch specific
timer code follows in later commits.
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.
Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
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.
Some platforms and configurations do not allow user code to change the
value of the register used for TLS. On these architectures a syscall can
be used to allow the kernel to update the register on their behalf.
This does not immediately update the value in the user context on many
configurations as the values are only stored in the user context on a
context switch.
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.
The DTS compilation was arm platforms only. Moving it to the top level
config file, making it available to RISCV platforms. The generated files
are almost identical with minor differences. A new argument(--arch) is
added to the hardware_gen.py for the differences.
The previous minimum (4) was actually too small to fit more than 1
capability, which would not allow the kernel to boot. A 4K minimum means
on 32-bit, an 8 size is the minimum (256 slots) and on 64-bit, 7 (128
slots).
In addition to being a more practical minimum, this also allows for
simplification of the boot code for future commits.
Introduces a kernel option that, when enabled, reduces the kernel window in a user address
space to just be Static Kernel Image and Microstate (SKIM), instead of the full kernel
address space. This isolates the important kernel data from the user preventing a
Meltdown style attack being able to violate secrecy. The kernel text and read only data,
i.e. anything that is static from boot, is not secret and can be allowed in the SKIM window
and potentially read by the user. Additionally to switch to and from the actual kernel
address space a small amount of state needs to also be in the SKIM window.
This is only an implementation for x86-64, although the same design is applicable to ia32
TOPLEVELTYPES is not intended to be configurable by the user, rather is a reflection
on the types defined by the source. This changes the TOPLEVELTYPES argument to be
a property, allowing it to be constructed as a generator expression when generating
BF files. By being a property, and not something like a global property, it removes
the need to ensure that additions to TOPLEVELTYPES are done prior to any bitfield
target definitions.
Defines an empty custom target whose purpose is to hold properties and configuration
data that can be retrieved using generator expressions in the build phase.
Using the `INTERNAL` attribute implied `FORCE` overriding any value the user may have set
for these. This was not the intention, and they should merely set a `CACHE` value if one
does not already exist.
