Gerwin Klein
Gerwin Klein
We just finished tracking down a bug in a PR where `ticks_t` was implicitly converted by the compiler to `word_t`, changing the value (overflowing 32 bit) and causing the kernel...
Should mentioned which files are installed and where to expect them.
The combination of `clang`, `release`, and `SMP` hangs on boot on the `hifive` board, see e.g. https://github.com/seL4/seL4/actions/runs/7508485461/job/20463803054 ``` U-Boot 2018.09-g6f6e014-dirty (Jul 04 2019 - 12:40:44 +1000) DRAM: 2 GiB MMC:...
This could be just a fluke, but I have not seen this failure before, so we should investigate. The [scheduler accuracy test failed](https://github.com/seL4/seL4/actions/runs/6799723233/job/18514588830#step:4:3505) for config `ODROID_XU4_debug_MCS_clang_32`: ``` Running test SCHED0011...
## Generic - [ ] add completed status of RISCV - [ ] add ongoing status of AARCH64 - [ ] update status of MCS verification - [ ] update...
At boot time we print memory regions as `[a..b]` even though `b` is not included in the interval. This has confused me a number of times in the past, I...
In general, the seL4 manual puns too much between objects and capabilities, which tends to lead to confusion. The correct terminology used in the code and specs is that capabilities...
We should provide a glossary of technical terms in the seL4 manual so it is easy to look up what e.g. VSpace, CSpace, etc mean without need to search through...
The [Haskell kernel](https://github.com/seL4/l4v/tree/master/spec/haskell) has extensive code-level documentation in literate programming style, which is not visible for people working purely on the C implementation. We should migrate this documentation and turn...
This PR adds verification for the SGISignalCap API of [RFC-17](https://sel4.github.io/rfcs/active/0170-multikernel-ipi-api.html) (seL4/seL4#1222). Specs and proofs are updated for all architectures (affects mostly ARM, ARM_HYP, and AARCH64), including all affected parts of...