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.)