Pre-RFC: Build interface

RFC discussion
1

Summary

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.

Motivation

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.

Guide-level explanation

The process of generating a bootable image for a seL4-based project should generalise cleanly to the following:

  1. Project build system generates an encoded build configuration
  2. Kernel build system takes configuration and produces a kernel image, libesel4 binary, and libsel4 header
  3. Project build system takes configuration and produces a user-level application image
  4. 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.

Reference-level explanation

Currently, the kernel build system used to build a user-level image is split across seL4, seL4_tools, and riscv-pk.

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 seL4_tools, and riscv-pk.

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.

Drawbacks

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.

Prior art

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.

Unresolved questions

  • 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-pk into the git repository?
  • How is the configuration space defined?
2

I’m in two minds on this now. The discussion on RFC-6 indicated to me that I was trying to introduce unnecessary policy, when what I actually want is less policy.

I would be very happy with a kernel build system that can output (for a given configuration):

  • kernel ELF file
  • libsel4.a [I actually think this can go away and we have a header only library, but that’s a topic for a different RFC].
  • libsel4 include directory

If this can be done by just using git to grab a single repo at a specific tag/branch without needing other that would be ideal.

Despite what I had proposed in RFC-6 I think I’d be very happy without including elfloader (or similar) as part of this. My reasoning here is that I think there are different approaches that can be used for this loader step (and indeed I ended up writing an alternate loader for a project rather than using elfloader). I don’t think the loader and kernel need be tightly coupled.

So, specifically, I think it would be ideal for the kernel build system to address #2 and leave #1, #3 and #4 to the project.

The kernel build system can currently be used to build a kernel image from a configuration specified with command line arguments to CMake

Is there an exact example of this? The example on the website is for the pre-canned configurations. I was able to get a cmake only build working by moving some code around a little bit, but I fully admit that could be due to my lack of detailed knowledge of CMake.

3

I would prefer that the project be responsible for providing a loader, but without a well defined interface for that loader to start the kernel, that’s difficult actually work in practice. If the boot interface proposal gets enough interest to look like it will resolve this then I’d prefer to change this proposal.

For building the kernel standalone, you should be able to initialise a CMake build directory with the source path being specific as the kernel source directory.

mkdir build
cd build
cmake -G Ninja -S /path/to/seL4 .
ninja
4

I very much like the boot interface proposal although I haven’t had time to read all the details and comment yet.

I think there is an existing boot interface in practise, and it would be possible to document that as-is, without having to have the new boot interface as a gating item for this proposal.

5

@kent.mcleod suggests that the actual sequence should be as follows for newer versions of CMake

mkdir build
cd build
cmake \
    -G Ninja \
    -DKernelPlatform=${PLATFORM} \
    -C ${SEL4_PATH}/configs/seL4Config.cmake \
    -S ${SEL4_PATH} \
    -B . 
ninja kernel.elf

And for older versions that don’t support the -B, -S, or -C arguments, a file similar to the following is needed:

/** BUILD_CMAKE_PATH **/

list(APPEND CMAKE_MODULE_PATH ${CMAKE_CURRENT_LIST_DIR})
find_package(seL4 REQUIRED)
sel4_configure_platform_settings()
project(sel4core C ASM)
sel4_import_kernel()
sel4_import_libsel4()

With the following alternate command

mkdir build
cd build
cmake \
    -G Ninja \
    -DCMAKE_MODULE_PATH=${BUILD_CMAKE_PATH} \
    -DKernelPlatform=${PLATFORM} \
    ${SEL4_PATH} 
ninja kernel.elf
6

@kent.mcleod suggests that the actual sequence should be as follows for newer versions of CMake

These examples shouldn’t require any modifications to the current seL4/sel4 repository.
For older versions of CMake the sequence would still work but requires CMake to be in the build directory. So it would work with:

mkdir build
cd build
cmake \
    -G Ninja \
    -DKernelPlatform=${PLATFORM} \
    -C ${SEL4_PATH}/configs/seL4Config.cmake \
    ${SEL4_PATH}
ninja kernel.elf

My second example was if you needed to also build libsel4.a as the first example only includes the kernel build files:

/** In some source directory or generated location: CMAKE_TEMP_PATH **/
cmake_minimum_required(VERSION 3.13)

find_package(seL4 REQUIRED)
sel4_configure_platform_settings()
project(sel4core C ASM)
sel4_import_kernel()
sel4_import_libsel4()

mkdir build
cd build
cmake \
    -G Ninja \
    -DCMAKE_MODULE_PATH=${SEL4_PATH} \
    -DKernelPlatform=${PLATFORM} \
    ${CMAKE_TEMP_PATH} 
ninja kernel.elf libsel4.a
7

There are 2 PRs up for supporting standard CMake patterns for building and installing the kernel and libsel4 headers/sources:

This would allow you to build and install with:

cmake -G Ninja -DCMAKE_INSTALL_PREFIX=<path-to-install> -DKernelPlatform=imx6 <src-dir>
cmake --build .
cmake --install .

This will install the following files:

./bin/kernel.elf: Location of kernel.elf binary
./kernel_Config/include: The include root for the kernel_Config
interface library
./libsel4/include: The include root for libsel4
./libsel4/src: The c source files for the libsel4 library
./libsel4/sel4_Config/include: The include root for the sel4_Config
interface library
./libsel4/autoconf/include: The include root for the autoconf interface
library

This isn’t enough information to be able to import an installed kernel back into another CMake project or to build the elfloader from, but should be enough for what @bennoleslie was asking for.

There’s also an issue on GH for tracking what additional items would need to be installed to support building the elfloader or using CMake on top: What needs to be exported when installing a kernel CMakeLists project? · Issue #411 · seL4/seL4 · GitHub

I’m currently looking for feedback on all of the above. I’ve got implementations for what I listed under the issue, but wanted to give space for discussion before looking to get it all merged.

8

The conversation got splintered. FWIW I have followed up directly on #410. Short answer is I like it, let’s get it merged! I have some minor additional requests that you can find over there. I’ll keep the rest of my comments on github.