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>
- 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>
Allow SGIs to be generated from non-SMP kernels.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
The outermost if statement can be removed in reply_pop
because reply_pop is called only in reply_remove, which
includes an explicit check for this condition.
The new inline function setThreadStateBlockedOnReply is
used within reply_push.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The SiFive Premier P550 [1] is a new development board from SiFive
that is based on the ESWIN EIC7700X SoC.
The platform is interesting to the seL4 community as it implements
the RISC-V hypervisor extension meaning we now have real hardware to
evaluate RISC-V hypervisor changes to seL4. It also implements the
Sscofpmf extension and so we'll be able to get more experiment with
proper profiling on RISC-V.
Unfortunately, it seems we still do not have proper ASID suppor
according to [2].
The board comes in two configurations, 16GB and 32GB of memory.
This adds support for the 16GB model.
The DTS comes from SiFive's fork of Linux [3].
No modifications were made, any extra things are in the overlay.
[1]: https://www.sifive.com/boards/hifive-premier-p550
[2]: https://forums.sifive.com/t/asid-vmid-support-in-p550-eic7700x/6887
[3]: https://github.com/sifive/riscv-linux/tree/dev/kernel/hifive-premier-p550
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Wrap config_set macro in a static inline function so that verification
automation does not simplify away dead code branches based on it, but
the compiler still does.
In most parts of the proofs we want to pretend that we don't know the
config value yet and consider both options. This makes the proofs more
independent on the config value that is selected.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Save and restore the CNTKCTL register alongside other virtual timer
registers when switching VCPUs.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
This introduces two new constants to the vcpu reg enum, with the goal of
unifying reg range saves/restores and making explicit which registers
are affected.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
seL4_VCPUReg_CPACR was sometimes saved to an inactive current VCPU,
overwriting the previous value and erroneously enabling FPU access.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
In aarch64 kernel configurations, it is not possible to configure the
FPU to be disabled. This makes certain ifdefs redundant.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Moves it to the arm-specific arch data.
Adds an extra CONFIG_HAS_ARM_TLB_LOCK that defaults to ON when the
architecture is ARM_CORTEX_A8.
Again, variable was noticed in the objdump of a RISC-V build, despite
only being used for a specific ARM CortexA8 platform.
Signed-off-by: julia <git.ts@trainwit.ch>
The virtual timer registers managed within a VCPU context are
not saved if written to, if the VCPU in question is disabled. This
results in any updates to the virtual timer registers being
lost/written over when that VCPU is next scheduled and context
switched in.
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is added for completeness, but it's not efficient for userlevel to
deactivate PPI IRQs on different cores than they were received on.
Signed-off-by: Kent McLeod <kent@kry10.com>
Separate priority drop from deactivation so that when the kernel
delegates interrupts to userlevel, they can be left in the active state
until user level performs the ack invocation which deactivates them.
This is more efficient than doing a disable and enable operation
for each handled interrupt as it is core local and doesn't require
sending operations to the GIC distributor..
Signed-off-by: Kent McLeod <kent@kry10.com>
Instead of special handling for the SBI region in the kernel, which can
be platform specific, treat it as a reserved memory region in the device
tree which is sufficient to prevent the kernel from turning the reserved
region into kernel untyped caps.
Signed-off-by: Kent McLeod <kent@kry10.com>
The clock sync test at boot keeps failing for the hifive board with time
deltas as high as 5. We think this is because mmode might be taking a
big lock for reading the time.
Add a macro for allowed delta and set it to a higher value for RISC-V.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Make which user thread ID register used by the kernel for its TLS
operations configurable. Either tpidru or tpidruro can be selected which
map to architecture registers tpidru and tpidruro on aarch32 and
tpidr_el0 and tpirrro_el0 on aarch64.
The default value of this option is tpidru to stay compatible with the
kernel's current behaviour.
Signed-off-by: Kent McLeod <1759184+kent-mcleod@users.noreply.github.com>
Use atomic operations to get and set the IPI pending flag to
ensure that if an IPI is observed, the IPI arguments are also
observed.
Using atomics makes this requirement explicit to the compiler.
Without this change there is a race between setting up an IPI
and another core checking for ipi == 1. This can happen before
IPI_MEM_BARRIER has been executed.
Found by Yanyan Shen.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Align the kernel lock to the exclusive reservation granule size.
Without this nearby writes can delay atomic operations implemented
with looping exclusive load/store instructions for an undefined time.
Cleanup IPI code.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Remove cpu argument from clh_lock_acquire/release, it is never
valid to call them with something else than getCurrentCPUIndex().
Use clh_is_self_in_queue() instead of poking into lock internals
in ipiStallCoreCallback().
Add some comments from the paper to make it easier to match the
implementation with the description in the paper it's based on.
Don't use confusingly different naming, but follow naming from
the paper: Rename 'node' to 'myreq' and 'next' to 'watch', etc.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
