This directory-scoped varible is now used by config_option,
config_choice and config_string to set a created CMake cache variable as
advanced or not. An advanced variable is hidden by default in the CMake
configuration editors. Setting SEL4_CONFIG_DEFAULT_ADVANCED to ON will
cause variables to be advanced and not show up in the cache. Projects
can set this to limit the amount of options presented in the
config editor. Any cache variable can have this overridden by calling
mark_as_advanced(CLEAR config_name)
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.
On aarch64 physBase is the constant that points to the bottom of
physical memory (RAM).
Prior to this change the kernel window was mapped directly to physBase,
which is usually not a 0 paddr. As a consequence the kernel could not
access any memory below physBase.
This change fixes this issue by mapping the start of the kernel window
to 0 in the physical address space.
- add new constant PADDR_LOAD, the location of the kernel image in the
physical address space.
- add new constant PADDR_BASE, the start of the physical address space
(0).
- add new constant KERNEL_ELF_BASE, the location of the kernel image in
kernel virtual memory.
A consequence of this change is that on aarch64, the kernelBase constant
now points to the start of the kernel window in virtual memory, but
*not* to the start of the kernel image as these are now different.
Prior to this commit this check would fail on ARMv8.2 and greater, as
having a bit set after this version does not imply that FPU/SIMD is not
supported.
For ARMv8.2 and above the values of the AdvSIMD/FP bits in
ID_AA64PFR0_EL1 are as follows:
- 0b1111 means FPU/SIMD is not supported.
- 0b0000 means FPU/SIMD is supported except for half-precision floating
point arithmetic.
- 0b0001 means FPU/SIMD is supported including half-precision floating
point arithmetic.
In the pip namespace, 'pyaml' is "pretty-yaml", a YAML generator (but
not a YAML parser); 'pyyaml' (accessed with "import yaml"), a.k.a.
"PyYAML", is the YAML serialiser and reader we actually use.
Bump the minor version number per semantic versioning rules. (One could
argue that we are "removing" pyaml (pretty-yaml) from our interface and
therefore a major version bump is required, but we weren't _actually_
using that module so I would argue that the introduction of 'pyyaml' is
the visible change.)
Thanks to Japheth Lim for identifying this issue.
The `shoehorn` tool in tools/seL4 (the sel4_tools repository) requires
this.
Bump minor version number per semantic versioning rules (interface
extension). (0.3.1 instead of 0.3.0 because 0.3.0 saw the light of day
with an incorrect dependency on `libarchive` instead of `libarchive-c`.)
This reverts commit a14264336c.
There are (at least) 3 namespaces relevant to Python module names:
Debian package names, PyPI module names, and the name of a module used
by actual Python language imports. That's one more than my brain could
handle. I wanted "libarchive-c" in setup.py instead of "libarchive".
Make sure that when the kernel boots a scheduling control cap is created
and that the initial thread and idle thread are scheduled using correct
systemt time.
mcs requires an additional 2 registers for performing system calls to
pass information regarding the reply capability and the destination of a
nbsend/recv.
If the time is being read in 32-bit mode it is read in two operations
between which the time can change. If the time causes the low bits to
roll over to 0 and the high bits to increment between reading the low
and high bits an incorrect time will be returned.
A check is added to ensure that an accurate time is returned.
The `shoehorn` tool in the tools/seL4 (the sel4_tools repository) will
require this in a future commit.
Bump minor version number per semantic versioning rules (interface
extension).
Use the __ASSEMBLER__ macro to suppress C definitions from appearing in
non-C files when the preprocessor is used. Other libsel4/*/constants.h
files use this strategy to avoid duplicating definitions for seL4 object
sizes that can changed based on kernel configuration.
Preemption can be triggered due to a revoke operation, which may have
deleted one or both of the current thread and current scheduling
context. Don't manipulate the current thread if it is no longer valid
and just charge the SC iff it is valid and the thread is not.
This was discovered during verification.
ChargeBudget can be called after a preemption, but the preemption may
have deleted the scheduling context. Do not charge scheduling contexts
that have been deleted (check scRefillMax).
Preemption can be via the timer interrupt. In this case we need to
update the timestamp so we can reprogram the timer for the next timeout
and guarantee it is in the future, otherwise we will end up setting a
timeout in the past.
Prior to this change calling yieldTo on an sc with a thread that was not
in the scheduler and had an insufficient/unready head replenishment
would be added incorrectly to the scheduler.
If the thread isn't in the scheduler, use schedcontext_resume to ensure
that it is in the release queue if it has an insufficient/unready head
replenishment, and thus prevent that thread from being added to the
scheduler.
If the scheduling context is changed on the currently running thread
this causes issues if the operation triggers a preemption. This change
makes the proofs easier, and also makes sense for the api, as users
wishing to suspend the current thread should just use Suspend.
A fault message is an IPC. Threads which have faulted can be inactive,
blocked on send, or blocked on reply. Always clear tcbFault when
cancelling IPC to make sure restarted threads are not in a fault state.
Some invocations contain two phases, and certain operations cannot be
allowed to run in the first phase as it could effect the currently
running thread and result in an invalid system state for the second
phase. This change filters those invocations, preventing them from being
used in the first phase of a two-phase, blocking system call.
If we're in a scenario where do_call or fault is set, but there is no
reply, the calling/faulting thread needs to be set to inactive to
prevent it reentering the scheduler in a bad state. If the reply is set,
then the calling/faulting thread is set to blocked on reply correctly.
If a thread's fault endpoint has been deleted, such that cancelAllIPC is
called on that endpoint, set the thread state to inactive. This prevents
threads with faults from entering the run queue and makes the
behaviour consistent with threads faulting without a fault handler set.
This came up as verification now need the invariant that threads in the
runqueue have no faulted, an invariant not required before MCS.
Previously the behaviour was not broken, as threads would just refault
and be made inactive at that point.
Schedcontext_bind is currently called in ThreadControl, which
manipulates capabilities which in turn can result in KsSchedulerAction
being deleted. This means that we cannot use possibleSwitchTo in this
function.
This is a stop-gap fix for verification, the long term fix is to split
setting scheduling parameters from ThreadControl, then we can return to
a direct switch, and also do a direct switch for other thread/scheduler
settings like priorities.
When setting a thread priority, we need to check if it is in the
scheduler before putting it back in the scheduler, otherwise we do not
know enough about the scheduling context to know that the thread is
active.
Rather than preserving the chain break it completely. This changes the
semantics such that if a reply is removed in the middle of a call
chain, a donated scheduling context cannot return to the original
caller.
When yieldingTo a same prio thread, the same prio thread should run
first, not the current thread. Due to changes to possibleSwitchTo in
master scheduler this code became outdated and the current thread would
be rescheduled immediately.
The desired behaviour is that the thread being yieldedTo should be at
the head of the scheduler queue for its priority, and the current thread
should be just after it.
We use the chargeBudget logic in the kernel on seL4_Yield to free up
the budget available in the head refill, however this
updates scConsumed. Given this is a simulated charge (the thread is
yielding the budget, not actually using it), this is incorrect.
