According to Arm documentation, the exception-handling routine
needs to zero the following bits in FPEXC:
DEX, IDF, IXF, UFF, OFF, DZF and IOF
In seL4, the user space fault handler should do this, as the kernel
doesn't know when user space is done handling the FPU trap.
In case of virtualisation, the guest kernel should clear these bits.
Now that the seL4 kernel doesn't handle FPU traps itself any more,
user space can handle asynchronous traps if it wants to.
Signed-off-by: Indan Zupancic <indan@nul.nu>
On 32-bit ARM the fpexc system register is set by loadFpuState,
which includes the FPU enable/disable bit FPEXC_EN_BIT. This
register is part of the usercontext and needs to be initialised
correctly, otherwise the FPU will be disabled by loadFpuState.
Before, this bug was hidden because the FPU was enabled lazily
after a trap. This bug just caused one extra FPU trap at first
FPU use for each task: The first handleFPUFault would fail to
enable the FPU, causing another FPU trap when user space gets
restarted.
On the second FPU fault, switchLocalFpuOwner calls enableFpu first
and then calls saveFpuState because ksActiveFPUState is set to the
current task's FPU state. Then it gets saved with FPEXC_EN_BIT set
and the task can continue with the FPU actually enabled.
This also means that with the old code, the initial FPEXC state
of each task was equal to the previous active FPU task's.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Also release FPU when dissociating a vcpu, otherwise ksCurFPUOwner
may be wrong.
fpuRelease() sets ksCurFPUOwner to NULL, if this happens before
we return to the host, it may end up with the FPU disabled and no
FPU state loaded. Instead of hunting down and handling all obscure
corner cases where this might happen (dissociating vcpus, cross-core
operations), just check for this in vcpu_fpu_to_host().
Signed-off-by: Indan Zupancic <indan@nul.nu>
It's not only used when deleting a thread any more.
Swapping fpuRelease and dissociateVCPUTCB makes no practical
difference as they are independent, but it simplifies
verification slightly.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Add config choice and change the default from XSAVEOPT to XSAVE.
The first config choice is used as the default option. Only XSAVE
is guaranteed to always work, the others require newer CPUs.
Get rid of dubious FPU state headers, we don't need them:
- XCOMP_BV_COMPACTED_FORMAT is set by xsavec or xsaves.
- We can init MXCSR with the ldmxcsr instruction.
Only system state should be configured in IA32_XSS_MSR,
setting FPU user state bits causes an exception.
All memory should be zeroed already, no need to do it again.
See also issue #179.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Trivial change, except for x86 virtualisation and bootup.
Normally the seL4_TCBFlag_fpuDisabled flag is used to decide whether
to enable or disable the FPU. However, with x86 virtualisation there
is only one TCB. Use the task flag for the host and always enable FPU
for the guest.
When either the host or the guest's FPU is loaded, ksCurFPUOwner will
point to our TCB. saveFpuState and loadFpuState check fpu_active and
do the right thing depending on the current FPU user. To make this
work it was necessary to pass tcb_t to saveFpuState and loadFpuState.
Use the idle thread to store the initial FPU state. x86KSnullFpuState
is kept to simplify verification.
However, when Arch_initFpu is called, the idle thread hasn't been
created yet, so move the initialisation to after create_idle_thread,
but before create_initial_thread, as that leads to Arch_initFpuContext
using x86KSnullFpuState.
Also initialise VCPU FPU registers correctly for x86, otherwise the
initial state is wrong and can't be loaded when XSAVES is enabled.
Signed-off-by: Indan Zupancic <indan@nul.nu>
On x86 both the VM monitor as the VM guest have their own FPU state.
The FPU of the monitor is controlled with seL4_TCBFlag_fpuDisabled
TCB flag. For the guest running on the VCPU the FPU will always be
enabled.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Add flags to tcb_t and the seL4_TCBFlag_fpuDisabled flag.
Enums are signed, make TCB flags word_t to make it unsigned.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Retain the ridiculous name to make clear which invocation is being
handled.
Rename tptr to tcb for consistency within the file.
We have a dom_t type, use it as early as possible.
Signed-off-by: Indan Zupancic <indan@nul.nu>
This was removed in 2016 289bf92bf0.
Additionally, 5fac9e8198 removed the
section of the comment regarding having enough room for all the
untyped caps; because otherwise "enough space for 12 caps" is
somewhat uninteresting (most of the cspace is taken up by untypeds).
Signed-off-by: julia <git.ts@trainwit.ch>
As decided at the most recent TSC meeting, bump cmake format to the
latest version. This will change/break style in many of the existing
cmake files, but pinning pyyaml to < 6 is not a long-term option.
Also bump patch version of autopep8, which should not lead to style
changes.
Bump overall sel4-deps version because the cmake-format change is
incompatible. Version 0.6.0 was not published because of the pyyaml
pinning/downgrade.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Migrate documentation of the API docs generation process here from the
docsite where it is too much out of view. Here it is closer to where it
is needed an more likely to get updated when things change.
Compared to the docsite version, this has applied:
- standard wrap column
- markdown lints
- adjusted headings
- `object-api-sel4-arch.xml` etc renames
- include RISC-V in structure
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove manual table of contents for rendering on the docsite, which will
provide an automatic TOC.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When evaluating XML condition expressions, properly treat undefined
values as undefined, not as False. Otherwise, the negation of an
undefined value may make an entire expression true and incorrectly
label some methods as MCS methods.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- introduce arch interface for IRQControlCap dependencies as well as for
isMDBParentOf (Arch_isIRQControlDescendant, Arch_isMDBParentOf). This
mirrors the corresponding interface in the proofs and Haskell and
avoids #ifdef proliferation in generic code.
- Arch_isIRQControlDescendant is currently only used for SGISignalCaps
- Arch_isMDBParentOf is used for SGISignalCaps and SMCCaps
- fix argument checking in Arch_decodeIRQControlInvocation (+ style
tweak)
- Arch_sameObjectAs must return false for SGISignalCaps to align with
finality definition of caps, i.e. SGISignalCaps are always final. This
has no behaviour change, because finality doesn't matter for behaviour
for SGISignalCaps, but we require for the proofs that the concept of
finality aligns with the spec.
- simplify checks for IRQControlCap in sameObjectAs: sameObjectAs can
never be true for IRQControlCap.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Fix a bug in VGIC Maintenance/VPPI logic that allowed a thread to be
simultaneously BlockedOnReply and in the release queue.
Co-authored-by: Alwin Joshy <joshyalwin@gmail.com>
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
set ts-2025 for master branch l4v and leave on ts-2024 for MCS until MCS
is updated to Isabelle2025 as well.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Non-functional change. This will probably affect verification,
so definitely not expecting this to be merged anytime soon.
But it was very weird we had this rootSlot argument mark as UNUSED,
and it took me a bit to realise exactly what excaprefs[0] was
supposed to be.
Signed-off-by: julia <git.ts@trainwit.ch>
We're currently using AWS Arm VMs, and vanilla Isabelle2024 ships a Z3
version that does not work on Arm. Using the ts-2024 branch fixes this
until we have upgraded everything to Isabelle2025.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This fixes the error message in decodeSetTimeoutEndpoint
and correctly updates current_syscall_error.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
We no longer need to check this as the previous commit changed
decodeSetSchedParams to only pass the thread_control_sched_update_sc
flag if these conditions are true.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
The implementation of TCB_SetSchedParams did not follow the API
reference, as it would fail if:
a. The TCB already had a scheduling context, even if this was the same
as the one being passed in.
b. The scheduling context was bound to a TCB, even if this was the TCB
that was invoked.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Before:
- invokeSchedContext_Consumed and invokeSchedContext_YieldTo clobber
the message info field in the reply from kernel, which results in a
length 0 message.
- invokeSchedContext_Consumed and invokeSchedContext_YieldTo may crash
the kernel for read-only IPC buffers
- invokeSchedContext_Consumed and invokeSchedContext_YieldTo generate
a reply from kernel for syscalls that should not generate replies
- completeYieldTo does not set the badge register, which will contain
whatever that previous syscall returned and not correctly indicate
success/failure.
- completeYieldTo sets registers of the current thread, combined with
IPC buffer message registers of potentially another thread.
Instead:
- pass the thread to setConsumed instead of the IPC buffer, so we can
write to the correct registers
- look up the IPC buffer again and check for write authority
- follow the kernel reply protocol, which includes only generating a
message for `call`. This means, we need to pass the flag through from
higher-level decode functions.
- set thread state to Running if a reply message from the kernel was
created, leave on Restart for default empty success message.
- set the badge register
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
