Pre-RFC: ARM Boot Interface Versioning

1

Summary

Previous discussion on a boot interface (Pre-RFC: Boot Interface) stalled.

I think one reason for stalling is that there are differences of opinions on exactly what the boot interface should be.

This RFC proposes an alternative that allows for multiple boot interfaces.

Motivation

Different platforms and systems have different needs for their initial startup / boot time configuration of the kernel.
In particular the specification of untyped memory regions is particularly important.

While there have been discussions on somee options here there is yet to be a strong proposal with widespread support.
One challenge to buiding this support is that it is difficult to build and prototype solution right now.
Additionally, any change has the potential to be disprutive to the ecosystem, which of course reduces the change of any change being accepted.

Explanation

The function signature for init_kernel is changed to incorporate a boot protocol version number.

BOOT_CODE VISIBLE void init_kernel(
    paddr_t ui_p_reg_start,
    paddr_t ui_p_reg_end,
    sword_t pv_offset,
    vptr_t  v_entry,
    paddr_t dtb_addr_p,
    uint32_t version_dtb_size
)

The final parameter dtb_size is adjusted to include both a version number and the dtb size.

The top four bits of the version_dtb_size is to be considered the version, while the
lower 28-bits the dtb_size. For example:

uint8_t version = version_dtb_size >> 28;
uint32_t dtb_size = dtb_size & 0x0fffffffUL;

This allows for dtb_size of up to 256MiB which should be sufficient in any practical system.

This approach should result in a version of zero for all existing software that uses the current boot interface.

Values 0 through 14 are reserved for official seL4 boot interface version.

Values 15 is avaialble for custom boot interface versions.
This is used, for example, when prototype a new interface or for a fork-specific boot interface.

When handling a different boot interface the kernel may treat the arguments to init_kernel differently.
For example, it may treat dtb_addr_p as a pointer to a data structure that conveys additional information between the loader and the kernel.

Usage

By itself this doesn’t really do anything.

What it allows for is development of new boot interfaces and the merging of those boot interfaces
in such a way that the kernel can remain compatible with other boot interfaces.

Even in the case where only a single boot interface is used in the kernel at any point in time
this still has the benefit of the kernel being able to check the version between the loader and the kernel.

Alternatives

An alternative is that those experimenting with alternative boot interface can just change the code without worrying about backwards compatibility.
The challenge with this is that coming up with a new boot interface takes some time, and leads to a long lived branch.
The kernel is now moving at a pace where it is preferable to continually rebase/merge against upstream.
This is easier to do when the bulk of code is new rather than changes to existing code.

An alternative is that we always see the kernel as strongly coupled with the loader, so no version checking would be required.

An alternative is that any change in boot interface is not versioned.

2

If we introduce this, it should not be limited to ARM, but also apply for RISC-V. Not sure how about x86. My impression was, that seL4 follows the idea there is always a kernel/system loader that knows exactly what to loade. The kernel itself is not meant to run from scratch. Thus the problem could be solved at a meta-level also, a certain kernel will always get exactly what it expects.
I have commented in other places, that I not too happy with the current boot interface in general and more radical change might be beneficial. There should be a few more details about the user image that are passed. We could also change the way how data is passed. Instead of registers, there could be a data structure in memory with either fixed fields or something highly dynamic, like a tag-length-value blob (like the ATAGS from linux) or the DTB format.
Maybe we should come up with a list first, what we want to change and then see how this affects the interface. Just adding a version here might make things more messy and requires a plan how to support this legacy - which might be something nobody is really too enthusiastic about in the long run.

3

I think there are plenty examples of potential changes over in the referenced Pre-RFC: Boot Interface It was precisely the fact that this conversation stalled out that I was looking for a different way of approaching the problem.

4

In the other discussion, @bennoleslie used loader code to refer to code that passes control to the kernel, and boot code to mean code in the kernel. I’d add that boot code is code in the kernel that runs until control is first passed to user level.

What are the problems that this change is trying to solve? My guesses:

  1. There is currently no way that the kernel boot code to check if the loader code has done what it expects.

As pointed out in the alternatives section, we currently see the boot code as strongly coupled with the loader code. This is also consistent with how we currently see the first user level code as strongly coupled with the kernel code. There’s currently no version identifier in the seL4_BootInfo structure either. So there appears to be a decision point here: Do we at least wish to be able to detect when there is a version mismatch between loader/kernel/user code assumptions at runtime? This is probably net useful in my opinion.

It seems that there are implied larger problems that this proposal is making a first step towards addressing:

  1. The boot code has too much policy and not enough configuration options to control it. An example of this is it’s assumption that the kernel and userlevel code can be described via 2 contiguous memory ranges referring to binaries preloaded in RAM memory.
  2. The same kernel binary can only be loaded with a single strategy and so you couldn’t take the same binary and deploy it across different loaders that want to use different loading variants
  3. If only one implementation of the bootcode is going to get verified, then there should be options to evaluate different candidates than what is already present.

The current verification of the kernel assumes that when the boot code passes control to user level, the kernel state has been initialized and satisfies all of the required spec invariants. The boot code doesn’t currently have the same verification story as the rest of the kernel but adding a stronger story is an open goal. The verification has even less to say about how the loader code should have set things up when passing control to the boot code.

My most radical view is that until the boot code becomes verified, loader code and boot code are essentially the same. So if we are happy for the use of arbitrary loaders then we should also be happy for them to provide arbitrary boot code too and handling all execution before control is passed to userlevel and the kernel invariants have been initialized would allow them to better implement their own policies for initial kernel object layouts and initial object values. The current kernel boot code then just serves as a tested working example of what this code could be.

This would also allow multiple versions of boot code to be tested and developed before hopefully agreeing on a version to verify that is satisfactory for everyone.

5

Thanks for the thoughtful reply @kent-mcleod2

Regarding terminology, I was using loader code to refer to any (all?) code on the system that executed prior to the init_kernel entry point. I was considering init_kernel and everything it does up to the point of transferring control to the user thread to be kernel boot code (or just boot code).

I specifically said loader (and not Elf Loader) to allow for all the code that goes into making that happen, which also includes any platform bootloader coder, and also to allow for alternative code bases other than ElfLoader to be used. (Which is something I currently actually do).

Certainly this is a step towards solving the first two points that Kent mentions. Specifically right now I have a branch (/ fork / patches) that enables more than 2 memory ranges referring to binaries (and specifically having a region that is considered untyped device memory so that user code can make it large pages and not have it erased by the kernel).

I also very much would like to allow for more kernel configuration to be provided by the loader and reduce the number of kernel binaries that are required. Including, for example, the ability to specify the physical memory and location of devices in physical memory. This would (perhaps) reduce the number of kernel configurations required.

But these are somewhat ideas only. And while I respect the Pre RFC approach, I don’t think I’ll advance these ideas without examples and working code. To this end, part of this proposal is an extremely minor thing (let’s 4 unused bits to represent a version) that enables some experimentation with these ideas.