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>
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>
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>
Eliminate #ifdefs for BF_CANONICAL_RANGE in bitfield specifications,
using the new field_ptr command. Use word_size expressions for some of
the padding fields to make clearer where the sizes come from.
The transformations in this commit are written to produce exactly
identical output for code and proofs. In some rare cases, padding
could in the future be rearranged to make more use of field_ptr, but
these edits would create code differences and are left for later.
It may now also be to share more blocks between generic 32 and 64
definitions if they only reference word_size. This is also left for
later to reduce noise.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Doing an ISB is very expensive, about ~30 cycles on some CPUs,
so try to avoid them if possible.
For the writes to (most) system registers to be observed, a
'Context Synchronization event' needs to occur (see ARM DDI 0487
M.a §D24.1.2.2 / pD24-8367).
The kernel is not doing any FPU operations after disabling the FPU,
so there is never a need for an ISB there. Returning to user space
counts as a 'Context Synchronization event' and ensures the FPU enable
or disable has completed when user space starts executing.
An ISB after enabling the FPU is only needed in case the FPU was
disabled for the kernel and the kernel wants to do FPU operations
like saving or restoring the FPU state. The ISB ensures that the
FPU enable system register write is finished before FPU using
instructions are executed.
For Aarch64 non-HYP it is possible to disable the FPU for user space
(EL0), but keep it enabled for the kernel (EL1). This is done by
setting CPACR_EL1.FPEN to 1, which the code actually already did.
Aarch64 with virtualisation enabled is more complicated and needs
higher level changes to achieve the same, which aren't done here,
the change is limited to removing the ISB in disableFpu().
This partially fixes issue #1569.
Signed-off-by: Indan Zupancic <indan@nul.nu>
This will sometimes fail when using QEMU RISC-V virt
with multiple cores, make the behaviour consistent as
QEMU ARM virt.
Given that QEMU is not intended to be a cycle accurate
simulator, I imagine that is why this does not reliably
succeed.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Otherwise it is not possible to send SGIs to all cores on platforms
with non-contiguous Affinity values or more than 16 cores.
16 is the limit of the target list, which is only relevant when
sending an SGI to multiple targets at once.
Update the API documentation to reflect what's actually happening.
Signed-off-by: Indan Zupancic <indan@nul.nu>
The compile error for exposing vcpu_t could be easily fixed, the real
issue is the functions not existing when HYP is disabled.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This reverts https://github.com/seL4/seL4/pull/1490 as the
change that was made in that PR was reading the wrong part
of the GIC specification, because ARM decided that the
register layouts are different in non-secure vs secure mode.
Fixes (again) https://github.com/seL4/seL4/issues/1489
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
These diagrams were really unclear and confusing to me,
especially as I always needed to convert from "2^64 - 2^39"
form to "0x0000008000000000" form many times in my head.
They were also out of date and wrong, containing graphics of the
PDPT (from x86) as well as TLB bitmaps.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Move setIRQTrigger from <arch>/hardware.h into interrupt.h together
with the rest of the IRQ interface, because it is now a visible
interface even for platforms and architectures that do not provide the
functionality.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide a default dummy implementation for setIRQTrigger even for
non-GIC platforms where this operation is not supported. Otherwise,
the function is declared in the header, but has no implementation.
Implementing it as UNREACHABLE() means verification will show that the
function is not called.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Adding a spec with precondition False means verification has to show
that the function is not called.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide an implementation of the header function plat_SGITargetValid
even for non-GIC platforms. This function will not be called, but
verification has a general lemma about it, and the default
implementation makes that lemma true without adding special cases.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
There's a few cases in the kernel where the ksKernelEntry tracking
is not perfect, such as in SError reporting, and (I believe) a few
other places which I haven't tracked down to a cause - but some of
e.g. the RISC-V trap code where the first entry faults and the 2nd
proceeds can report stale information.
In these cases, the kernel says that the entry was via a certain
syscall or interrupt (etc), even though that was clearly not the
case because we know the kernel exited. Now we will print out this:
halting...
Kernel entry via Unknown (0)
The changes:
- When exiting the kernel, via `c_exit_hook()`, reset
`ksKernelEntry.path` to "Unknown".
An alternative here would have been add a global "valid" boolean
to the kernel state, but this requires modifying every site where
we set the ksKernelEntry.path to also set valid = true, which is
ugly.
- Remove Entry_UnimplementedDevice from entry_type_t as it is never
used, to leave enough room to add Entry_Unknown.
- Switch out the CONFIG_DEBUG_BUILD || BENCHMARK TRACK ENTRIES #if
in the x86 breakpoint code with the more concise
`TRACK_KERNEL_ENTRIES` define used elsewhere.
Signed-off-by: julia <git.ts@trainwit.ch>
Similar to #510 but for all other platforms. The idle_thread runs
without a stack and so cannot handle the stack prologue. This should
hopefully make the kernel rely less on FORCE_INLINE for this as well.
We create idle.S assembly files for each platform, as GCC does not
support `__attribute__((naked))` on AArch64 (GCC 13.2.0) and bails out.
Signed-off-by: julia <git.ts@trainwit.ch>
Helps the C compiler to recognise irqInvalid as a constant. This in
turn helps with binary verification, because irqInvalid is already
parsed as a constant in Isabelle since it is never written to.
See also the discussion in #1349 and #1324
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The GIC platforms use irq_t for irqInvalid -- bring remaining AArch32
platforms in line with that.
irq_t is an unsigned type (when it is an integer) and enum constants are
signed. For the proofs to treat these platforms uniformly, they need to
be the same kind. They can't all be enums, because irq_t can be a more
complex type for SMP platforms.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Also, change the definition of ASID_HIGH from
((a >> asidLowBits) & MASK(asidHighBits))
to
((a) >> asidLowBits)
because the mask is an unnecessary operation (this is handled by the
proofs). It is unnecessary because these (SW) ASIDs are kernel-only
and are never exposed to users, so they will never set bits asid from
the asidLow and asidHigh bits.
Signed-off-by: julia <git.ts@trainwit.ch>
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>
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>
Remove fault-based FPU state saving and loading.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
