This drops subsection for riscv so that subsections for rv32/64
belong to same level as those of x86 and arm32/64.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
Currently, the kernel permits userspace VMMs to enable and use the
VMX-preemption timer by allowing writes to the following VMCS fields:
- VMX_GUEST_PREEMPTION_TIMER_VALUE (count)
- VMX_CONTROL_PIN_EXECUTION_CONTROLS (timer enable bit)
- VMX_CONTROL_EXIT_CONTROLS (save current count on context switch bit)
It also forwards the timer expiry event as a VM exit.
But it does not tell userspace how fast the timer will count down,
making it impossible to use. This commit exposes the timer's scale
via `seL4_X86_VCPU_ReadMSR`.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
- separate the update of the release queue in tcbReleaseEnqueue from
the setting of ksReprogramTimer, so that verification may reason
uniformly abbout the update of the queue.
- use local variables in sendIPC and receiveIPC to avoid repeated
accesses of the heap.
- move the update of the replyTCB field in receiveIPC so that the
updates related to the thread state are grouped together, to more
closely align with the Haskell specification.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
a7 is not changed by seL4_Yield, so the original declaration is correct.
However, in some loops GCC 14.2 may drop the load to a7 if a7 or
memory are not declared as clobbered in the assembly block. This is a
problem if *other* code does write to a7. For some reason GCC 14.2 does
not recognise those other loads. GCC 14.3 and GCC 15 both work as
expected.
The problem manifests in SCHED0011 in sel4test.
This change works around the GCC 14.2 problem because GCC 14.2 is the
standard Debian trixie compiler and it is likely that people will hit
the problem even if we say that GCC 14.2 should not be used.
The workaround uses the same implementation of seL4_Yield as the Arm and
x86/x64 versions do: inline call to sys_null with an empty asm volatile
declaring memory as clobbered. The memory clobber declaration eliminates
the miscompilation, and overall the implementations are now consistent.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When we renamed CHANGES to CHANGES.md, the copyright info from
reuse/dep5 for CHANGES was not transferred.
Remove CHANGES from .reuse/dep5 and add info to CHANGES.md directly.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Fixed incorrect arguments descriptions for X86PageMapEPT, to make it
consistent with other invocations that take an EPT and guest physical
address such as X86EPTPTMap.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
The call to setThreadState within suspend is
moved to the end of the function, in order to
preserve invariants about the queues.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Previously TCB_WriteRegisters/ReadRegisters ignored the count parameter
and unconditionally copied the entire seL4_UserContext, this leads to
unnecessary overhead for VMM operations.
This addresses issue #1085
Signed-off-by: Yifei Zhan <yifei@zhan.science>
For preprocess checks on pull requests, check against the base_ref of
the pull request (e.g. master) instead of against the seL4 revision in
the verification manifest.
If base_ref has advanced over the verification manifest revision, we do
not want to see that difference again on pull requests, but only the
difference the pull request causes itself.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The call to rescheduleRequired within scheduleTCB is performed only when
the scheduler action is ResumeCurrentThread, and therefore will only set
the scheduler action to ChooseNewThread. This removes the call to
rescheduleRequired and replaces it with the direct update to the
scheduler action.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The upstream action in the ci-actions repository has changed slightly
and leaves the PDF in a different location.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Make verification and release builds equal by setting the default for
KernelArmHypEnableVCPUCP14SaveAndRestore to OFF. The option is still
available to set in non-verification builds, only the default changes.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add GIC_VERSION cmake option (default 2) to select between GICv2 and
GICv3 for the qemu-arm-virt platform. GICv3 support requires waking
the redistributor on QEMU and configuring interrupt security grouping
for the hypervisor.
Resolves: seL4/seL4#1170
Signed-off-by: Kent McLeod <kent@kry10.com>
Allow userspace reads to `VMX_CONTROL_SECONDARY_PROCESSOR_CONTROLS`
field of VMCS. seL4 already allow writes to the field so no reason to
not allow reads.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Previously, X86_64_VTX_64BIT_GUESTS forced the VCPU into 64-bit mode by
hardcoding the IA-32e bit in VM-Entry Controls. This prevented userspace
from starting a VCPU in real mode, which break cases where you want the
guest to be able to manage its own mode transitions. Such as booting
an UEFI firmware.
This change allows the guest to manage its own mode transitions
(real -> protected -> long mode). The X86_64_VTX_64BIT_GUESTS config is
now scoped strictly to enabling 64-bit features like MSR access.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Allow userspace reads and writes to `VMX_CONTROL_ENTRY_CONTROLS` field
of VMCS. Which is primarily used for enabling long mode and loading of
certain MSRs on VM Entry. As far as I know this field only controls the
behaviour of the VCPU and would not allow userspace to violate any
kernel properties such as disabling external interrupt exiting or EPT.
The effects of bits in this field are defined in
Chapter 27.8 "VM-ENTRY CONTROL FIELDS" of the
Intel SDM Order Number: 325462-090US February 2026.
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Allow CR0.PE and CR0.PG to be cleared if "Unrestricted Guest" mode is
supported by the host CPU. This mode allows guest software to run in
unpaged protected mode or in real-address mode. From [1] with Indan's
feedback applied.
[1] https://github.com/seL4/seL4/pull/1438
Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>
Co-authored-by: Heyang Zhou <hello@su3.io>
When original.family >= 0xF, the extended model was incorrectly
assigned to ci->display.family instead of ci->display.model. This
matches the Intel implementation and AMD CPUID specification.
Signed-off-by: Weixie Cui <cuiweixie@gmail.com>
Made-with: Cursor
Previously, CMake defaults to adding various flags to the compile
options, such as `-O3`, `-DNDEBUG`, and `-g`. Here is an excerpt from
CMakeCache.txt:
//Flags used by the C compiler during RELEASE builds.
CMAKE_C_FLAGS_RELEASE:STRING=-O3 -DNDEBUG
//Flags used by the C compiler during RELWITHDEBINFO builds.
CMAKE_C_FLAGS_RELWITHDEBINFO:STRING=-O2 -g -DNDEBUG
We instead change the CMAKE_BUILD_TYPE to 'None' so that CMake
doesn't try to be clever and append extra compile flags. Anything
that depends on seL4 will be unaffected as CMake variables are scoped.
This should have no meaningful change to the kernel's generated code,
as the compile flags were being overridden anyway.
Relevant parts of the build.ninja file for comparison:
- Now, `-DRELEASE=ON`:
FLAGS = -march=armv8-a -D__KERNEL_64__ -std=c99 -Wall -Werror
-Wstrict-prototypes -Wmissing-prototypes -Wnested-externs
-Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull
-nostdinc -ffreestanding -fno-stack-protector
-fno-asynchronous-unwind-tables -fno-common -O2 -nostdlib
-fno-pic -fno-pie -mgeneral-regs-only -mno-outline-atomics
-E -CC -I/sel4test-manifest/build/kernel/generated_prune
- Before, `-DRELEASE=ON`:
FLAGS = -march=armv8-a -D__KERNEL_64__ -O3 -DNDEBUG -std=c99 -Wall
-Werror -Wstrict-prototypes -Wmissing-prototypes
-Wnested-externs -Wmissing-declarations -Wundef
-Wpointer-arith -Wno-nonnull -nostdinc -ffreestanding
-fno-stack-protector -fno-asynchronous-unwind-tables
-fno-common -O2 -nostdlib -fno-pic -fno-pie
-mgeneral-regs-only -mno-outline-atomics -E -CC
-I/sel4test-manifest/build/kernel/generated_prune
Note the lack of -O3 -DNDEBUG options.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This was done way back in 2017: 0abc72027, but somehow
was missed from CMakeLists.txt and hyp_traps.S files.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Only call the command on CMake files that may be the first file
evaluated from the project. Remove from all other files.
Signed-off-by: Kent McLeod <kent@kry10.com>
The AArch64 FPU trap helpers were modifying both CPTR_EL2.TFP and
CPTR_EL2.TCPAC when enabling or disabling FPU trapping. However, only
TFP controls trapping of FP/SIMD instructions from EL0/EL1 to EL2.
TCPAC traps accesses to CPACR_EL1 and is unrelated to FPU instruction
execution. Trapping CPACR_EL1 is unnecessary for seL4’s FPU handling
and can interfere with other architectural features that are
controlled via CPACR_EL1.
In particular, CPACR_EL1 is an Architectural Feature Access Control
Register and is not limited to FP/SIMD. For example, Morello uses
CPACR_EL1.CEN to enable CHERI instructions. Trapping CPACR_EL1 via
TCPAC would therefore require special handling or could break guests
that legitimately modify CPACR_EL1 for non-FPU features.
Since seL4 only needs to trap FP/SIMD instructions if FPU is disabled
per TCB/VM, it is sufficient to control CPTR_EL2.TFP alone. Remove the
modification of TCPAC from enableTrapFpu()/disableTrapFpu() and leave
CPACR_EL1 accesses untrapped.
This aligns the implementation with the architectural intent of the
AArch64 FP/SIMD trapping model and avoids assuming that CPACR_EL1 is
used solely for FPU control.
See Issue #1601 for more context and discussion.
Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>
This eases verification by using a local variable
which remains unchanged during execution of the
function.
This preserves semantics since refill_unblock_check
will not modify the tcbSchedContext field of any TCB.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
At the moment, the seL4 microkit does not setup TLS variable
support. The workaround has been to `#define __thread` (blank)
before including `<sel4/sel4.h>` in `<microkit.h>`, which causes
issues if `<microkit.h>` is included *after* `<sel4/sel4.h>`,
often with obscure linker errors to `__emutls_**` symbols.
Instead we add a libsel4 config option that allows us to build
it with __thread copied out. We introduce an LIBSEL4_THREAD_LOCAL
macro in a similar way to the existing LIBSEL4_INLINE macro.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
- Factor out the inline assembly from invokeSMCCall so that it can be
made a separate machine operation in the specification. This part of
the change should produce the same binary as before.
- Parse IPC buffer arguments in decode, not in invoke. This eliminates
the "buffer" argument to the invoke function and keeps argument
processing in decode.
- Use setMR instead of replicating its functionality.
- Reduce decode argument list to the ones that are used.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
No change to behaviour, the commit just makes sure all cases are
explicitly listed instead of falling through to default.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The AArch64 kernel now has verification support for SMC caps. Remove
dependency of KernelAllowSMCCalls on "NOT KernelVerificationBuild" and
set KernelAllowSMCCalls to ON by default for AArch64 verification
builds.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This in particular introduces the function
schedContext_unbindReply, which is used within
finaliseCap, as well as invokeSchedContext_Unbind.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Done in order to ensure overflow does not occur. More
specifically, we call usToTicks on an argument only
when it has been checked to be at most MAX_PERIOD_US,
so that we know that overflow does not occur as a
result of the conversion. We also rephrase the check
on extra_refills. Rather than performing an addition,
which may in extreme cases overflow, we perform a
subtraction, which we know does not underflow, as a
result of our invariants.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Not all platforms are 512-byte aligned. Specifically, 64-bit
platforms are 1024-byte byte aligned.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Try detect if we are running as a guest based on the CPUID
and skip clock_sync_test if we are.
Similar as previous patches for skipping QEMU on ARM/RISC-V
but at run-time instead of build-time.
Tested with qemu-system-x86_64 using `-smp 4`, the test is now
skipped with regular QEMU as well as `-accel kvm`.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
schedContext_donate() is performance critical and should be fast,
but migrateTCB() assumes that there is a change in affinity and
calls fpuRelease() unconditionally, causing unnecessary FPU
saving and restoring.
Signed-off-by: Indan Zupancic <indan@nul.nu>
White space change only:
- left-align sizes within each block declaration
- min 2 spaces to separate field name from size
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
