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>
Add helper functions to get kernel image location. This removes any
dependencies from the rest of the code on symbols and defines. It
also avoid passing a parameter though various functions.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Currently getting the timestamp for RISC-V platforms uses the
`rdtime` pseudo-instruction which ends up invoking OpenSBI
and then accessing the CLINT memory-mapped `mtime` register.
This patch eliminates the use of `rdtime` in favour of
directly getting the timestamp for performance.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Now the vspace_cap is used for all vspace roots and all other page
tables are referred to by page table caps.
Signed-off-by: Kent McLeod <kent@kry10.com>
Remove the pde_t type and replace all usages with pte_t.
This doesn't remove the page directory cap type yet. Now the page
directory cap refers to a table of pte_t entries and is treated the same
as the object that a page table cap refers to.
Signed-off-by: Kent McLeod <kent@kry10.com>
This first commit only handles 4k pages.
4k pages are mapped using level 3 descriptor formats which annoyingly
have an opposite type definition (bit[1]) from all other levels. At all
other levels, a bit value of 0 is page and 1 is table. At level 3, a bit
value of 1 is page (and there is no bit value for a table).
This prevents us from using a single tagged-union type definition for
all page table descriptor definitions. For now we treat 4k pages as
special and try and push on ahead with the single type definition
anyway.
Signed-off-by: Kent McLeod <kent@kry10.com>
Guard the new implementation of 64-bit x86 guests behind a config
option. This is done so that existing projects that use x86_64 hosts
with ia32-bit guests can continue to be supported until either the old
feature is preferred to be deprecated, or support can be added to
support both simmultaneously.
Signed-off-by: Kent McLeod <kent@kry10.com>
This commit combines a number of smaller commits which do the following:
* Enter IA-32e mode when running a 64-bit host
* Handle additional general purpose registers in 64-bit mode
* Handle 64-bit specific MSR events
* Properly save and restore FS, GS, and Shadow GS registers
CCDC-GVSC DISTRIBUTION A. Approved for public release; distribution
unlimited. OPSEC#4481.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
__builtin_offsetof is not part of the verification C subset -- avoid
accidental use by not declaring a macro for it and filter out the
single use by explicitly marking it as invisible to verification.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Prefer compile_assert over _Static_assert. The latter is only available
in C11, and the verification demands C99.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Enable the timer only at initialization and since it is always
enabled. It is not needed to be re-enabled.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
Generic Timer IRQs are level-sensitive, when the CNT_TVAL
is updated the trigger condition is de-asserted and the
change is propagated to the GIC in a finite time to clear
the pending state.
However, we have to make sure the timer deasserts before
EOIR/DIR, otherwise the interrupt happens again. Therefore,
we need an isb() to cause the timer to de-assert before EOIR/DIR.
There is also a chance of spurious IRQ. A spurious IRQ can be
generated, in the case we have a level-sensitive IRQ, and its
pending state is cleared at device-level but not yet propagated
to the GIC. In between the IRQ deactivation and IRQ ack of the
new interrupt if the requested change from the timer gets propagated
then it causes a spurious IRQ.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
In the interest of stability and not breaking
things, the value of VMReadOnly remains the same.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Add a config option, KernelAArch64UserCacheEnable, that enables user
level access to DC CVAU, DC CIVAC, DC CVAC, and IC IVAU which are cache
maintenance operations for the data caches and instruction caches
underlying Normal memory and also access to the read-only cache-type
register CTR_EL0 that provides cache type information. The ArmV8-A
architecture allows access from EL0 as fast cache maintenance operations
improves DMA performance in user-level device drivers.
These instructions are a subset of the available cache maintenance
instructions as they can only address lines by virtual address (VA).
They also require that the VA provided referrs to a valid mapping
with at least read permissions. This corresponds to lines that the
EL0 could already affect via regular operation and so it's not expected
to break any cache-partitioning scheme.
The config option allows this policy to be selected for a particular
kernel configuration, but it is default enabled as this has been the
existing behavior for current aarch64,hyp configurations and have not
been explicitly disabled in non-hyp configurations.
Signed-off-by: Kent McLeod <kent@kry10.com>
- dmb() no longer works for GICv3, and consequently
a stronger barrier like dsb() has to be used. A weaker
variant of dsb is used to ensure the observability of
complete stores in the same inner-shareable domain.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
- "When an address translation instruction is executed,
explicit synchronization is required to guarantee the
result is visible to subsequent direct reads of PAR_EL1."
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
GICD_IROUTERn is at the offset 0x6100 for SPI 32.
SGIs and PPIs do not have a target since they are private to CPUs.
Signed-off-by: JorgeMVP <jorgepereira89@gmail.com>
Add compile time checks for conditions on physBase that are necessary
for verification of multikernel builds to succeed -- if these fail, the
proofs will fail.
If these succeed, and nothing else has changed compared to a verified
kernel other than physBase, then the proofs will succeed. This does not
mean that all platform requirements are validated, it just means that
all requirements for the proofs to be consistent are met.
The conditions correspond to those in
spec/machine/*/Arch_Kernel_Config_Lemmas.thy
in the verification repository.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Mention that it can be Ok for regions to overflow. State explicitly
that the end is exclusive.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This fastpath optimizes the performance of VM faults in
seL4. It is heavily based on the existing seL4_Call
fastpath and includes the addition of fastpathing replies
to faulted threads in the seL4_ReplyRecv fastpath.
Currently only supported only implemented for aarch64.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
For verification flexible w.r.t kernel placement in physical memory, we
need to relate physBase as a named constant to its abstract equivalent.
Unfortunately, apart from enums, the C programming language does not
have real constants. The C parser follows the C standard and requires
enums constants to be storable as int, meaning without major overhaul
enums are not sufficient for storing word_t-sized memory addresses.
Since the linker scripts can't deal with static inline functions
in the constants they need (KERNEL_ELF_BASE and KERNEL_ELF_PADDR_BASE),
we provide the following preprocessor definitions for the linker
specifically:
* PHYS_BASE_RAW (the numerical value returned by physBase())
* KERNEL_ELF_BASE_RAW
* KERNEL_ELF_PADDR_BASE_RAW
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
On the ZCU102 Rocketchip instantiation, the PLIC is available required
to use hardware peripherals like a UART
Signed-off-by: Chris Guikema <chris.guikema@dornerworks.com>
The thread context structure layout is explicitly designed to have the
register context first, as this simplifies saving the user context on
entry in assembly code. On the exit path there is no need to hard-code
this assumption, stick to the semantics and leave details to the
compiler.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
The signal fastpath aims to optimize the
seL4_Signal operation. In this commit, it is
implemented for MCS AARCH64 (SMP and non-SMP).
The fastpath does not include the case where
signaling results in a higher priority thread
being unblocked and made available for
scheduling (on any core). It does not
fastpath the case where the signaled thread
is donated a scheduling context and has its
FPU state saved in the FPU of a core.
Co-authored-by: Shane Kadish <shane.kadish@csiro.au>
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Remove the return value from configure_sched_context(), because it never
fails. As a consequence, create_idle_thread() also never fails and does
not need a return value.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
Because ksCurTime is compared cross-node now, time across
nodes must be the same. Check this once during boot.
Replace __atomic_signal_fence with the more correct
__atomic_thread_fence, as ksNumCPUs will be changed
cross-node.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Remove the now unused core argument from refill_new and replace all
REFILL_NEW calls with direct calls.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
The code using ksCurTime assumes that ksCurTime is up-to-date,
but this assumption is wrong for ksCurTime of other CPU cores.
Those can be quite some time in the past.
The implications of using NODE_STATE(ksCurTime) is that clocks
on all cores must be synchronous:
- Riscv is okay: The specification states: "The real-time clocks
of all hardware threads in a single user application should be
synchronized to within one tick of the real-time clock."
- x86 okay if not ancient when Invariant TSC is supported.
- aarch64 is okay.
- arm32: arm_global.h is okay. Exynos timer seems okay. am335x and
omap3430 are single-core.
See also #854.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Use the thread passed as parameter instead of making assumption that
this is in sync with the global state.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
- explicitly mention the parameter to make macro less obscure.
- add brackets to make the expression an atom.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
The pointer to a reply object, if any, can be accessed
via the replyObject in the thread state
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
At least some server-class Skylake processors use 0x55 as
their model ID.
These are Skylake X processors.
Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>
The kernel expects object sizes to be powers of two for size and
alignment computations.
- add missing padding for MCS 64-bit configurations for notifications
(other configs were already fine)
- add missing padding for reply object struct
- strengthen compile time assertion to catch discrepancies in the
future.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The messageinfo register is set to 0 after processing a kernel object
invocation if the invocation set the thread state to restart. This is a
problem if the kernel object invocation had also set the message info
register.
The existing convention in this case is for the kernel invocation to
set the thread state to running right before it returns to avoid the
problematic code path. However, there are some invocations that do not
follow this convention and their message info register gets clobbered.
There are also some invocations that set message registers without
setting the message info register at all, or that do not guard their
message register updates with a call parameter.
This commit fixes these issues modulo setConsumed, which we defer to a
later point.
Co-authored-by: Jimmy Brush <code@jimmah.com>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
For a VM fault in a hypervisor context, 32-bit Arm translated the IP
address into an IPA, while 64-bit Arm did not. The previous commit
made these consistent by performing the translation on both.
After investigation and discussion, the 32-bit Arm behaviour was
declared a bug: reporting an IPA (instead of a VA) to the VMM is not
very useful and can cause issues when the fault message is not sent
immediately (SELFOUR-1602). This commit, therefore, removes all stage 1
translation from Arch_setMRs_fault on Arm platforms.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit introduces `addressTranslateS1` to be used on Arm platforms
with hypervisor enabled for stage 1 (vaddr to IPA) translation. On
AArch32 this is a rename from `addressTranslateS1CPR`, and on AArch64 it
wraps `ats1e1r`. This changes the ABI on AArch64 to report faulting
address as IPA.
Reasoning:
With hypervisor enabled, AArch64 defined `addressTranslateS1CPR` to do
nothing, while AArch32 defined it to do stage 1 translation. This
delivered VM faults to the user with the faulting address being either
an IPA or a vaddr depending on mode. This inconsistency is undesireable.
This commit proposes adjusting the inconsistency to match AArch32
behaviour, as it is one of the verified platforms.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For ARM currently TIMER_PRECISION exists, but that is in microseconds
and not fine-grained enough.
This is needed to make periodic tasks synchronous with the system clock.
If this value is zero every period will be extended with the overhead of
taking an interrupt and reading the system clock. To avoid this drift,
the configured value should be set to at least the average overhead.
See also issue #844.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
sysexit requires a 64-bit operand to remain in 64-bit mode when
switching to user level. gcc versions older than 12 encode this as
"REX.W SYSEXIT" while clang encodes this as "SYSEXITQ". Both compilers
don't support the alternate encoding. We instead use ".byte
0x48,0x0F,0x35" which is the actual opcode of the required instruction
which will work with both compilers.
Signed-off-by: Kent McLeod <kent@kry10.com>
seL4_UserTop must be defined to be > 0xC0000000 when the kernel is in
hyp mode due to assumptions made by the kernel init code.
Signed-off-by: Kent McLeod <kent@kry10.com>
Accessing the hyp mode SPSR register via the banked instruction syntax
is UNPREDICTABLE if hyp is the current mode. The direct syntax needs to
be used instead. This is documented in the ARMv7 Architecture reference
manual.
Signed-off-by: Kent McLeod <kent@kry10.com>
CPSR.AIF already presented in HCR_COMMON macro,
And HCR_NATIVE includes HCR_COMMON, then no need
To set CPSR.AIF bit again
Signed-off-by: Cao Jianlong <caojianlong@outlook.com>
The latest code updates introduced CONFIG_ENABLE_KERNEL_LOG_BUFFER
meanwhile other code and config.cmake keeps using
CONFIG_KERNEL_LOG_BUFFER
Signed-off-by: Nataliya Korovkina <malus.brandywine@gmail.com>
Now that there is no need to reserve page table entries in each VSpace
object, the full architecture specified address space range is usable.
Signed-off-by: Kent McLeod <kent@kry10.com>
Each vspace object has a count of how many SMMUv2 context banks are
bound to it. This attribute is moved out of a reserved page table entry
slot into the asid_map_t structure.
This also reduces the width of the MappedCB field from 12 to 8 bits
which is large enough to hold the maximum number of CBs allowed by the
SMMUv2 spec (128). This conserves otherwise wasted bits.
Signed-off-by: Kent McLeod <kent@kry10.com>
When switching to the new thread, it's VSpace must have a valid ASID
mapping. This means that the ASID in the vspace cap must resolve to the
same vspace object as the vspace cap does. In addition, when the VSpace
object is for a stage 2 translation there must be a currently assigned
hardware VMID for the vspace. Otherwise the slowpath must be taken.
Once these checks are done, the TTBR registers can be directly updated
without needing to perform another ASID translation.
Signed-off-by: Kent McLeod <kent@kry10.com>
This stores the 8-bit vmid in the ASID map rather than in a
slot of the virtual address space root for hypervisor configurations.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Kent McLeod <kent@kry10.com>
This uses the asid_map bitfield from x86 for aarch64 to map from ASID to
a given address space.
This will allow for alternate mappings from ASIDs in the future as well
as moving small amounts of metadata into the the ASID table itself.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Kent McLeod <kent@kry10.com>
This is not supposed to happen, thus printing the value gives a bit more
insight what might have happened here.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Put the parameter in brackets to ensure it is an atom. This makes the
macro work as expected in corner cases like ARRAY_SIZE(foo + 3) also.
Signed-off-by: Axel Heider <axelheider@gmx.de>
When building seL4 on a host whose default encoding is not UTF-8,
tools/bitfield_gen.py complains, as with the following log from
Python 3.6 on a Ubuntu 18.04 host says:
Traceback (most recent call last):
File "tools/bitfield_gen.py",
line 2773, in <module>
string = f.read()
File "/usr/lib/python3.6/encodings/ascii.py", line 26, in decode
return codecs.ascii_decode(input, self.errors)[0]
UnicodeDecodeError: 'ascii' codec can't decode byte 0xc2 in position
607543: ordinal not in range(128)
As the Python 3 doc for open() [1] says the default encoding is
platform dependent, such build error may happen on some hosts.
We can either updating tools/bitfield_gen.py to call open() with
an explicit encoding="utf-8" parameter, or avoiding UTF-8 characters
in the source codes.
After inspecting the two places in current source tree that use UTF-8
characters, none of them is absolutely necessary. Let's convert them
to ASCII characters.
[1] https://docs.python.org/3.6/library/functions.html#open
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>
In `vcpu_enable` and `vcpu_disable`, use `setHCR` to wrap setting
REG_HCR_EL2 (similar to AArch32).
Reorder `vcpu_enable` to match AArch32 operation order for easier proof.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Since hardware.h is shared with assembler code, it's better to avoid
having C ode in there. This also aligns the RISC-V port with the ARM
port, where machine.h contains the special register wrapper functions.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Factoring out the benchmark syscall handling in dedicated functions
improves code readability and maintainability.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Explicitly include the config header file as the first thing, don't rely
on other headers doing this eventually.
Signed-off-by: Axel Heider <axelheider@gmx.de>
When calling chargeBudget or commitTime, only consume time within the SC
refills if the SC does not belong to the idle thread. This is to make it
easier to prove that the idle thread is always runable, even if it has
just consumed its SC's current timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Defined to be equal to CONFIG_NUM_DOMAINS. seL4 makes control-flow
decisions based on whether the number of domains is greater than 1. To
perform refinement proofs independent of the number of domains, we need
to follow both branches of these if statements, pretending we don't know
which branch will be taken. This is made significantly harder when
preprocessed C code ends up with comparisons like `if (16 > 1)`.
By adding a numDomains that appears in the C code, we obtain a name we
can point to and link up to higher level specifications.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
It seems all Cortex-A7, Cortex-A15, Cortex-A53 boards require to
flush to coherency in order to get it work.
It is a temporary fix, and we will keep track on this issue.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
The getMaxUsToTicks function is supposed to return maximum
amount of time you can pass to usToTicks without overflow,
but in RISC-V implementation it returns ticks instead. This
patch corrects it so it's implementation is akin to those in
other platforms.
Signed-off-by: Marcin Witkowski <mwitkowski@antmicro.com>
Hide the actual SBI call parameter details of the legacy API and remove
the pointer parameters in the higher code layers. This is a preparation
step for switching to the newer SBI API.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Since uint32_t and uint64_t are used, stdint.h needs to be included.
- Improve comments about GCC/LLVM internals.
Co-authored-by: Matthew Brecknell <matthew@brecknell.net>
Signed-off-by: Axel Heider <axelheider@gmx.de>
The memory mapping for the timer only uses 1K on AllwinnerA20, but
the minimum device mapping is 4K in seL4. Other devices within this
4K page (CCU and PIO) cannot be accessed in the userland.
Replace the kernel timer with the ARM generic timer on AllwinnerA20,
and remove the implementation for AllwinnerA20 specific timer in the
kernel. So we should have user access to those devices now.
Signed-off-by: Luca (Wei) Chen <wei@cvluca.com>
32-bit architectures have to share a small 4GiB address space between
privileged and non-privileged modes. Picking the address to split the
address space at affects how much virtual memory userlevel can use, and
how much physical memory the kernel can turn into untypeds. This is
something that should be configurable policy as different divisions make
sense for different applications. For now we only add the config
option to qemu-arm-virt to try it out before potentially adding it to
all 32-bit platforms.
Signed-off-by: Kent McLeod <kent@kry10.com>
The function Arch_finaliseInterrupt() is empty now and can be removed as
it serves no purpose any longer. There has never been a guarantee that
it gets only called due to kernel entry caused by an interrupt. Instead,
getActiveIRQ() is called in various places of the kernel to check if
there is a pending interrupt. There is a guarantee that the generic
kernel code calls ackInterrupt() within the same kernel entry call
path eventually, when it has finished processing this interrupt. Any
architecture or platform specific cleanup can be done there is this is
necessary.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
PC99 is the only platform that uses Arch_finaliseInterrupt() instead of
ackInterrupt(). There seem no reason for this, thus the code is moved
from Arch_finaliseInterrupt() to ackInterrupt() now.
Arch_finaliseInterrupt() is empty now, but still kept, because it is
part of the proofs and provides a hook that might be useful one day.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
On aarch64 in EL2, there aren't any addresses after 2^48 and so the
any kernel device untypeds that have very large physical addresses could
potentially move into an invalid address range when translated to a
Kernel window PPTR address when being stored in a cap slot. The kernel
in EL2 doesn't need to share its address space with user level and so we
can make the kernel window start low enough that we can't get overflows.
We start from the second entry in the top level page table so that we
don't conflict with any setup code running in the lowest 512GiB of
virtual addresses.
Signed-off-by: Kent McLeod <kent@kry10.com>
CONFIG_DEBUG_BUILD and CONFIG_PRINTING are different config options that
can be used independently from each other. CONFIG_PRINTING controls the
backend of kernel print functions while CONFIG_DEBUG_BUILD controls
other kernel debug features.
Note that CONFIG_VERIFICATION_BUILD is the config option that controls
whether any of these options can be used.
Signed-off-by: Kent McLeod <kent@kry10.com>
- KernelGlobalsFrame caused the definition of seL4_GlobalsFrame which
was a reservation at the top of the user address space on ARMv6
platforms.
- KernelDangerousCodeInjectionOnUndefInstr was used to implement calling
user code in kernel mode won ARMv6.
Signed-off-by: Kent McLeod <kent@kry10.com>
Remove all support for ARMv6 architectures now that all platforms and
CPUs that use this architecture have been removed.
Signed-off-by: Kent McLeod <kent@kry10.com>
The platform was the original verification target of seL4 over 10 years
ago and by now there doesn't appear to be any ways to obtain new
hardware.
Currently, the KZM platform is the only ARMv6 platform and supporting it
requires a few work-arounds for emulating mechanisms that newer hardware
supports. Removing this platform also implies removing armv6 support
soon.
Signed-off-by: Kent McLeod <kent@kry10.com>
Moving the type checks avoid the need for conditional compilation. This
also allows simplifying some include file dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Use SMP_TERNARY() macro.
- Rename get_hart_id() to plic_get_current_hart_id(), as this is just a
helper function for the other PLIC code in this file.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
RISC-V defines the concept of a PLIC, but leaves the details open. The
driver is for the PLIC of the SiFive U54/U74 SOC, which is used on
the HiFive Unleashed/Unmatched and Polarfire board.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- describe PLIC behavior and corner cases.
- provide a common header file for the API.
- add a dummy PLIC driver for spike.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Move CSR SIE access wrappers to generic code.
- Move CSR SIE/SIP bit constants to header file.
- Rename CSR SIE/SIP bit constants to use the names from the RISC-V
specification.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
MODE_RESERVED is unused on RISC-V, so remove it from the code base. It
can be brought back when needed based on the state of the ARM
implementation, which has been clean up to remove global dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- define NUM_RESERVED_REGIONS to align ARM and RSIC-V code
- add runtime checks to catch errors. These checks can't be static or
use assert(), as the parameters are passed by a kernel loader. They
must be considered dynamic and can potentially change any time out
of the kernel's control.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Update GIC_VCPU_MAX_NUM_LR constant to reflect that only 16 list
registers are supported on GICv3. The kernel still reads the actual
number of supported list registers out of the GICH_VTR register so the
kernel would still do the right thing before this change.
Signed-off-by: Kent McLeod <kent@kry10.com>
This adds sufficient kernel support for the GICv3 interrupt controller
to be used in a virtualization context on aarch64.
This set of changes has some limitations, however it is still an
improvement on the status quo.
Limitations:
1: This only provides support for aarch64. Anyone wanting support
for aarch32 + GICv3 + virtualization would need to add additional
code.
2: This code only supports 32 priority levels. Support for more
than 32 priority requires changing the get/set_gic_vcpu_ctrl_apr
interface. This is feasible, but requires a more invasive set of
changes. 32 priority levels has been shown to be sufficient in
practise.
Impacts on verification:
This set of changes should only impact Aarch64 Hypervisor
configurations. This is not yet verified so should not have
an impact on verification.
Level of testing:
This has been tested on an iMX8QXP based board. Testing
has at this point in time been limited to a single virtual
machine.
Note: support for this board is not yet upstrea, but is
currently being prepared.
Explanation of changes:
Ideally a new config item would not be required and this
could be driven purely by DTS and hardware.yml configuration.
However, the structures.bf requires changes. This can only
deal with config.h header files, not other more complex
header files. As such it was necessary to introduce a config
item which can be used for this purpose.
The appropriate platforms (as determined by examination of
DTS files) have been updated with the appropriate config
setting. This config setting only has any relevance if
hypervisor mode is already enabled, so should not cause
any difficulty for existing code or configuration.
Note: No testing has been performed on the updated
platforms.
There may be alternative factorings of this, which could
be considered in future work.
Signed-off-by: Ben Leslie <benno@brkawy.com>
- The field 'slot_pos_max' from 'ndks_boot' is not needed, the value
stored there is the constant BIT(CONFIG_ROOT_CNODE_SIZE_BITS).
- Improve the error message if the limit has been reached
Signed-off-by: Axel Heider <axelheider@gmx.de>
The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This removes the operations that trigger a reschedule or reprogram the
timer from `preemptionPoint` to ensure the relevant state updates in
the proof occur where they are easier to verify.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The L2 cache handling functions were copied from the ARM code in the
initial port, but they are not used on RISC-V. Remove them from the
code base, they can be brought back if a platform has an L2 cache that
needs to be maintained.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
Turns out the invariant 17109eb8c9 refers to is hard to prove
because it is not true, and the runtime check is necessary. This
assertion fails in sel4test SCHED_CONTEXT_0003 (Basic
api_sc_bind/UnbindObject testing).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a comment to clearly state the functions are empty on purpose, but
they still need to be provided to support the generic code flow.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The functions insert_region() and create_rootserver_objects() are not
used outside of boot.c, so there is no reason to make it publicly
available.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Replace the macro SMP_TERNARY(getCurrentCPUIndex(), 0) by the much
simpler macro CURRENT_CPU_INDEX() that does the same.
Signed-off-by: Axel Heider <axelheider@gmx.de>
CURRENT_CPU_INDEX() is supported to return a word_t. The C parser from
the verification toolchain requires declaring word_t constants without
casting integer values to word_t.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This fixes a correctness and security issue where uncached user
mappings might see old data from before the clearMemory operation.
See also the discussion on GitHub issue #481
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Also merge create_device_untypeds() and create_kernel_untypeds() into
create_untypeds() to simplify the code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Make the definition for NULL generic, so it can be used in constants
that are shared by C and assembly code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Provide the macro ULL_CONST() for 'unsigned long long' constants, and
use it where applicable.
- Add a verbose explanation why the 'unsigned long long' type is used
for time constants.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Reorder the macro definitions to ensure things are define before they
are used.
- provide a verbose explanation why the UL_CONST() macro is needed.
- make BIT() macro is defined generic by using UL_CONST().
Signed-off-by: Axel Heider <axelheider@gmx.de>
Also make the output more verbose in case of errors, which is
helpful when porting the kernel to new platforms.
Signed-off-by: Axel Heider <axelheider@gmx.de>
With this change, even architectures which do not use a distinct region
to map the kernel ELF will use the `kpptr_to_addr` to translate any
address from the kernel region.
This ensures that these accesses are correctly checked for bounds when
used and will make it easier to move the ELF mapping into a distinct
region of virtual address space.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Move all of the virtual to physical translation functions into a single
common file and use the updated constants.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Like SCTLR, CNTV_CTL is switched to/from hardware when we enable/disable
the VCPU, so it must be read from a saved VCPU context when that VCPU
isn't active.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The scheduler cannot correctly schedule once the timestamp exceeds
MAX_RELEASE_TIME as releases beyond this point may be subject to
overflow. For most systems this should still allow a great many years if
the timestamp starts from 0 at system boot.
Some systems currently start with a random initial timestamp and my
begin with a timestamp that prvents correct budgeting. This assert helps
to catch cases where scheduling becomes invalid due to the timestamp
exceeding the give bound.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The proofs currently only guarantee that the system scheduler is correct
while the current time is less than INT64_MAX - 3 * MAX_PERIOD ticks.
With the MAX_PERIOD configured to almost INT64_MAX, this would imply
that the system scheduler is never correct.
To ensure that we get a large duration where the system is correct, we
take 1/8th of the TOTAL representable time as the MAX_PERIOD, ensuring
that 3 * MAX_PERIOD is still less than half of all representable time.
For a system with a 1MHz scheduling clock, this produces a valid
execution time on the order of 2^19 years.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This re-introduces the overrun handling but bounds charging of budget
such that we never calculate a refill with a start using an integer
overflow.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
