Timer reads go via mmode on RISC-V, and the hifive board regularly fails
the clock sync test at boot because of that.
We could add a larger allowed delta, but the observed values so far are
up to 5us, so it is questionable what we then know after the test if we
do that. Disable for RISC-V instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Verification requires inline assembly blocks to have consistent types.
In gic_v3 files, the `msr` and `mrs` instructions are used both with
uint32_t and uint64_t types, which causes the Isabelle C parser to fail.
According to the Arm GICv3 specification, the registers we are accessing
are all 64 bit registers. Some of them have the top 32 bits reserved as
res0. These are the ones that currently are used with uint32_t,
presumably for consistency with the corresponding gic_v2 functions.
To make the C parser succeed:
- for the SYSTEM_READ_WORD and SYSTEM_WRITE_WORD macros, use word_t or
uint64_t
- for functions that are declared with uint32_t, leave the declaration
intact, but use uint64_t internally for MSR with an explicit cast
to/from uint32_t. This is the behaviour we are assuming the C compiler
to have added implicitly before.
This commit does not change the fact that the gic_v3 virtualisation
functions assume a 64-bit architecture. For AArch32, word_t and uint64_t
may be incorrect.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Since cdbae0b3b2, seL4 has used a
0-indexed naming for the levels of the page tables, starting
from the root (0) and down to the lowest level (2), for
CONFIG_PT_LEVELS=3.
However, the naming of the stored page table was never updated,
leading to a variety of confusing code such as:
kernel_image_level2_dev_pt[RISCV_GET_PT_INDEX(vaddr, 1)] = \
pte_next(paddr, true);
When CONFIG_PT_LEVELS=4, the entries of the level 1 page table
instead point to gigapages (1GiB) instead of megapages (2MiB).
This is the same as the previous behaviour.
Signed-off-by: julia <git.ts@trainwit.ch>
riscv64-linux-gnu- is supposed to be semantically equivalent to
riscv64-unknown-linux-gnu- but the names don't indicate whether the
toolchains have multilib support. At time of this commit,
riscv64-unknown-linux-gnu- is the default name given to the
multilib-capable riscv-toolchian installed via
https://github.com/riscv/riscv-gnu-toolchain.git so leaving it as a
higher priority.
Signed-off-by: Kent McLeod <kent@kry10.com>
This changes the default configuration values of the build options:
KernelRiscvExtF and KernelRiscvExtD from OFF to ON.
The options control whether the kernel will support user applications
that use either of the floating point extensions. When these options are
off, FPU instructions will cause an exception.
Arm and x86 default FPU architecture support to ON and so this change is
making the default option consistent across architectures.
Signed-off-by: Kent McLeod <kent@kry10.com>
Spend a couple minutes trying to decipher a weird
sip encoding until I realised it was in hex.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
The new reusable workflow feature of GitHub allows us to avoid
repeating the workflow definitions and collect them in the ci-actions
repo instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Nowhere else in the documentation uses the phrase
"Must be a depth of 32"
which seems incorrect for 64-bit riscv.
Also, the index parameter had the same description as root, which
is incorrect.
Signed-off-by: julia <git.ts@trainwit.ch>
We no longer guarantee the invariant that the replyObject reference is
NULL when the thread state is not BlockedOnReceive or BlockedOnReply.
It is likely that this invariant was true in the kernel so far, but
proving it would require a new proof that the reference is already NULL
for any setThreadState to a simple state like Running, Inactive,
Restart. This either means reasoning about the state the thread had
before setThreadSate, or explicitly setting the reference to NULL more
often.
There are many of these setThreadState instances, and the benefit of
maintaining the invariant is low. Not maintaining the invariant removes
some state updates from low-level functions (called often) at the cost
of adding some if-checks in higher-level functions (called less often).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Right now the `platform_gen.json` and `platform_gen.yaml` files contain
regions that are not actually used by the kernel. This is fine for
`platform_gen.h` because they are guarded by #ifdefs with kernel config
defines but the same approach does not work for YAML and JSON.
So, this patch changes the Python scripts that generate this files so
that they only generate the regions that actually end up being used.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Presumably, this was copied from the common_arm.lds linker script,
but it was a particular implementation detail of the arm32 code,
and is unneeded on RISC-V.
Signed-off-by: julia <git.ts@trainwit.ch>
These are never supposed to happen.
Note, that this will still use the kernel stack to save the registers
and so if page tables are corrupted, it will continually fault near the
trap_entry. But this is reasonably easy to tell from a debugger.
Not all traps will be handled via the s-mode trap handler; it depends on
the value of the `medeleg` register. This appears to default to 0xf0b509
(in QEMU) and so we can catch page faults.
Without this, traps in the kernel will be attributed to a trap of the
current running thread.
Previously, some kernel modifications that corrupted memory caused:
```
Caught cap fault in send phase at address 0
while trying to handle:
vm fault on data at address 0 with status ��7
in thread ��ffffffff8401bc00 "idle_thread" at address 0
With stack:
Invalid vspace
```
Now, the kernel prints out:
```
KERNEL ABORT (exception within s-mode)!
scause: 0xf, stval: 0x0
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 2, Invocation tag: 1
```
Signed-off-by: julia <git.ts@trainwit.ch>
On aarch64, clang interprets the compile option -mgeneral-regs-only
as disabling all FPU-related registers and instructions, which not
only include those generated by the compiler (which is how gcc would
interpret this option), but also those in (inline) assemblies written
explicitly by the programmer, which gcc does not forbid with this
option. This commit enables FPU-related registers and instruction
explicitly in the FPU-context switching code, so the kernel will build
under clang-18 on aarch64. The commit that changed the behaviour
between clang-17 and clang-18 is eabffc7 of the LLVM project.
Signed-off-by: Liu, Chang <cl91tp@gmail.com>
Presumably intended to be something like
typedef enum IRQConstants { ... } platform_interrupt_t;
this instead declares a symbol that is exported and kept in the
binary, but is never used. Remove it.
Spotted as my kernel.elf binary contained a strange symbol:
ffffffff8401b7f0 g O .bss 0000000000000004 platform_interrupt_t
Signed-off-by: julia <git.ts@trainwit.ch>
The previous commit 05858be didn't actually add it to both instances
of the if/else statement, and so doesn't actually work in all cases
(e.g. with `../init-build.sh`).
Signed-off-by: julia <git.ts@trainwit.ch>
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>
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>
