Allowing Microkit to not require a kernel patch

[Ivan-Velickovic]

There is currently a single patch to the seL4 kernel (https://github.com/seL4/seL4/commit/c8ef493d038b81cc43f82c0190788e4b3bdb4d9d) that Microkit depends on.

What is the patch for?

The patch allows the boot-loader, which runs before seL4, to specify an extra region of device untyped at run-time when the boot-loader jumps to seL4.

Why is the patch necessary?

The boot-loader that Microkit systems use places all binaries in the expected places in physical memory before jumping to seL4. This includes binary for seL4 itself, the initial task (aka the monitor), as well as the binary for each protection domain.

However, when seL4 starts, it clears all physical memory that it defines as 'normal'. This means all memory in RAM (except seL4 itself and the initial task) will be cleared. Without the kernel patch, this would include the PD ELFs, meaning that when the PDs start, all the code for them will be gone.

In order to avoid this, we place all the PD ELFs in a contiguous region of physical memory that we tell seL4 at boot is 'device' memory, meaning that it won't clear it and hence the PD ELFs remain in tact after seL4 has booted.

How will the patch be removed?

Assuming there are no blocking issues, the new Rust capDL initialiser can be used to embed the binaries for each PD in the initialiser itself, while not copying the binaries around in memory. This allows us to have the memory efficiency desired without a patch to the kernel.

After the kernel patch is removed, a specific branch of seL4 will no longer be required. Note that Microkit may be pinned to a specific version of seL4 still, so not just any commit of the kernel will work.