elfloader-tool

Elfloader

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.

ARM

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.

1. (EFI only) Elfloader is entered at _gnuefi_start entry point.
2. (EFI only) Elfloader relocates itself
3. Elfloader _start is called. This is in arch-arm/<arch_bitness>/crt0.S.
4. Elfloader initialises the driver framework, which enables UART/printf.
5. Elfloader loads the kernel, user image, and DTB, determining where the kernel needs to be mapped in memory.
6. If the kernel window overlaps the elfloader's code:
   • (AArch32 EFI only) the elfloader relocates itself. See relocate_below_kernel for a detailed explanation of the relocation logic.
   • (Other platforms) the elfloader aborts.
7. The elfloader resumes booting. If it relocated itself, it will re-initialise the driver model.
8. If the elfloader is in HYP mode but seL4 is not configured to support HYP, it will leave HYP mode.
9. The elfloader sets up the initial page tables for the kernel (see init_hyp_boot_vspace or init_boot_vspace).
10. If SMP is enabled, the elfloader boots all secondary cores.
11. The elfloader enables the MMU.
12. The elfloader launches seL4, passing information about the user image and the DTB.

Binary

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.

U-Boot

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).

ELF

The elfloader supports being executed as an ELF image (via bootelf in U-Boot or similar).

EFI

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.

RISC-V

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.

Driver framework

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);

UART

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).

Porting the elfloader

To ARM

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.

To RISC-V

TODO - it seems there's not actually that much that needs to be done on the elfloader side.