Currently, building `libsel4` as a static library with `KernelIsMCS`
enabled fails with the following error:

```
static declaration of 'seL4_NBWait' follows non-static declaration
```

This [was mentioned][1] in the original PR that modified exported
functions to use `LIBSEL4_INLINE_FUNC`.

[1]: https://github.com/seL4/seL4/pull/101#issuecomment-442010551



Signed-off-by: Klim Tsoutsman <klim@tsoutsman.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>

This removes a memzero call from the seL4_SchedContextObject and seL4_ReplyObject cases of createObject. The memory is now cleared via clearMemory within resetUntypedCap

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

Signed-off-by: Seiya Nuta <nuta@seiya.me>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Co-authored-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

This adds support for the Pine64 Quartz64 and other devices based on
the Rockchip RK3566. The platform support is adapted from the
Rockpro64 code, except that the RK356x has A55 cores, and adjusting
for the fact that the ARM Generic Timer is the only on-chip timer
available.

Signed-off-by: Peter S. Housel <housel@acm.org>

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

GitHub has deprecated the old node12-based actions.

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

Apply changes from commit 0f619780

 for MCS also

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

- makes setting more generic an allow overriding parameters
- save QEMU parameters in DTS as comment

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Also reject any unknown CPU.

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Like the sel4test hardware runs, a sel4bench run can be requested via
adding a label (`hw-bench`) to any PR.

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

Fix issues from refactoring in commit 27b4411e



Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Fix wrong name used in refactoring of commit 4b491dcf



Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

activate_global_pd is just an alias for activate_kernel_vspace nowadays

Signed-off-by: Axel Heider <axel.heider@hensoldt.net>

Signed-off-by: Jorge Pereira <jorgepereira89@gmail.com>

The clock frequency on the mpfs icicle kit is 1 MHz so the
TIMER_FREQUENCY polarfire config was changed to 1 MHz (was 10 MHz). This
fixes the errors seen duration the scheduler preemption test.

Signed-off-by: Alex Pavey <Alex.Pavey@dornerworks.com>

Signed-off-by: Alex Pavey <Alex.Pavey@dornerworks.com>

Signed-off-by: Alex Pavey <Alex.Pavey@dornerworks.com>

This also adds a compile assert for checking that MinSchedContextBits
is the correct size in relation to seL4_CoreSchedContextBytes.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

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>

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

Remove redundant (and incorrect) reserved memory
definition for VideoCore memory. The reserved
memory area is defined in 'overlay-rpi4.dts'.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

RPi4 is definitely running in low peripheral
mode by default.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

kernel,bcm2711: Fix RPi4 DTS overlay

The build system mishandling of disjunct
memory areas seems to no longer be true.
It may have been a bug in build system/env,
so remove the comment about it and update
memory node accordingly.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

kernel,bcm2711: Remove leftover comment

Remove leftover comment about adding DMA
dedicated reserved memory areas.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

Translate system timer address, and remove IRQs for
channels 0 and 2. These channels are used by VideoCore,
having them defined causes a spam of spurious interrupts.

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

Signed-off-by: Hannu Lyytinen <hannux@ssrc.tii.ae>

Signed-off-by: Hannu Lyytinen <hannu.lyytinen@unikie.com>

kernel,bcm2711: Fix RPI4 address mapping

Fix build error and warnings by removing GPIO mapping
from overlay. Also as a note, don't add 'serial1' or 'ethernet'
here, because 'serial1' is already mapped to sel4 kernel by
'chosen' block in 'overlay-rpi4.dts', and the translation for
the 'ethernet' is done with 'ranges' property.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

kernel,bcm2711: Fix memory area overlay DTS

First fix is to change the memory area reserved for
the VideoCore from 64 -> 76 MB, as this is the default
value on RPi4. Using other values would require configuration
of the first stage bootloader with 'config.txt' file.

Second fix is separating the disjunct memory areas
to separate nodes, as the generator Python scripts
in 'kernel/tools/' etc discarded the first area below
1GB limit if all areas were defined in the same node.
The effect of different variations can be observed
during kernel build in the generated
'kernel/gen_headers/plat/machine/devices_gen.h' header.

Third fix is adding the reserved memory area for the
VideoCore memory to avoid any collisions.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

See commit e22089d0

 (rpi3: Mark first memory page
as reserved, 2021-07-12) for more details. Same thing
applies to RPi4 also regarding the spin tables
and secondary cores.

Signed-off-by: Joonas Onatsu <joonasx@ssrc.tii.ae>

This was only required since the PCI bus was generating devices that
were too large when running in hypervisor mode. That behavior has been
fixed, so the overlay is not needed.

Signed-off-by: Chris Guikema <chris.guikema@dornerworks.com>

When compiling in the Docker container on an M1 MacBook, or any other
ARM host, the CMAKE_HOST_APPLE variable is not set. Therefore, no
CROSS_COMPILER_PREFIX is set and x86 applications will not compile.

This commit adds another check to see if the host processor is an ARM
chipset, and sets the appropriate CROSS_COMPILER_PREFIX variable.

Signed-off-by: Chris Guikema <chris.guikema@dornerworks.com>