This proposes to introduce a well-defined process for generating a kernel image for a given configuration as well as producing a bootable image from a kernel image and user-level image.
The discussion for RFC-6 highlighted the need for a means to integrate the building of seL4 into other build systems. Presently, it is essentially impossible to construct a project that produces a bootable user-level image that doesn’t tightly integrate into the CMake build system used to build the kernel itself and the seL4-based projects maintained by the seL4 Foundation.
It is desirable for a system to be constructed on seL4 that is independent from the build system that only depends on the build system of the kernel to the extent that it produces a kernel for a given configuration and a user-level image from a kernel image and user-level image.
For certain use cases, it may be preferable to distribute a compiled binary of a particular verified kernel configuration and boot stage binary.
The process of generating a bootable image for a seL4-based project should generalise cleanly to the following:
- Project build system generates an encoded build configuration
- Kernel build system takes configuration and produces a kernel image, libesel4 binary, and libsel4 header
- Project build system takes configuration and produces a user-level application image
- Kernel build system takes configuration, kernel image, and user-level application image and produces a bootable image.
For some cases it may be preferable to depend on distributed binaries as much as possible, such as when a binary-verified configuration is targeted. In this case, the configuration would be supplied with the pre-compiled kernel with some components of the boot-stage of the distributed image also pre-compiled.
In addition to the above, the kernel build should be reproducable. For a kernel built with the same compiler, configuration, and source code version should produce an identical binary file.
The build system that generates the kernel and bootable image will be provided as both a git repository and, for future release versions, a tarball. Binary releases will be provided for each future release version of the kernel as tarballs.
All actively-maintained seL4 Foundation projects will be updated to utilise this build interface to ensure it is tested and maintained.
The kernel build system can currently be used to build a kernel image from a configuration specified with command line arguments to CMake, however utilising the tools needed to construct a bootable image requires the construction of a broader CMake build system that utilises the components available in
After this change, only the
seL4 will be required to build both the kernel and user-level image. The build system will accept an encoded kernel configuration that includes the expected path of the generated user image. The build system can then be invoked to produce the
libsel4 library binary and headers needed to build a user-level image. It can then be invoked separately to produce the kernel image, and then finally again to take the built kernel image and user-level binary to produce a bootable image.
This tightly couples the kernel and the pre-boot software that executed prior to the kernel. It also prevents the choice of alternative implementations of bootloaders and pre-kernel boot software. This also forces a user-level image to be chosen at build-time rather than allowing a user-level image to be chosen at boot time without needing to recompile the image with the kernel for each user-level image that may be used.
Rationale and alternatives
An alternative may be to provide a distinct repository that provides an encapsulated build system for producing a bootable image.
- This would allow separate implementations of tools providing such bootable images
- This would require a well defined interface between the tools producing boot images and the kernel image defining the boot and firmware interfaces of the kernel; the boot interface is not currently well defined and the firmware interface may be defined by the bootloader in use
- This would require any boot interface to be defined and implemented directly in the binary of the kernel rather than in a pre-boot stage implemented in a component of the bootable image
The current construction of the kernel for arm and RISC-V results in the kernel depending on
elfloader to initialise the system and start additional cores with the minimal amount of work occuring in the kernel image itself before boot (essentially only generating the initial capabilities and task). The x86 implementation of the kernel depends on multiboot to boot the first core with the kernel being responsible for starting further cores.
Until a well-defined boot interface exists, it makes little material difference as to whether a component such as
elfloader is packaged with the kernel or externally as it is effectively the only option for starting an seL4 system on the platforms for which it is used. Given that the choice of boot image tool does not effectively exist, splitting the two is of no benefit.
Most other kernels can be compiled and used in a manner that doesn’t require user-level software to be built using an extension of the kernel’s build system.
- How is a kernel configuration encoded?
- Potentially just a sorted list of CMake command-line options
- Should the build systems for the kernel and bootable image be configured separately?
- How do we incorporate
riscv-pkinto the git repository?
- How is the configuration space defined?