Skip to content

Conversation

@matneutrality
Copy link

This PR adds support for x86_64 targets.

This requires another PR in the seL4 repository to update the boot protocol.

While embedded ARM and RISC-V machines are wholly defined by Device Tree (DT) files, x86 machines typically discover the details of the hardware at boot time by querying ACPI tables and friends. For Microkit to build a system image for a given x86 machine we use the microkit-x86-machinedump tool on the target hardware to detect the hardware details and produce a JSON file that can be passed to Microkit.

Even when building natively (i.e. no cross compiling) the toolchain
can be called with its full prefix. We do no need to assume that the
host machine is an x86_64.

Signed-off-by: Mathieu Mirmont <[email protected]>
Build the libmicrokit for x86_64.

Signed-off-by: Mathieu Mirmont <[email protected]>
Build the monitor for x86_64.

Signed-off-by: Mathieu Mirmont <[email protected]>
The x86 boot protocol is sufficiently different from that of ARM and
RISC-V to justify making a custom loader.

Signed-off-by: Mathieu Mirmont <[email protected]>
First attempt at porting the microkit tool to x86_64. A notable change
is the x86 machine.json file that acts a bit like a DTB file for a
specific x86 board.

Signed-off-by: Mathieu Mirmont <[email protected]>
Match the seL4 kernel by removing the MSI region. For reference, the
comment in the kernel's platAddDevices() function says:

> Remove the MSI region as poking at this is undefined and may allow
> for the user to generate arbitrary MSI interrupts. Only need to
> consider this if it would actually be in the user device region

Signed-off-by: Mathieu Mirmont <[email protected]>
On x86 the kernel loads the inittask as a multiboot module and copies
it immediately after the kernel, followed by the reserved region. This
is different from what is done on ARM and RISC-V.

Signed-off-by: Mathieu Mirmont <[email protected]>
Somehow objects are created in different order on different platforms,
so on X86 the schedcontrol caps are created before the paging caps,
while on ARM it's the other way around. This difference changes the
capability index in the root CNode.

Signed-off-by: Mathieu Mirmont <[email protected]>
The seL4 kernel does not create untyped caps for memory regions
smaller than seL4_MinUntypedBits since they wouldn't be large enough
to be retyped into objects. This value is set to 4 on all
architectures so it is hardcoded for now.

Signed-off-by: Mathieu Mirmont <[email protected]>
Fix a copypasta between RISC-V and X86. The error was of no
consequence since in both case the value is set to 0.

Signed-off-by: Mathieu Mirmont <[email protected]>
Recent versions of grub reject ELF files without section header table
(i.e. sh_offset = 0). This is a bug in grub. As a workaround, add an
empty inactive section header to the generated ELF files.

Signed-off-by: Mathieu Mirmont <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant