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>
This reverts commit 3d2ae69f9c:
"ARM/SMP: Re-implement atomic exchange taking sel4 IPI into account"
Also removed riscv's try_arch_atomic_exchange_rlx().
This was added because CAS can take very long to finish on ARM if
the exclusive reservation granule (ERG) is large for the platform,
as any writes on other cores within up to 2Kb could make the CAS
fail.
The correct fix is to add padding around the global lock equal to ERG
to make CAS fast, which would make the extra IPI check redundant.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Compatibility with versions <3.10 is going away.
As it happens, we're not using any CMake features that have changed
between 3.7 and 3.16, so bump the lowest version to 3.16.
Also remove the minimum version statement from the platform config
files --- they're all very simple files that are version independent;
and the version is checked elsewhere anyway.
Also, Fix style issue
A commit to fix style to make the PR go through.
Signed-off-by: Peter Chubb <Peter.Chubb@unsw.edu.au>
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>
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>
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>
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>
getKernelStack() is never called, and readHTPIDRO() was only called in
getKernelStack(). readTPIDRPRW() is only used in hyp configurations.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
On aarch32, single stepping is configured by setting an instruction
breakpoint to mismatch mode. The way that it is checked whether a
given breakpoint is being used as a normal breakpoint or for
single-stepping is by checking if it has been configured to mismatch.
This works because the HW debug API does not currently provide a way
to otherwise configure mismatch breakpoints, but seems like an
unsatisfactory solution. Whether single-stepping is enabled, and
the breakpoint that is being used for it is already stored in the
TCB of a thread, and this commit changes checks related to
single-stepping to use this information instead.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Changing the debug register fields to what they are referred to
as in the ARMv7 and ARMv8 manuals. Mostly a cosmetic change,
but improves clarity.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
This is most likely an artifact from the change of the IPC buffer
handling before v11.0.0, where a thread-local register (tp on RISC-V)
was reserved by the kernel for storing the pointer to the thread's
IPC buffer. Architectures such as aarch64 would set the register
inside Arch_switchToThread() and then not touch the register in
restore_user_context(). When the RISC-V port was up-streamed, it
didn't restore the register with the other registers, but also
didn't restore it in Arch_switchToThread() and so ended up restoring
it right at the end of the restore process.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Axel Heider <axel.heider@codasip.com>
This removes the tcb parameter from schedContext_unbindTCB, which
is unnecessary, since it is always the scTcb of the given sc.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This refactors awaken, providing an inline function for the
while loop condition, and modifying tcbReleaseDequeue to now
perform the entire loop body.
Since tcbReleaseDequeue will perform tcbReleaseRemove on the
head of the release queue, the variable ksReprogram will be set
to true within tcbReleaseRemove, and therefore, we do not need
to set this variable separately within the loop body of awaken.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
When KernelArmDisableWFIWFETraps is disabled (trapping of WFI/WFE is
enabled), the kernel traps WFx instructions from both native and vCPU
threads. This change makes the code in line with the config description.
In any case, there don't exist many use cases for trapping WFx from
native threads vs vCPU threads. Example: kvm uses this to yield physical
CPU time to other vCPUs instead of busy waiting.
Signed-off-by: Andy Bui <andy.bui2001@gmail.com>
Correctly mask the IOAPICVER register to the Maximum Redirection Entry
field to potential avoid spurious higher bits on e.g. AMD processors.
Set IOAPIC_IRQ_LINES to the maximum value this field is allowed to
return (239+1). While our haswell machines report 24 IRQ lines as
expected, the skylake machines report 120.
The only impact should be the size of the ioredtbl_state array.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This introduces library functions for updating the linked lists which
use the tcbSchedNext and tcbSchedPrev pointers of a TCB, and uses these
to perform the updates to the ready queues and the release queue.
In order to accommodate this, ksReleaseQueue is now of type tcb_queue_t.
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The prior behavior would emit ANSI escape codes which set the terminal
foreground color to black bold (`[30;1m`), leaving the default
background color. On many terminals configured with a dark color scheme,
this creates black on black characters, i.e. the output is invisible.
This change moves to a better adapted output, where the output is only
marked as bold (`[1m]`), which works well on all color schemes.
Fixes#1243
Signed-off-by: wucke13 <wucke13@gmail.com>
Check for CONFIG_ENABLE_SMP_SUPPORT instead of checking for the
number in CONFIG_MAX_NUM_NODES. This allows enabling SMP support
with just one node also.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
Previously accessing the ccnt_num_overflows
value using the NODE_STATE macro. In SMP
configurations, this looks for this value
in the system node state, however, it
resides in the cpu arch node state. This should
therefore be accessed using the ARCH_NODE_STATE.
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Add padding to keep vcpu struct packed on 32-bit platforms. This doesn't
change the size on 32-bit platforms, because the compiler would insert
padding itself. It does increase the size of the struct by one word
on 64-bit platforms, but it remains below 2^vcpuBits.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Currently the seL4_VCPUReg enum only defines the seL4_VCPUReg_VMPIDR_EL2
register when the kernel is configured for SMP. This register should be
available for unicore systems too as otherwise a user level VMM is not
able to control the value of MPIDR_EL1 that the guest VM reads.
Signed-off-by: Kent McLeod <kent@kry10.com>
Partially revert commit 70d1a5f792.
Can't include arch/machine.h because that will cause
a circular include dependency.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Current verification model does not include lazy FPU switching, i.e. it
acts as if this function always returns true, so no FPU faults could be
produced. In order to guard against deriving a contradiction, we don't
allow the C parser to translate it.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
- directly test for page PTE types instead of testing for invalid etc.
- remove unnecessary condition `resolve_ret.ptBitsLeft > PAGE_BITS`
(always true).
- reduce bitfield accesses via pointers to make verification easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- The failure condition `resolve_ret.ptBitsLeft > PAGE_BITS` prevented
larger page sizes from being flushed in VSpaceRoot invocations.
Instead of testing for number of bits left to resolve, simply check
the PTE whether it is a page or not.
- reduce bitfield accesses via pointers to make verification a bit
easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
On AArch64, if this is int, we encounter a situation where we can't
prove equivalence with the abstract spec without an extra invariant that
the number of these registers isn't zero (to satisfy 32<->64 bit casts).
Sticking with word size will make sense on both 32 and 64 bit.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Arch_decodeInvocation takes a word_t length and then passes it to
functions that take an unsigned int length. This was OK on 32-bit where
these types are the same, but on 64-bit this is a downcast without a
range check. It isn't clear why this doesn't trip a compiler warning.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The comment that PRECISION is too low when the assert fails was wrong.
PRECISION should have no influence on it.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- make sure the tick count does not underflow
- make sure the tick count does not become 0 in the division, because
a value of 0 stops the timer.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Move the ksCurTime assertions out of setDeadline, because they are not
necessarily true there. Assert ksCurTime in setNextInterrupt instead.
We only know that the deadline being set is at least ksCurTime -
getTimerPrecision(), which can be slightly in the past (ksCurTime is
already slightly in the past, at kernel entry).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previously, a refill would be ready if its head time
was at most getKernelWcetTicks after the current time.
This would mean that refill_unblock_check could
bring a refill's time forward, which violates an
invariant (namely that the time of the last refill
is at most the period from the time of the head refill).
Moreover, since the time to exit the kernel is always
less than the WCET, this might result in us running
a thread whose refill time is in the future, which
seems to violate the timing model.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
