seL4
Add support for static X86_64 targets
This PR adds support for x86_64 hardware, with a QEMU emulated machine and an Odroid H2+ board as reference targets. X86 is quite a different beast compared to ARM and RISCV, so a few things to note about this port:
No device tree
On x86 we typically don't have a convenient device tree file describing the target and available at compile time. Instead the hardware is discovered at runtime by walking the ACPI tables, quering arcane BIOS ROMs, and sometimes by poking known memory addresses. The Microkit tool needs to emulate the seL4 boot on the target so we need to know some things about the target at compile time to build an image.
We do this by providing a machine description file to the Microkit tool when building x86 images. This is a simple JSON file that can be produced in various ways. Currently we use the bootable Microkit x86 Machine Dump tool that is run on the target board and produces the JSON file on a serial port. The boards that we target typically have serial ports, either physical or remotely accessible via the BMC/IPMI, so this simple tool covers our needs.
The example boards come with the machine.json files.
Boot protocol
The Microkit loader populates a region of memory with the contents of the PDs and passes this region to the seL4 kernel to be marked as device memory. On ARM and RISCV this region is passed via two extra registers when jumping to the seL4 entry point.
On x86 the kernel follows the multiboot boot protocol and generally use the popular GNU GRUB bootloader, alleviating the need for an ELF loader. The bootloader enables protected mode (32-bit) with a flat 1:1 memory map. We pass the extra memory region with the PDs to the kernel via a custom multiboot tag. This requires very few changes to the seL4 kernel code and fits nicely with the boot code. Since the bootloader can directly load 32-bit ELF files, the system image is packed as an ELF32 binary with the seL4 kernel and all PDs as segments, letting the bootloader do the work. The x86 Microkit loader therefore does not actually load anything: it only adds a tag to the multiboot tables received from the bootloader and jumps into the kernel entry point.
No VMMs
Virtualisation is a bit different on X86_64 and ARM. This commit does not support virtualisation on x86_64.
And the matching PR for the changes to the seL4 kernel: https://github.com/seL4/seL4/pull/1340
We've rebased this work onto the latest main commit of Microkit here as an interim x86 solution until something better is worked out. The rebased version fixed a few bugs and implements VM Fault printing on x86. To compile, use this version of seL4.
The main problem to get this merged is how the loading works.
To my understanding, the approach of having one image that then unpacks the kernel, initial task, and PD data works for ARM and RISC-V but not for x86. I don't think we would be able to boot most of our platforms at TS using this way. I think this is shown also by the fact that a script must be run first before you can boot on QEMU as well.
One potential solution to look into is appending the PD data to the monitor and having its initialisation process slightly differ so that it reads from that memory instead of device memory. This would mean we do not have to make patches to the kernel as well.
Sorry for the very late response. I agree, something like this would be the best approach to solve the loading problem. The cherry on the cake would be to use the CapDL loader as Microkit loader, since that's pretty much what it's designed to do. At this point it would make sense to use the CapDL loader for ARM and RISC-V as well, that would remove the per-arch deltas in the Microkit tool. That's a somewhat bigger scope though.
Do you have time/resources to look into alternative solutions for booting?
Unfortunately no, we do not have the resources to continue this Microkit port. The funding that was allocated to this work has abruptly ended. Whomever want to pick it up please feel free to do so, it's open-source of course, and I'd be personally happy if some of this gets upstreamed eventually.
I'm just learning about seL4, so I'm not sure how useful this would be, but for boot loaders an alternative you may wish to look into is Limine. Limine supports x86/x64, Aarch64 and RISC-V, and it will handle all the loading/booting into long mode for you. It does require a higher-half kernel though. However, Limine will give you access to all of the tables and the systems memory map (among many other things), and then all you have to do is walk the ACPI tables to find the MCFG table (if I remember right) for PCIe.
Hi @matneutrality, https://github.com/seL4/microkit/pull/337 adds support for x86-64. Through the transition to using capDL, knowing the physical memory layout on x86 at build time is not required with those changes.
Thanks for giving us a starting point for x86-64 support and apologies that it took us so long to get around to doing this.
