Skip to content

libmicrokit: add microkit_vcpu_x86_deferred_resume() call #431

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dreamliner787-9 wants to merge 2 commits into
base: main
Choose a base branch
from
Open

libmicrokit: add microkit_vcpu_x86_deferred_resume() call #431

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
112a7e9
libmicrokit: integrate x86 seL4_VMEnter()
dreamliner787-9 Mar 9, 2026
eaecb0d
manual: add microkit_vcpu_x86_deferred_resume
dreamliner787-9 Mar 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions docs/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -624,6 +624,13 @@ To find the full list of possible faults that could occur and details regarding
kind of fault, please see the 'Faults' section of the
[seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf).

For x86 VCPU fault specifically:
Only the `child` argument will contain a valid value. The return value of `fault()` is ignored. To resume a VCPU from
a fault, `fault()` must call `microkit_vcpu_x86_deferred_resume()` with the intended values before returning.

To deduce the VM Exit reason, read the `SEL4_VMENTER_FAULT_REASON_MR` message register. For more details,
please see the 'Virtualisation' section of the [seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf).

## `microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo)`

Performs a call to a protected procedure in a different PD.
Expand Down Expand Up @@ -958,6 +965,15 @@ virtual CPU with ID `vcpu`.
Write the registers of a given virtual CPU with ID `vcpu`. The `regs` argument is the pointer to
the struct of registers `seL4_VCPUContext` that are written from.

## `void microkit_vcpu_x86_deferred_resume(seL4_Word rip, seL4_Word ppc, seL4_Word irq)`

Resume the bound vCPU when current execution returns to libmicrokit's event handler (see [Internals](#Internals)).
It switches the PD's thread from regular execution mode into the guest execution mode whenever it is scheduled thereafter.

This will set the program counter of the vCPU to `entry_point`, the Primary Processor-Based VM-Execution Controls to `ppc`
and the VM-Entry Interruption-Information Field to `irq`. Any previous value of these vCPU fields set by
`microkit_vcpu_x86_write_vmcs()` will be overwritten.

# System Description File {#sysdesc}

This section describes the format of the System Description File (SDF).
Expand Down
33 changes: 20 additions & 13 deletions libmicrokit/include/microkit.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,12 @@ extern char microkit_name[MICROKIT_PD_NAME_LENGTH];
extern seL4_Bool microkit_have_signal;
extern seL4_CPtr microkit_signal_cap;
extern seL4_MessageInfo_t microkit_signal_msg;
#if defined(CONFIG_VTX)
extern seL4_Bool microkit_x86_do_vcpu_resume;
extern seL4_Word microkit_x86_vcpu_resume_rip;
extern seL4_Word microkit_x86_vcpu_resume_ppc;
extern seL4_Word microkit_x86_vcpu_resume_irq;
#endif

/* Symbols for error checking libmicrokit API calls. Patched by the Microkit tool
* to set bits corresponding to valid channels for this PD. */
Expand Down Expand Up @@ -188,13 +194,8 @@ static inline void microkit_vcpu_restart(microkit_child vcpu, seL4_Word entry_po
{
seL4_Error err;
seL4_UserContext ctxt = {0};
#if defined(CONFIG_ARCH_AARCH64)
ctxt.pc = entry_point;
#elif defined(CONFIG_ARCH_X86_64)
ctxt.rip = entry_point;
#else
#error "unknown architecture for 'microkit_vcpu_restart'"
#endif

err = seL4_TCB_WriteRegisters(
BASE_VM_TCB_CAP + vcpu,
seL4_True,
Expand All @@ -218,9 +219,7 @@ static inline void microkit_vcpu_stop(microkit_child vcpu)
microkit_internal_crash(err);
}
}
#endif

#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
static inline void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq, seL4_Uint8 priority,
seL4_Uint8 group, seL4_Uint8 index)
{
Expand Down Expand Up @@ -263,7 +262,7 @@ static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word re
microkit_internal_crash(err);
}
}
#endif
#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */

#if defined(CONFIG_ALLOW_SMC_CALLS)
static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMCContext *response)
Expand All @@ -275,7 +274,7 @@ static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMC
microkit_internal_crash(err);
}
}
#endif
#endif /* CONFIG_ALLOW_SMC_CALLS */

#if defined(CONFIG_ARCH_X86_64)
static inline void microkit_x86_ioport_write_8(microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word data)
Expand Down Expand Up @@ -391,9 +390,8 @@ static inline seL4_Uint32 microkit_x86_ioport_read_32(microkit_ioport ioport_id,

return ret.result;
}
#endif

#if defined(CONFIG_ARCH_X86_64) && defined(CONFIG_VTX)
#if defined(CONFIG_VTX)
static inline seL4_Word microkit_vcpu_x86_read_vmcs(microkit_child vcpu, seL4_Word field)
{
seL4_X86_VCPU_ReadVMCS_t ret;
Expand Down Expand Up @@ -477,7 +475,16 @@ static inline void microkit_vcpu_x86_write_regs(microkit_child vcpu, seL4_VCPUCo
}
}

#endif
static inline void microkit_vcpu_x86_deferred_resume(seL4_Word rip, seL4_Word ppc, seL4_Word irq) {
/* On x86, a TCB can only have one bound VCPU at any given time.
* So we don't take a `microkit_child vcpu` here. */
microkit_x86_do_vcpu_resume = seL4_True;
microkit_x86_vcpu_resume_rip = rip;
microkit_x86_vcpu_resume_ppc = ppc;
microkit_x86_vcpu_resume_irq = irq;
}
#endif /* CONFIG_VTX */
#endif /* CONFIG_ARCH_X86_64 */

