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>
