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.

[Indanz]

When working on the MEP system @bennoleslie and I ran into the issue that we wanted to reserve a large contiguous memory area, and the only way to do that would be to change seL4's DTS and mark the region as device memory. That reserved memory was also used to load a user space binary.

We used U-boot to load seL4, the Linux kernel and the seL4 application to the correct memory location. Then the VMM would copy the kernel to its final location, but as the original copy was still there, restarting Linux was relatively easy. Updating the Linux kernel is a matter of temporarily mapping that loading area writeable, writing the new image, unmapping and restarting the VM as usual. The same for updating the user application: After its binary was updated, just restart it as usual and the new image will be loaded. This seems harder to do if you embed the image into the loader.

Although using DT for this works, it propagates through all layers and is not very elegant. It seems like that patch is a slightly cleaner solution for this problem, as it at least takes out seL4, although it only helps for the Microkit loader and not Elfloader.

To me it seems your alternative solution works fine if you don't need memory regions with known physical addresses (for e.g. U-boot), and don't need contiguous memory for e.g. VMs.

[Ivan-Velickovic]

Thanks for your comments.

To me it seems your alternative solution works fine if you don't need memory regions with known physical addresses (for e.g. U-boot), and don't need contiguous memory for e.g. VMs.

I am a bit confused by this, I don't see how this would stop us allocating a large contiguous region of memory? The Microkit tool has only two restrictions on where it can allocate user-specified memory regions from. One is the region for seL4 itself, and the other is for the initial task. Everything else could be in theory used by the user. Given neither seL4 or the initial task use up much space relative to the typical size of RAM, I don't see how allocating a large contiguous chunk of memory for a VM at particular physical address (e.g for 1-1 mappings for DMA) would be difficult. If it would be difficult with the proposed approach, it would be difficult with the existing approach, as both approaches would use about the same amount of memory.

This seems harder to do if you embed the image into the loader.

Can you clarify what you mean by "loader" in this case? Loader means boot-loader to me but some other people use it to mean the initial task.

[Indanz]

I am a bit confused by this, I don't see how this would stop us allocating a large contiguous region of memory?

In our case we tried allocating exactly half of 1 GB memory region, but that was impossible to do because of fragmentation and reserved UTs at both start and end of the address space. There were some patches fixing some of those unnecessary fragmentation issues in seL4, but I don't think all were fixed yet. So the only way to get this was reserving that area as device memory in DT.

Your Microkit patch would allow the same to be achieved, but you can't embed half the RAM in the initialiser itself. Or can you tell the initialiser where to put itself and what memory to reserve? If so, perhaps it's still possible.

Can you clarify what you mean by "loader" in this case? Loader means boot-loader to me but some other people use it to mean the initial task.

I meant it generically. If whatever any loader needs to load is embedded into it, then reloading an updated binary will always be more difficult, because you can't reuse the existing loading code. Except if you can reserve extra space and overwrite the embedded binary, but you have to be very careful when doing that.