When seL4 master is updated, the preprocess-deploy workflow tests
whether the change affects the prepocessed sources seen by verified
configurations. If not, then the development verification-manifest is
automatically updated to the new commit.
Previously, this was only done for the non-MCS manifest (devel.xml).
This commit implements the same process for the MCS manifest (mcs.xml).
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>
- makes setting more generic an allow overriding parameters
- save QEMU parameters in DTS as comment
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>
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>
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>
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 <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 e22089d0c (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>
Add a comment that they are empty on purpose. They are not removed to
keep the infrastructure in case there will be deprecated items in the
future.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- 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>
* 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>
