Microkit x86

[matneutrality]

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.

[matneutrality]

And the matching PR for the changes to the seL4 kernel: seL4/seL4#1340