I don't understand why you don't just add a cmdline option instead, then you don't need a special Microkit loader for x86.

And why not add a dynamic loading bit to the Microkit init code instead of arcane machine description file and boot emulation?

ACK on d4ffd52 though, you could create a separate PR for that if you want.

I don't understand why you don't just add a cmdline option instead, then you don't need a special Microkit loader for x86.

This is what I did indeed initially: passing the address and size of the extra memory region as a command line argument. The drawback with this approach is that since the size of the memory region changes depending on what's in the image, nearly every rebuild means having to update these magic numbers in the grub config file. It's not only impractical but also quite brittle, and it feels wrong to have to keep track of internal details of the image outside of it. The benefit of this intermediate loader is that it embeds these magic numbers.

And why not add a dynamic loading bit to the Microkit init code instead of arcane machine description file and boot emulation?

Hmm I understand the appeal, but this would be quite a departure from the static system image concept of Microkit, wouldn't it? I'm not sure how such a system would even look like. Also dynamic sounds like something that would be much harder to prove.

Microkit currently very much relies on knowing the hardware at compile time (device trees) and emulating the boot process, that's what it does on all supported architectures. This port essentially does the same thing on x86_64.

The drawback with this approach is that since the size of the memory region changes depending on what's in the image, nearly every rebuild means having to update these magic numbers in the grub config file.

No? Just reserve a region plenty big enough, e.g. 8 MB, and you rarely have to update your GRUB config.

It's not only impractical but also quite brittle, and it feels wrong to have to keep track of internal details of the image outside of it. The benefit of this intermediate loader is that it embeds these magic numbers.

You could write a script that updates the GRUB config automatically, that would also make more sense than this chainloader approach. You need to update the binaries anyway, can as well update the cmdline too then if you don't want to waste any space.

Hmm I understand the appeal, but this would be quite a departure from the static system image concept of Microkit, wouldn't it?

The static image concept applies to what kind of seL4 system is created, not on what hardware it runs. It's fine to create the static seL4 caps/vspace/cnodes/etc. loader init stuff, but it should depend on the user system, not the x86 hardware it will run on. That is, mostly you can't assume a specific memory layout.

You have to think long-term. Microkit as it is can almost do live updates of the system image because of the SDK approach: All you need to do is revoke all the used untypes and load a new image.

I'm not sure how such a system would even look like. Also dynamic sounds like something that would be much harder to prove.

It means that instead of hard-coding assumptions, you do runtime detection instead. So that you don't need to recompile your software if you want to use a different COM port, for instance.

(Yes, I know the seL4 kernel doesn't do as much runtime detection as it could and has too many config options, but that's no excuse.)

Basically, whatever info you collect with microkit-x86-machine-dump, you collect in the Microkit loader instead, and expose it to software somehow so it can do the right thing.

Long-term Microkit should expose all unused untyped memory to the system in some way anyway, so it's easy to add dynamic features on top of a static Microkit system.

Microkit currently very much relies on knowing the hardware at compile time (device trees) and emulating the boot process, that's what it does on all supported architectures. This port essentially does the same thing on x86_64.

You are shoehorning the Arm approach onto x86, which makes no sense whatsoever. x86 has been binary compatible for 40 years, meaning you can run the same binary on different machines. There is no reason why the same seL4 binaries can't do the same, except if people like you make things unnecessarily difficult.

Aarch64 is moving in the same direction, by adopting UEFI and defining the system (although only for server hardware).

One huge advantage of Microkit is that the same SDK can be used for multiple programs without recompiling the kernel. Imagine how convenient it would be if you could run the same Microkit binaries on multiple machines! (And the same binary on QEMU.)

It's not only impractical but also quite brittle to recompile a Microkit image for every machine you want to run it on.