This refactors refill_budget_check and schedule_used to
ease verification by limiting heap access via refill_head
and refill_tail, and providing (inlined) named functions
for both the condition and bodies of the loops.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The settings KernelArmVtimerUpdateVOffset and
KernelArmDisableWFIWFETraps should be project settings, not platform
settings, and the values set here are not required for the platform to
work -- they just provide a different default.
Setting these in platform configs could lead to inconsistent project
builds when switching between platforms.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The default python version changes on ubuntu-24, which breaks the
version of cmake-format we are currently using.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Reflect the slow timer read on this platform by increasing the value
for TIMER_PRECISION.
MCS+SMP+debug tests have been failing the clock sync boot test (see
also issue #1053). The proposed fix, which was to make reading the
timer faster, only works for certain OpenSBI versions and is not
enabled by default.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Current TCB_PTR_CTE_PTR assumes that thread blocks are aligned at
BIT(seL4_TCBBits). However the idle thread blocks are aligned
differently at BIT(TCB_SIZE_BITS), thus TCB_PTR_CTE_PTR cannot be
used for idle threads.
This changes idle thread alignment to be consistent with standard
TCBs. Even though macros like TCB_PTR_CTE_PTR should not be used
for idle thread, verification assumes consistent alignment for all
TCBs.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
Multiple versions of GCC were unable to determine that these variables
in decodeX86PortInvocation are initialized in all cases.
Oddly, this compilation failure was only observed with -O1. Compilation
with -O2 was not failing.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The increment and reserve here is not an issue, but to keep
consistency with the change made in 291af86 we should remove it.
See PR #1317 for more info
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
In cases where the kernel is passed a very fragmented map of
available memory (specifically when booting from GRUB on x86),
it is possible for multiple available regions to overlap with
a single reserved region.
Currently, if there is an overlap
(where avail_reg[a].start >= reserved[r].start), the available
region is trimmed and the region index is incremented. This causes
any other overlapping regions to be handled as if they are
non-overlapping, since it's now looking at the next reserved region.
This eventually leads to reserved memory being passed to the root
task and can cause corruption issues if it is used.
It is fine to skip this index increment, since the available region
is now either empty or non-overlapping, and both cases are already
trivially handled.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
This adds `seL4_CapSMC` to table 9.1 and updates section 9.1 so
that to be in line with latest upstream code.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
With recent proof improvements the proofs now apply to further platforms
in the ARM and AARCH64 configurations.
Refactor the verified configs to build on one include file per major
architecture which is then used for each platform with potentially
modified settings. Add path argument to `cmake_script_build_kernel`
macro to accommodate inclusion from different locations in the file
system.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Do not perform cache flushing in clearMemory. Instead flush the cache
only for those object types where it is necessary, and only when the
object is retyped, not when the untyped cap is reset.
This reduces overall need for flushing and delays it to the point of
use. This should speed up boot time significantly, but may impact WCET,
because the largest flush is now the largest page size (e.g. 24) instead
of CONFIG_RESET_CHUNK_BITS (8). The user could already request a flush
of the largest page size before, though, so it this may not actually
impact WCET. Remains to be investigated.
Why this is safe:
- Flushing is only necessary for objects that are seen by other parts of
the system, not for kernel-internal object. These objects are
non-device frames (including IOMMU pages) and page tables. All other
objects are only read/written by the kernel. Frames need to be flushed
to RAM (as clearMemory did), because they could be seen uncached by
devices. Page tables only to PoU for the page table walker.
- Before createNewObject in retype, these objects do not exist and
cannot be seen by any part of the system. createNewObject is the point
where new objects can become visible to the user.
- Theoretically, we could defer flushing further to the point where
frames or page tables are mapped, but it is more complex to track
whether a flush has already happened when they are mapped multiple
times, whereas at retype the object cannot have been flushed already.
- The original implementation, before clearing memory was moved into
reset untyped, also flushed at the same points.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This factors out code from cancelAllIPC and cancelBadgedSends
by introducing the inline function restart_thread_if_no_fault
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Make str_to_long more defensive against malformed content, since this
function runs on user (cmd line) input on x86. The input is from boot
time, i.e. trusted, but the function should still be memory safe.
This change does not fix overflow issues which may still lead to
undefined behaviour.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
getKernelStack() is never called, and readHTPIDRO() was only called in
getKernelStack(). readTPIDRPRW() is only used in hyp configurations.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We relied on str.removeprefix(), which is only available in
python >= 3.9. To make this script more portable, we add our
own implementation.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
This configuration is not in CI (hence why it lead to
a build error in the first place) so I just tested
it locally via sel4test with:
```
../init-build.sh -DPLATFORM=qemu-riscv-virt \
-DMCS=1 -DKernelRiscvExtD=1 \
-DKernelRiscvExtF=1 -DRISCV32=1
```
and it passed.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This eases verification by using a local variable
which remains unchanged during execution of the
function.
This preserves semantics since tcbSchedDequeue
will not modify the scTcb field of the given sc.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
On aarch32, single stepping is configured by setting an instruction
breakpoint to mismatch mode. The way that it is checked whether a
given breakpoint is being used as a normal breakpoint or for
single-stepping is by checking if it has been configured to mismatch.
This works because the HW debug API does not currently provide a way
to otherwise configure mismatch breakpoints, but seems like an
unsatisfactory solution. Whether single-stepping is enabled, and
the breakpoint that is being used for it is already stored in the
TCB of a thread, and this commit changes checks related to
single-stepping to use this information instead.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Changing the debug register fields to what they are referred to
as in the ARMv7 and ARMv8 manuals. Mostly a cosmetic change,
but improves clarity.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
This is most likely an artifact from the change of the IPC buffer
handling before v11.0.0, where a thread-local register (tp on RISC-V)
was reserved by the kernel for storing the pointer to the thread's
IPC buffer. Architectures such as aarch64 would set the register
inside Arch_switchToThread() and then not touch the register in
restore_user_context(). When the RISC-V port was up-streamed, it
didn't restore the register with the other registers, but also
didn't restore it in Arch_switchToThread() and so ended up restoring
it right at the end of the restore process.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Axel Heider <axel.heider@codasip.com>
This removes the tcb parameter from schedContext_unbindTCB, which
is unnecessary, since it is always the scTcb of the given sc.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This refactors awaken, providing an inline function for the
while loop condition, and modifying tcbReleaseDequeue to now
perform the entire loop body.
Since tcbReleaseDequeue will perform tcbReleaseRemove on the
head of the release queue, the variable ksReprogram will be set
to true within tcbReleaseRemove, and therefore, we do not need
to set this variable separately within the loop body of awaken.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
