libmicrokit: add API for resuming x86 VCPU

[dreamliner787-9]

Depends on seL4/seL4#1534, I've worked around this for now by including vmenter.h in libmicrokit/include/microkit.h.

Previously, the Microkit event handler had no mechanism on x86 to resume a vCPU while simultaneously waiting for an incoming notification. This PR adds microkit_vcpu_x86_deferred_resume() to libmicrokit, providing a cleaner way to integrate x86 vCPU resumption with the Microkit event handler.

Due to a kernel limitation in void NORETURN slowpath(syscall_t syscall) of src/arch/x86/c_traps.c, only the VMM's TCB bound Notification is checked for a pending Notification. An endpoint object can't passed to seL4_VMEnter() so PPCs won't work while the VCPU is running. Technically, PPCs still work if the VCPU isn't resumed, but I feel like we should not expose this footgun to users.

[midnightveil]

For the record: I'm not entirely convinced this is the best way the API could look/behave, it feels quite ugly.

[dreamliner787-9]

For the record: I'm not entirely convinced this is the best way the API could look/behave, it feels quite ugly.

Yes I agree, as discussed internally, there isn't a clean way to integrate the way virtualisation works on x86 seL4 with the Microkit event loop. Unless we allow the user to override the main() entrypoint and let the user call into the library in some way...

[Indanz]

For the record: I'm not entirely convinced this is the best way the API could look/behave, it feels quite ugly.

Yes I agree, as discussed internally, there isn't a clean way to integrate the way virtualisation works on x86 seL4 with the Microkit event loop.

Why can't the Microkit event loop be x86 virtualisation aware? Or have a x86 version of the event loop that calls VMEnter instead of recv. You can add a special function that enters this x86 virtualisation aware event loop and never returns. Then the user only needs to do one special call during init once. If the tooling is aware of all this, it could do this automatically on return of the init function too and the user wouldn't need to do anything special (other than being aware that a VCPU task runs both normal code and a VM).

[dreamliner787-9]

For the record: I'm not entirely convinced this is the best way the API could look/behave, it feels quite ugly.

Yes I agree, as discussed internally, there isn't a clean way to integrate the way virtualisation works on x86 seL4 with the Microkit event loop.

Why can't the Microkit event loop be x86 virtualisation aware? Or have a x86 version of the event loop that calls VMEnter instead of recv. You can add a special function that enters this x86 virtualisation aware event loop and never returns. Then the user only needs to do one special call during init once.

I've done some thinking on what you've said and I like it a lot. My take on your idea is that we will have one API that looks like:

static void microkit_x86_vcpu_on(uint64_t rip, uint64_t prim_proc_ctl, uint32_t irq_info)

The user calls this before returning from init() or notified() once during the PD's lifetime. This switches the normal event loop into a x86 virtualisation aware mode. Then the Microkit will automatically resume the VCPU as part of the event loop. No deferred calls like right now.

For argument passing to seL4_VMEnter(), that will be initially taken care of with this call. For subsequent VM exits due to notifications or faults, we can easily hook it to the existing read/write VMCS API. That is, any writes to the guest RIP, Primary Processor Controls or IRQ info get written to local variables, then it will be written to message registers right before the event loop calls seL4_VMEnter(). Rather than having to do a read/write VMCS syscall.

Under this model, the user just need to be aware that a PD with a VCPU will be executing guest code if init() or notified() returns and the PD get scheduled.

Edit: it maybe beneficial to have a microkit_x86_vcpu_off as well. So that this model is similar to the ARM's VCPU restart and stop APIs.

If the tooling is aware of all this, it could do this automatically on return of the init function too and the user wouldn't need to do anything special (other than being aware that a VCPU task runs both normal code and a VM).

This would be ideal, but VCPUs are resumed by user code at runtime so I'm unsure how this could fit in.

[Indanz]

If the tooling is aware of all this, it could do this automatically on return of the init function too and the user wouldn't need to do anything special (other than being aware that a VCPU task runs both normal code and a VM).

This would be ideal, but VCPUs are resumed by user code at runtime so I'm unsure how this could fit in.

Resuming a VCPU is just calling seL4_VMEnter(). That is no different from a code flow point of view than blocking on seL4_ReplyRecv(). Either can be called after return of the user callback function.

Considering x86 VCPU tasks can't receive IPC calls anyway, but only notifications, for Microkit it would make sense to model non-notification returns from VMEnter as Protected procedure calls. Or be more specific and add another callback function for those.

(I'm ignoring the practical implementation split between generic Microkit and libvm or whatever virtualisation aware code you have. For a more virtualisation agnostic Microkit it would help to move stuff more into libraries and less in the Microkit framework.)

[Indanz]

Doesn't that mean that you want to take that argument away from microkit_vcpu_x86_write_vmcs/microkit_vcpu_x86_read_vmcs too? (And any other x86 virtualisation functions there may be.)

[dreamliner787-9]

That's a good point, the reason why I haven't done that is because I don't know how VM with multiple VCPUs will look like yet, because there are multiple approaches you can take.

You could allow one VMM PD access to multiple VCPU caps to configure them and/or handle faults, i.e. you will have an implicit "big VMM lock". This is currently how ARM VM are modelled in Microkit. For x86, we will need additional trampoline threads that resume the VCPUs. The downside is that you have more context switching, but you would be able to replicate the ARM model. In this case we would need to pass microkit_child vcpu to all the VCPU APIs.

Or, you could adopt a "multi VMM" approach where each PD only have access 1 VCPU. Then the user is responsible for creating 1 PD per VCPU, handle IPIs with explicit channels between the PDs and synchronise access to any global VMM state themselves. This model would incur less context switching and there isn't a "big lock" like the previous one. But there are more complications: you would need to ensure that all the VMM PDs have access to the same resources (memory regions, interrupts, etc) for fault handling, and channels between the VMM PDs for every possible combinations of IPIs (n(n-1) channels). In this case we would not need to pass microkit_child vcpu to all the VCPU APIs.

Arguably the "multi VMM" approach is already possible on both ARM and x86 in Microkit. But at this point I'm not sure whether supporting the "big VMM lock" model on x86 is appropriate so I'm keeping the option open.

[Indanz]

What you say argues against dropping the parameter for microkit_vcpu_x86_on/off too though.

I strongly advise against some trampoline construction that shuffles all VCPU handling to one VMM task: The reason to have multiple VCPUs is to use multiple cores, so they all will be on different cores. If you handle all VCPUs with one VMM task, all operations become cross-core with huge overhead: First the fault/trap needs to be propagated to the core the VMM is on, and then any reply needs to be funnelled back.

The added value of handling multiple, independent virtual machines with one VMM is approximately zero.

This means that also on Arm, you do not want to use the model with one central VMM handling multiple VCPUs, even though it's simpler.

But there are more complications: you would need to ensure that all the VMM PDs have access to the same resources (memory regions, interrupts, etc) for fault handling,

Why? A VMM doesn't need access to the virtual machine's memory, interrupts etc.

and channels between the VMM PDs for every possible combinations of IPIs (n(n-1) channels).

Why do you need IPIs? Why would one VMM care about what others do?

If you need some kind of central control, then have a global VMM manager which communicates with all the VMMs handling VCPUs. Then you need only n channels and have only one decision point.

[Indanz]

Can't you at least group them together in a structure?

I would do that for all those global Microkit variables and put them all in one structure (and the vcpu ones in a substructure of that one). Then it's also easier to hide implementation details from the user, as you can do a forward declaration of the structure and hide the content.

[dreamliner787-9]

I will group the x86 VCPU ones in a structure, then we can do the other ones in a different PR.