The elfloader is responsible for preparing the hardware for seL4 on ARM and RISC-V. It loads the kernel and user image from an embedded CPIO archive, initialises secondary cores (if SMP is enabled), and sets up an initial set of page tables for the kernel.
On ARM platforms, the elfloader supports being booted in four ways: as a binary image, as a u-boot uImage, as an ELF file, and as an EFI executable. Each of these methods differs slightly. It can also provide seL4 with a DTB - either from the bootloader or included in the embedded CPIO archive.
_gnuefi_start
entry point._start
is called. This is in arch-arm/<arch_bitness>/crt0.S
.relocate_below_kernel
for a detailed explanation of the relocation logic.init_hyp_boot_vspace
or init_boot_vspace
).The elfloader expects to be executed with a base address as generated by the shoehorn
utility. You can determine the correct address for a given image by running
aarch64-linux-gnu-objdump -t elfloader/elfloader | grep _text
from the kernel build directory. The first field in the output contains the base address.
On aarch64, the elfloader will try and move itself to the right address, however, this will fail if the load address and the correct address are too close, as the relocation code will be overwritten.
It is also possible to override shoehorn
and hardcode a load address by setting IMAGE_START_ADDR in CMake.
The elfloader can be booted according to the Linux kernel's booting convention for ARM/ARM64. The DTB, if provided, will be passed to seL4 (which will then pass it to the root task).
The elfloader supports being executed as an ELF image (via bootelf
in U-Boot or similar).
The elfloader integrates EFI support based on the gnu-efi
project. It will relocate itself as appropriate, and supports loading a DTB from the EFI implementation.
The elfloader on RISC-V basically follows the ARM platforms. However, due to the lack of available platforms, only two ways are currently supported actively: building it as ELF file or binary image. In both cases the platform must provide a SBI implementation, which will be used by the elfloader for the log output channel and the multicore boot. The seL4 build system allows building OpenSBI
with the elfloader as payload. The bbl
Support has been dropped, because it is superseded by OpenSBI
.
The elfloader provides a driver framework to reduce code duplication between platforms. Currently the driver framework is only used for UART output, however it is designed with extensibility in mind. In practice, this is currently only used on ARM, as RISC-V uses SBI for UART, and SBI has no device tree entries. However, in the future it may become useful on RISC-V.
The driver framework uses a header file containing a list of devices generated by the hardware_gen.py
utility included in seL4. Currently, this header only includes the UART specified by the stdout-path
property in the DTB. Each device in the list has a compatible string (compat
), and a list of addresses (region_bases[]
) which correspond to the regions specified by the reg
property in the DTB.
Each driver in the elfloader has a list of compatible strings, matching those found in the device tree. For instance, the 8250 UART driver, used on Tegra and TI platforms has the following:
static const struct dtb_match_table uart_8250_matches[] = { { .compatible = "nvidia,tegra20-uart" }, { .compatible = "ti,omap3-uart" }, { .compatible = "snps,dw-apb-uart" }, { .compatible = NULL /* sentinel */ }, };
Each driver also has a ‘type’. Currently the only type supported is DRIVER_UART
. The type
indicates the type of struct that is found in the ops
pointer of each driver object, and provides type-specific functionality. (For instance, UART drivers have a elfloader_uart_ops
struct which contains a putc
function). Finally, drivers also provide an init
function, which is called when the driver is matched with a device, and can be used to perform device-specific setup (e.g. setting the device as the UART output).
Finally, each driver has a struct elfloader_driver
and a corresponding ELFLOADER_DRIVER
statement. Taking the 8250 UART driver as an example again:
static const struct elfloader_driver uart_8250 = { .match_table = uart_8250_matches, .type = DRIVER_UART, .init = &uart_8250_init, .ops = &uart_8250_ops, }; ELFLOADER_DRIVER(uart_8250);
The driver framework provides a “default” (__attribute__((weak))
) implementation of plat_console_putchar
, which calls the putc
function for the elfloader device provided to uart_set_out
- discarding all characters that are given to it before uart_set_out
is called. This can be overridden if you do not wish to use the driver framework (e.g. for very early debugging).
Once a kernel port has been started (and a DTB provided), porting the elfloader to a platform is reasonably straightforward.
Most platform-specific information is extracted from a DTB, including available physical memory ranges. If the platform uses a UART compatible with another platform, even the UART will work out of the box. In other cases, it might be necessary to add a new dtb_match_table
entry to an existing driver, or add a new driver (which is fairly trivial - only the match_table
and putchar
functions from an existing driver would need to be changed).
An appropriate image type needs to be selected. By default ElfloaderImage
is set to elf
, however, various platform-specific overrides exist and can be found in ApplyData61ElfLoaderSettings
in this repo, at cmake-tool/helpers/application_settings.cmake
.
TODO - it seems there's not actually that much that needs to be done on the elfloader side.