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>
Put MCS-only invocations into their own groups and files. This solves
the problem that doxygen gets confused by duplicate function names with
the same parameters.
MCS/non-MCS is distinguished by evaluating the <condition> field in the
API XML definition. If the condition evaluates to true when
CONFIG_KERNEL_MCS is set, it is an MCS-only method, otherwise it is
assumed to be non-MCS or present in both configs.
Fixes#558
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Disambiguate (for the reader) between normal and mcs versions of
SetSpace in the manual. This does not yet solve doxygen confusion.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
HTML_TIMESTAMP and LATEX_TIMESTAMP have been removed in more recent
doxygen versions. Since we are using the defaults, they are safe to
remove in our config file.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Different API groups may contain the same function name, for instance
IRQ_Control GetTrigger for RISC-V vs the same for ARM. Duplicate
function names with identical parameter lists confuse doxygen, leading
it to generate a single merged xml entry for both, which means one of
the entires will be missing and the other will be potentially wrong.
When the functions are placed in different files and different groups
at the same time, doxygen no longer is confused in all cases.
Therefore:
- generate a separate file for each API group
- generate a separate file group_defs.h that contains group definitions
and declares group nesting
Unfortunately, this does not seem to always work (e.g. the toplevel
MCS/non-MCS syscalls), so manual inspection is still necessary when
adding new calls and separate doxygen runs for duplicate function names
may be necessary. Generating separate files as above enables this
option, should it become necessary in the future.
Fixes#530
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Explicitly select xml parser (instead of html) via "lxml-xml" in
BeatifulSoup to avoid warning.
Signed-off-by: Gerwin Klein <gerwin.klein@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>
Make sure the invariant "sc_sporadic implies sc_active" is preserved by
invalid SchedContexts as well.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Change the statement ordering such that the "sc_sporadic implies
sc_active" invariant is not violated. In the previous code order, the
scSporadic flag is set while the scheduling context is still
potentially inactive. Setting the flag later avoids temporarily
breaking the invariant.
Move the badge setting together with the flag to keep these heap
updates together.
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>
This commit fixes a linking error when using LLVM's lld.
llvm-as doesn't assume or assign section flags for input section if
not specified. This will make the section non-allocatable and put
into a none segment and trigger relocation linking errors against
symbols in non-allocatble sections.
For example, when building with LLVM/lld for AArch64, the following
error occurs:
(traps.S.obj:(function arm_vector_table: .vectors+0x0): has non-ABS
relocation R_AARCH64_JUMP26 against symbol 'invalid_vector_entry')
This does not happen with ld.bfd (GNU's linker) as it seems to allow
relocations against symbols in non-allocatable sections.
The GNU's assembler documentation states that:
"If no flags are specified, the default flags depend upon the
section name. If the section name is not recognized, the default
will be for the section to have none of the above flags: it will
not be allocated in memory, nor writable, nor executable.
The section will contain data. [1]"
This commit explicitly sets .section flags in assembly to avoid
this error and for better intentionality (and good practice)
without relying on toolchains handling flags and linkage differently.
[1] https://sourceware.org/binutils/docs/as/Section.html
Sponsored by: DARPA.
Signed-off-by: Hesham Almatary <hesham.almatary@cl.cam.ac.uk>
gen_config.h files are no longer generated at build time rather than
configure time. This is a return to the behavior of the last release.
Remove mention of the temporary change.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Commit 6d439a4646, which added JSON configuration output, caused the
configuration headers to be generated at build-time instead of
configure-time. This broke CAmkES build systems which depend on
configuration headers in CAmkES files at configure-time.
This commit makes the configuration headers available at configure-time.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
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, don't go through `_ptr_set_` from the
bitfield generator (same as RISC-V).
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>
Report the vspace cap (1) as invalid, instead of the frame cap (0) in
decodeARMFrameInvocation to stay consistent with the other
architectures.
See also #1075
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
These proofs are currently still in progress (unfinished), but already
check large parts of the kernel and can break when the MCS preprocess
check fails.
Signed-off-by: Gerwin Klein <gerwin.klein@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>
`makeUserPage` was a bit confusing to understand, and went around the
bitfield-generator's back by modifying the tag bits. As a result, it did
not set bit 58 for 4k pages, meaning a 4k page could not be identified
from an encoded PTE. This version addresses that, and hopefully improves
the repetition.
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>
This change was missing from the rename of the pgd cap
to vspace cap on aarch64. Allows vm fault fastpath enabled
configs to build.
Signed-off-by: Dan Shea <danshea00@gmail.com>
- Describe the SMP lock variable mechanism detail.
- Add checks that the lock state is valid, this will catch potential
kernel loader problems.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
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>
Make a few changes to follow the syscall message passing convention:
- Confirm with a static assert that NUM_SMC_REGS >= n_msgRegisters.
- Require the input length to be >= NUM_SMC_REGS. This ensures that any
accesses to the IPC buffer memory is safe (if the IPC buffer isn't
present then the message length will be truncated to n_msgRegisters).
- If the call parameter isn't set then the kernel isn't supposed to
reply to the invoking thread. This means no updates to it's registers.
- Set the ThreadState to ThreadState_Running so that the default empty
success message isn't applied at kernel exit (which overwrites
msgInfoRegister)
Signed-off-by: Kent McLeod <kent@kry10.com>
The exec spec typically requires that invocations have a decode phase
that can fail followed by an invoke phase that can not fail.
A switch block is not required when there is only a single valid
invocation label.
Signed-off-by: Kent McLeod <kent@kry10.com>
