This project is mirrored from https://github.com/seL4/seL4.git.
Pull mirroring updated .
- 17 Jan, 2023 1 commit
-
-
Klim Tsoutsman authored
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>
-
- 13 Jan, 2023 1 commit
-
-
Axel Heider authored
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>
-
- 10 Jan, 2023 2 commits
-
-
alwin-joshy authored
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>
-
michaelmcinerney authored
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>
-
- 08 Jan, 2023 1 commit
-
-
Seiya Nuta authored
Signed-off-by:
Seiya Nuta <nuta@seiya.me>
-
- 03 Dec, 2022 3 commits
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
Co-authored-by:
Ivan Velickovic <i.velickovic@unsw.edu.au> Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
- 23 Nov, 2022 1 commit
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
- 21 Nov, 2022 4 commits
-
-
Peter S. Housel authored
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>
-
Gerwin Klein authored
Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
GitHub has deprecated the old node12-based actions. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Axel Heider authored
Apply changes from commit 0f619780 for MCS also Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
- 13 Nov, 2022 4 commits
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
- makes setting more generic an allow overriding parameters - save QEMU parameters in DTS as comment Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
Also reject any unknown CPU. Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
- 11 Nov, 2022 4 commits
-
-
Gerwin Klein authored
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>
-
Axel Heider authored
Fix issues from refactoring in commit 27b4411e Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
Fix wrong name used in refactoring of commit 4b491dcf Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
Axel Heider authored
activate_global_pd is just an alias for activate_kernel_vspace nowadays Signed-off-by:
Axel Heider <axel.heider@hensoldt.net>
-
- 08 Nov, 2022 1 commit
-
-
Jorge Pereira authored
Signed-off-by:
Jorge Pereira <jorgepereira89@gmail.com>
-
- 06 Nov, 2022 3 commits
-
-
alexkaiser authored
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>
-
Jesse Millwood authored
Signed-off-by:
Alex Pavey <Alex.Pavey@dornerworks.com>
-
Jesse Millwood authored
Signed-off-by:
Alex Pavey <Alex.Pavey@dornerworks.com>
-
- 04 Nov, 2022 1 commit
-
-
Michael McInerney authored
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>
-
- 30 Oct, 2022 1 commit
-
-
Axel Heider authored
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>
-
- 28 Oct, 2022 4 commits
-
-
Indan Zupancic authored
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>
-
Indan Zupancic authored
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>
-
Indan Zupancic authored
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>
-
Axel Heider authored
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>
-
- 27 Oct, 2022 1 commit
-
-
Michael McInerney authored
Signed-off-by:
Michael McInerney <michael.mcinerney@proofcraft.systems>
-
- 26 Oct, 2022 6 commits
-
-
Joonas Onatsu authored
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>
-
Joonas Onatsu authored
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>
-
Markku Ahvenjärvi authored
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>
-
Hannu Lyytinen authored
Signed-off-by:
Hannu Lyytinen <hannux@ssrc.tii.ae>
-
Hannu Lyytinen authored
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>
-
Joonas Onatsu authored
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>
-
- 23 Oct, 2022 2 commits
-
-
Chris Guikema authored
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>
-
Chris Guikema authored
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>
-