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>
It is an invariant in the MCS kernel that scSporadic implies sc_active.
Make use of that invariant by avoiding an explicit check for sc_active,
but assert the invariant in debug mode so it fails quickly when new
code breaks the invariant.
Essentially reverts 56098195f2 now that the invariant is preserved,
but adjusts the assertion from 17109eb8c9 to actually express
the invariant.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Follow Arm's code where it tries to place traps and vector
code adjacently in a 4KiB page to optimise performance
(through spatial cache locality).
Closes#1091
Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>
The vspace (top level PT) cap had non-standard names which were a bit
confusing to reason about. The name conflict with capPTBasePtr also
spits out fully-qualified names in verification.
This commit updates all the field names of vspace_cap to start with
"capVS" and updates all the call sites.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Clearing the pending state only has an effect if the IRQ state is
active-and-pending, which happens for edge-triggered interrupts if
another edge happens on the IRQ line for the currently active
interrupt. This window is small enough to ignore, at worst user
space will get another notification, which is harmless.
If unnecessary notifications are unwanted, the pending state should
be cleared during seL4_IRQHandler_Ack(), as that covers a much bigger
window. However, edge-triggered interrupts are not expected to happen
often. Making all interrupt handling slightly faster and the code
simpler is the better trade-off.
Reading the GIC config word is very slow for GICv2, see pull #1107.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Verification sees macros as the preprocessed C code. On other arches, we
have checkVPAlignment, but on AArch64 we had IS_PAGE_ALIGNED only. Since
this was the only use, this commit also removes IS_PAGE_ALIGNED in
favour of checkVPAlignment.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For verification purposes, use same arg names as other platforms, and
don't go through `_ptr_set_` from the bitfield generator (same as
RISC-V).
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Verification requires packed C structures for reasoning. While we
previously updated `struct vcpu` to be packed on AArch32, on AArch64
`struct gicVCpuIface` needs extra padding.
This extra padding now aligns a previously un-aligned field on AArch32,
meaning that needs to go away, and the comment there adjusted.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
These were marked DONT_TRANSLATE due to 32-bit `__asm__` blocks which
verification can't handle, which resulted in MODIFIES proofs not being
generated.
This commit adds the obvious MODIFIES proofs for machine ops: nothing
gets modified by reading hardware registers, and writing them only
changes state that isn't in the model.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Enable badged SMC capabilities to be revokable so that dynamic systems
can revoke badged capabilities that are handed out.
Signed-off-by: Kent McLeod <kent@kry10.com>
Provide seL4_BootInfoFrameSize (and seL4_BootInfoFrameBits) for
userland, to there is no longer a need to hard-code the 4 KiByte
assumption.
Signed-off-by: Axel Heider <axelheider@gmx.de>
C parser has issues with `return f(...)` when f's return type is void.
Rephrase `vcpu_hw_write_reg` to look like its AArch32 equivalent, using
`break` in the switch statement.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Verification infrastructure can only handle word-sized variable access
in __asm__ statements. The following functions use 32-bit access on a
64-bit arch and are now marked DONT_TRANSLATE:
* readCIDR
* writeCIDR
* readAFSR0
* writeAFSR0
* readAFSR1
* writeAFSR1
* readESR
* writeESR
* readISR
* vcpu_init_vtcr
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
