Ivan Velickovic
Ivan Velickovic
This PR aims to add test coverage for https://github.com/seL4/seL4/issues/214. More specifically. it implement tests for the scenarios outlined here: https://github.com/seL4/seL4/issues/214#issuecomment-1558628554. I have left out testing of `VMKernelReadOnly` mappings as I...
There are some fault types missing from the manual, such as: * VGIC maintenance faults (`seL4_Fault_VGICMaintenance`) * VCPU faults (`seL4_Fault_VCPUFault`) * VPPI events (`seL4_Fault_VPPIEvent`) I suspect these are missing since...
It would be nice, for projects like Microkit where the system architecture is specified at build-time, if the value of `MAX_IRQ` for ARM and RISC-V platforms is exported as part...
Roadmap
As some may be aware, there has been significant development and change on Microkit outside of the mainline version. This currently lives [here](https://github.com/Ivan-Velickovic/sel4cp). This issue outlines the roadmap of up-streaming...
There is currently no API for doing cache operations on ARM platforms. This leads to code like this https://github.com/seL4/microkit/blob/71e014494367d12f8b12bad9d7d1655778ca2cc2/example/tqma8xqp1gb/ethernet/eth.c#L609 which should not be necessary. We could add simple wrappers such...
seL4 enforces a maximum IRQ number for ARM and RISC-V platforms, we should check for this at build time to avoid an seL4 invocation error upon boot. Depends on https://github.com/seL4/seL4/issues/1207.
Currently Microkit supports 4K and 2MiB page sizes. It would be fairly easy to add 1GiB page sizes as well which would be useful especially for things like virtual machines.
I believe there are a couple of ARM platforms (the Raspberry Pi 3 is one of them) that have a non-standard interrupt controller. This platforms are configured with `HAVE_SET_TRIGGER` to...
The approach of using `seL4_NBSendRecv` in the event handler loop of libmicrokit when PDs essentially 'make' themselves passive by sending a message to the monitor is not ideal for multiple...
Initial CI has been added just to double-check PRs that *look* like they don't break anything. We will of course need proper CI that also tests the SDK. This will...