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>
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>
