Gerwin Klein

bitfield_gen: properly escape backslash

1

Replace `"\

Merge once CI has settled for release commit.

stale frame cap could be used to flush "wrong" memory

1

If a frame cap whose ASID/vaddr mapping information is out of date is used in one of the page flush operations (`ARMPageClean_Data`, `ARMPageInvalidate_Data`, `ARMPageCleanInvalidate_Data`, `ARMPageUnify_Instruction`), and the kernel runs in...

boot printing leads to assertion failure on SMP+MCS

7

Commit 43667a0 from PR #438 which looks entirely harmless, leads to an assertion failure immediately after dropping to user space for SMP + MCS on the sabre board. It's not...

Should we reduce DSpec to sys-init operations only?

3

Currently `DSpec` has capDL behaviour for most operations in the kernel, including granting caps via IPC and other operations that the system initialiser does not use. Although we had more...

support strongest-postcondition reasoning

1

We currently have `_sp` rules for a number of the basic monad constructs, and we're using them manually in some situations, e.g. to avoid case blow-up in wp reasoning or...

Currently, the `cspec/c` Makefile is insensitive to changes in `L4V_PLAT` in the sense that it will not necessarily rebuild correctly when you change the value of `L4V_PLAT`. This is no...

## Platform branches - what they are - how they work - how to fix them when they break

See also https://github.com/seL4/sel4bench-manifest/issues/16 -- gcc-11 is producing a segfault when compiling `ipc.c` in sel4bench: ``` [76/258] Building C object apps/sel4bench/projects_libs/libjansson/CMakeFiles/jansson.dir/jansson-2.7/src/load.c.obj ... ... /home/dinuka/Research/sel4bench/projects/sel4bench/apps/sel4bench/src/ipc.c: In function ‘process_ipc_results’: /home/dinuka/Research/sel4bench/projects/sel4bench/apps/sel4bench/src/ipc.c:40:27: internal compiler error:...

- add test SCHED0023 to check that round robin threads are indeed scheduled round robin. - print thread id in periodic thread tests The test relies on relative timing of...