static inline void microkit_deferred_notify(microkit_channel ch)
{
Expand Down
75 changes: 68 additions & 7 deletions libmicrokit/src/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,13 @@ seL4_Bool microkit_have_signal = seL4_False;
seL4_CPtr microkit_signal_cap;
seL4_MessageInfo_t microkit_signal_msg;

#if defined(CONFIG_VTX)
seL4_Bool microkit_x86_do_vcpu_resume = seL4_False;
seL4_Word microkit_x86_vcpu_resume_rip;
seL4_Word microkit_x86_vcpu_resume_ppc; /* "Primary Processor-Based VM-Execution Controls" */
seL4_Word microkit_x86_vcpu_resume_irq; /* "VM-Entry Interruption-Information Field" */
#endif /* CONFIG_VTX */

seL4_Word microkit_irqs;
seL4_Word microkit_notifications;
seL4_Word microkit_pps;
Expand Down Expand Up @@ -63,6 +70,18 @@ static void run_init_funcs(void)
}
}

static seL4_MessageInfo_t receive_event(bool have_reply, seL4_MessageInfo_t reply_tag, seL4_Word *badge)
{
if (have_reply) {
return seL4_ReplyRecv(INPUT_CAP, reply_tag, badge, REPLY_CAP);
} else if (microkit_have_signal) {
return seL4_NBSendRecv(microkit_signal_cap, microkit_signal_msg, INPUT_CAP, badge, REPLY_CAP);
microkit_have_signal = seL4_False;
} else {
return seL4_Recv(INPUT_CAP, badge, REPLY_CAP);
}
}

static void handler_loop(void)
{
bool have_reply = false;
Expand All @@ -89,25 +108,67 @@ static void handler_loop(void)
seL4_Word badge;
seL4_MessageInfo_t tag;

if (have_reply) {
tag = seL4_ReplyRecv(INPUT_CAP, reply_tag, &badge, REPLY_CAP);
} else if (microkit_have_signal) {
tag = seL4_NBSendRecv(microkit_signal_cap, microkit_signal_msg, INPUT_CAP, &badge, REPLY_CAP);
microkit_have_signal = seL4_False;
#if defined(CONFIG_VTX)
seL4_Word x86_vmenter_result;
seL4_Bool x86_vmenter_result_valid = seL4_False;
if (microkit_x86_do_vcpu_resume) {
/* There isn't a syscall that atomically send signal or reply, perform vmenter while waiting for
incoming notifications. So we have to dispatch any signal or reply first. Then switch execution
to the bound VCPU. */
if (have_reply) {
seL4_Send(REPLY_CAP, reply_tag);
} else if (microkit_have_signal) {
seL4_NBSend(microkit_signal_cap, microkit_signal_msg);
}

microkit_mr_set(SEL4_VMENTER_CALL_EIP_MR, microkit_x86_vcpu_resume_rip);
microkit_mr_set(SEL4_VMENTER_CALL_CONTROL_PPC_MR, microkit_x86_vcpu_resume_ppc);
microkit_mr_set(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR, microkit_x86_vcpu_resume_irq);

x86_vmenter_result = seL4_VMEnter(&badge);

x86_vmenter_result_valid = seL4_True;
microkit_x86_do_vcpu_resume = seL4_False;
} else {
tag = seL4_Recv(INPUT_CAP, &badge, REPLY_CAP);
tag = receive_event(have_reply, reply_tag, &badge);
}
#else
tag = receive_event(have_reply, reply_tag, &badge);
#endif /* CONFIG_VTX */

uint64_t is_endpoint = badge >> 63;
uint64_t is_fault = (badge >> 62) & 1;

#if defined(CONFIG_VTX)
if (x86_vmenter_result_valid) {
if (x86_vmenter_result == SEL4_VMENTER_RESULT_FAULT) {
is_fault = 1;
tag = seL4_MessageInfo_new(0, 0, 0, 0);
} else if (x86_vmenter_result == SEL4_VMENTER_RESULT_NOTIF) {
/* VCPU was interrupted while executing from a notification. Saves the instruction pointer,
* Primary Processor-Based VM-Execution Controls and VM-Entry Interruption-Information Field.
* So we can resume automatically with the correct values on the next event loop iteration. */
microkit_vcpu_x86_deferred_resume(microkit_mr_get(SEL4_VMENTER_CALL_EIP_MR), microkit_mr_get(SEL4_VMENTER_CALL_CONTROL_PPC_MR), microkit_mr_get(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR));
}
}
#endif /* CONFIG_VTX */

have_reply = false;

if (is_fault) {
seL4_Bool reply_to_fault = fault(badge & PD_MASK, tag, &reply_tag);
if (reply_to_fault) {

#if defined(CONFIG_VTX)
if (x86_vmenter_result_valid == seL4_False && reply_to_fault == seL4_True) {
/* Fault from child PD rather than from bound VCPU */
have_reply = true;
}
#else
if (reply_to_fault == seL4_True) {
have_reply = true;
}
#endif /* CONFIG_VTX */

} else if (is_endpoint) {
have_reply = true;
reply_tag = protected(badge & CHANNEL_MASK, tag);
Expand Down
Loading