Some recent offline discussions have brought up a number of questions about how the boot process works, how we get from an external bootloader such as U-Boot to an initial task executing on seL4, and which components are involved and what their precise responsibilities are.
The current situation differs somewhat between architectures, ARM and RISC-V both boot via the intermediary elfloader which is responsible for booting multiple cores, unpacking the ELF for the kernel and the initial task into physical memory a small amount of information about the initial task and device tree (although the form this currently takes is fairly limited). For x86, the kernel boots directly from multiboot and the boot code within the kernel is responsible for ELF loading the initial task and initialising additional cores.
The interface between the kernel and whatever starts it is fairly limited and can make it difficult to start the kernel via something other than elfloader (such as a ROM-based firmware loader) without needing to maintain a fork of the kernel itself. The documentation for this process is also limited.
For static systems, where there is a static set of task ELF files that are loaded at system startup, this can also lead to both elfloader and the root task being responsible for loading ELF binaries into memory.
I’m personally a fan of the way that elfloader separates the concern of initializing physical memory from the kernel’s responsibility of creating the initial kernel objects and capabilities for the root task and think we could better generalize this. I think we should consider making the kernel’s boot responsibilities more consistent across architectures and better defined and documented.
Fundamentally, the only responsibility the kernel needs to have is to initialize its global and per-core internal state and to create the initial capabilities and kernel objects and set up the capability space and virtual address space for the initial task. Much of what occupies the initial state of the initial task could be passed through directly from the whatever initializes the kernel, all the kernel needs to be able to add is the information describing how the initial capability space is structured.
My question at this point is what should the responsibilities of each component in the boot chain actually be and what should the interfaces between them look like?