Signed-off-by: Yanyan Shen <yshen@hybridkernel.com>

Signed-off-by: Axel Heider <axelheider@gmx.de>

* Fix compilation with CLANG > 11

LLVM 12 makes -moutline-atomics on by default;
turn it off.

Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>

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>

* Fix GCC-12 warnings (treated as errors)

This addresses bug #875.

Unfortunately, added a command line parameter to gcc is not backaward
compatible with other versions of GCC.  So use a #pragma in the only
file that's a problem.

Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>

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>

Signed-off-by: Ahmed Charles <acharles@outlook.com>

Signed-off-by: Ahmed Charles <acharles@outlook.com>

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>

Mark the .bss sections in the Arm and RISC-V linker scripts as NOLOAD to
reflect the default behavior. The x86 linker script already explicitly
sets this option.

Signed-off-by: Kent McLeod <kent@kry10.com>

This prevents the idle thread object from taking up space in the ELF
file as it is expected to be initialized as all zeroes.

Signed-off-by: Kent McLeod <kent@kry10.com>

This allows the .boot.bss data to be reclaimed by user level when the
kernel has finished booting.

Signed-off-by: Kent McLeod <kent@kry10.com>

The RISC-V Instruction Set Manual - Volume II: Privileged Architecture:

For non-leaf PTEs, the D, A, and U bits are reserved for future standard
use. Until their use is defined by a standard extension, they must be
cleared by software for forward compatibility.

Signed-off-by: Ahmed Charles <acharles@outlook.com>

Signed-off-by: FinnZhang <finnzhang@outlook.com>

This adds AUXUPD and GHOSTUPD comments to aid verification in
reasoning about the length and type of the refill buffer
associated with scheduling contexts

This also add a AUXUPD comment for replies

Signed-off-by: Michael McInerney <michael.mcinerney@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>

There are cases that reasonably require non-ASCII characters in the
source code, hence tools/bitfield_gen.py must be able to handle them
correctly. This commit makes sure the bitfield generator consistently
opens all files with UTF-8 encoding.

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Bin Meng <bmeng.cn@gmail.com>

Generated from maaxboard-dcss-hdmi.dts (Avnet/linux-imx) for more
comprehensive device support. Updated overlay to align.
Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>

Sometimes device trees may have differences between vanilla Linux
and SoC vendor, and the changes can be tedious to override with a
device tree overlay.

This change allows overriding the platform default dts and overlays
with a custom dts.

Signed-off-by: Markku Ahvenjärvi <markkux@ssrc.tii.ae>

Some inter-procedural optimisations can produce cloned or partial
functions in the binary. Since binary verification is incompatible with
cloned and partial functions, we add a config option to disable these
optimisations.

This does not change any defaults, so to avoid cloned and partial
functions for a binary verification build, it is necessary to explicitly
configure this, e.g. using `-DKernelBinaryVerificationBuild=ON`.

Signed-off-by: Matthew Brecknell <matt@kry10.com>

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>

sc_sporadic() already calls sc_active.

Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>

The MCS-related macros were causing the build to fail when configured to
use the sysenter instruction. Additionally, some message registers
weren't explicitly being passed to the assembly block for
seL4_NBSendRecv in this configuration.

Signed-off-by: Jimmy Brush <code@jimmah.com>

Signed-off-by: Kent McLeod <kent@kry10.com>

Use kernel's config.h

Signed-off-by: Axel Heider <axelheider@gmx.de>

Avoid redundant code.

Signed-off-by: Axel Heider <axelheider@gmx.de>

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>

Changes compiler options and the linker script to group most small data
objects together in a new .small section, and point __global_pointer$ at
.small so that nearly all objects can be referenced via gp.

Signed-off-by: Stefan O'Rear <sorear@fastmail.com>

Signed-off-by: Stefan O'Rear <sorear2@gmail.com>

For writing/reading/copying TCB registers, the
arch_flags parameter is not used on RISC-V (in
addition to x86 and ARM).

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Various kernel symbols have changed their names; update
the GDB macros to match.  Also remove hard-coded  0xf0000000 for
the address of the kernel window.

Signed-off-by: Peter Chubb <peter.chubb@unsw.edu.au>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

When using the cortex-a9 CPU allow the kernel to be used as a
hypervisor.

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>

The value supplied in the maaxboard.dts file provided by
Avnet is too small. It is corrected in the overlay DTS file.
Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>

Signed-off-by: Mark Jenkinson <mark.jenkinson@capgemini.com>
Co-Authored-By: Stephen Williams <stephen.williams@capgemini.com>

Set Write-through non-transient, No-Write-allocate, Read-allocate
attributes for kernel log buffer.

Signed-off-by: Nataliya Korovkina <malus.brandywine@gmail.com>