This adds a well-defined interface for the kernel to boot itself in a manner that allows any pre-boot software to be readily interchanged on any platform.
elfloader will then be modified to use this interface to boot the seL4 kernel and pass control to the kernel.
The seL4 kernel currently makes differing degrees of assumptions depending on the architecture for which it is targeted (x86 assumes multiboot, arm and risc-v assume particulars of
elfloader) and the responsibilities of the kernel aren’t consistent across architectures and platforms. This can make it difficult make more general use of the kernel with alternative bootloaders or to pass through boot-time configuration to a system build on seL4.
The kernel is generally responsible for configuring the few devices that it uses as the system runs (serial device in debug configurations, IRQ controller, and hardware MMU) as well as for constructing global kernel mappings and initial user-level mappings, objects, and capabilities.
The kernel should depend minimally on the boot process used or any any one particular boot process. Additionally, any initialisation that can be done prior to kernel boot that doesn’t affect the kernel’s ability to maintain platform or device configuration as the system executes should be delegated to the boot code that executes prior to the kernel.
The kernel will make a set of assumptions about the state of the system when it first accepts control:
- The kernel image is copied into physical memory
- That a given set of platform registers have been assigned specific values or refer to memory regions with specific contents.
- For a given platform and configuration
- The kernel is executing at some particular privilege level
- The kernel is with virtual addressing enabled with some specific configuration of the platform’s virtual addressing system
- x86 may assume specific GDT/IDT entries
- Specific values for relevant addressing registers
- Either that the kernel has been entered on only one core or that it has been entered on all available cores
The software that executes prior to the kernel starting supplies the kernel on each node with a numeric identifier for the node that is executing, a boot configuration structure, and a table of mapping regions.
The configuration structure specifies:
- the starting virtual address of the initial user-level task,
- the number of entries in the mapping region table, and
- a single word value that is passed to user-level via the bootinfo struct (generally a pointer to an extended boot information structure mapped into the initial task).
The mapping region table describes a series of physical address regions that are any of:
- a reserved region that should not be used by either the kernel or be made accessible to user-level,
- a mandatory kernel code / read-only data and read/write data virtual-physical mapping (which the kernel may expect to fall into fixed locations),
- a mandatory kernel read/write data
- a user-level virtual-physical mapping, or
- an unused physical memory region.
The physical regions must satisfy the following constraints:
- The physical address range of one region may not overlap the range of any other region
- User-level mappings must be aligned to the smallest page size and be a multiple of that size
- The two kernel-level mappings must each fall entirely within a single page of a size defined by the architecture (large on riscv32, ia32, aarch32, and x86_64; huge on riscv64 and aarch64)
- The mapping region table itself must
- Not fall within either kernel mapping region
- Not fall within any user-level mapping region
- Be aligned to the smallest page size
Any boot information passed to the initial task from the bootloader or boot code prior to seL4 is defined entirely by that bootloader or boot code.
When the kernel starts, if it is responsible for starting additional cores it does so. All cores wait until the boot core has initialised the kernel state and devices.
The boot core will check the region table to ensure that the regions satisfy the necessary constraints. It will then re-map itself using the kernel global mappings. It can then map and initialise any devices it uses directly.
The kernel will then create an initial set of untypeds from the regions of memory not covered by the reserved regions, kernel mappings, user-level mappings, or the region table itself.
From the initial untypeds, the kernel will bootstrap the initial task creating all the necessary kernel objects and mapping the user-level mappings into place.
Finally the kernel will reclaim the memory used by the region table and, if it was marked as reclaimable, the boot portion of the kernel code and produce untypeds.
Outline any arguments that have been made against this proposal and discuss why we may not want to accept it. Also discuss any complications that may arise from the proposed change that may require specific consideration.
Rationale and alternatives
- Most of this is how the kernel already functions
- Allows for pre-kernel boot software other than
elfloaderto be used to boot the kernel (e.g. simple embedded firmware)
- The boot process on x86 currently allows any user-level image to be specified at boot time but this is not currently possible when using
elfloader, alternative loaders could be used to overcome this limitation in elfloader
- Provides a general manner for boot information (such as DTB, multiboot information, or boot parameters) to be passed to the initial task (which is not currently well supported by the kernel)
- Allows the kernel code to be executed from flash, better supporting memory-constrained applications
- Clearly documents the assumptions made by the kernel at boot in a manner that can be easily checked
TODO: Prior art
Discuss prior art, both the good and the bad, in relation to this proposal. A few examples of what this can include are:
- For ecosystem proposals: Does this feature exist in similar systems and what experience have their community had?
- For community proposals: Is this done by some other community and what were their experiences with it?
- What lessons can we learn from what other communities have done here?
- Are there any published papers or great posts that discuss this? If you have some relevant papers to refer to, this can serve as a more detailed theoretical background.
This section is intended to encourage you as an author to think about the lessons from other systems, provide readers of your RFC with a fuller picture. If there is no prior art, that is fine - your ideas are interesting to us whether they are brand new or if it is an adaptation from other systems.
Note that while precedent set by other systems is some motivation, it does not on its own motivate an RFC.
TODO: Unresolved questions
- What needs to be resolved in further discussion before the RFC is approved?
- What needs to resolved during the implementation of this RFC?
- What related questions are beyond the scope of this RFC that should be addressed beyond its implementation?
- Specific formats for informational structures and tables on different platforms
- How will the assumptions of the kernel be specified/documented?