From c8ae3010bc8aeb64375b24694a0850e84d55d6ac Mon Sep 17 00:00:00 2001 From: Indan Zupancic Date: Thu, 9 Apr 2026 17:17:54 +0100 Subject: [PATCH] x86,SMP: Fix VMCheckBoundNotification IPI handling When a notification is bound to an IRQ that arrives on a different core than where the VCPU is running, x86 uses a special IPI to notify the other core about this. (For performance reasons you would try to avoid this setup. Nevertheless, it should work.) When an IpiRemoteCall_VMCheckBoundNotification arrives during a VM exit, the notification reply set by VMCheckBoundNotification() gets overwritten by the handleVmexit() reply, leading to lost notification events. This happens when VMCheckBoundNotification() gets called by the IPI handling code within NODE_LOCK_SYS. As there is no way to postpone the VM exit handling and the IPI code doesn't know whether it races with a VM exit, doing nothing if the current task is the target is the safest choice: Either the IPI itself caused a VM exit, or there was a VM exit happening already. To handle the first case, explicitly call VMCheckBoundNotification() in handleVmexit(). This must be done while holding the kernel lock, as the other core can release the lock any moment after it received our IPI reply. In the latter case, pending notifications will be detected and returned to user space by the next seL4_VMEnter() call. Fix tested by Alessandro Legnani. Resolves issue #1148. Signed-off-by: Indan Zupancic --- src/arch/x86/object/vcpu.c | 7 ++++--- src/arch/x86/smp/ipi.c | 7 ++++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/arch/x86/object/vcpu.c b/src/arch/x86/object/vcpu.c index cca0f13bb..a93e28b3e 100644 --- a/src/arch/x86/object/vcpu.c +++ b/src/arch/x86/object/vcpu.c @@ -1329,16 +1329,17 @@ exception_t handleVmexit(void) /* the basic exit reason is the bottom 16 bits of the exit reason field */ reason = vmread(VMX_DATA_EXIT_REASON) & MASK(16); if (reason == EXTERNAL_INTERRUPT) { + NODE_LOCK_IRQ(); if (vmx_feature_ack_on_exit) { - interrupt = vmread(VMX_DATA_EXIT_INTERRUPT_INFO); - ARCH_NODE_STATE(x86KScurInterrupt) = interrupt & 0xff; - NODE_LOCK_IRQ_IF(interrupt != int_remote_call_ipi); + interrupt = vmread(VMX_DATA_EXIT_INTERRUPT_INFO) & 0xff; + ARCH_NODE_STATE(x86KScurInterrupt) = interrupt; handleInterruptEntry(); } else { /* poll for the pending irq. We will then handle it once we return back * up to restore_user_context */ receivePendingIRQ(); } + VMCheckBoundNotification(NODE_STATE(ksCurThread)); return EXCEPTION_NONE; } diff --git a/src/arch/x86/smp/ipi.c b/src/arch/x86/smp/ipi.c index e979bb5ce..ae07686e8 100644 --- a/src/arch/x86/smp/ipi.c +++ b/src/arch/x86/smp/ipi.c @@ -46,7 +46,12 @@ void handleRemoteCall(IpiRemoteCall_t call, word_t arg0, word_t arg1, word_t arg clearCurrentVCPU(); break; case IpiRemoteCall_VMCheckBoundNotification: - VMCheckBoundNotification((tcb_t *)arg0); + tcb_t *tcb = (tcb_t *)arg0; + + /* For a running VM notifications are already checked by handleVmexit */ + if (tcb != NODE_STATE(ksCurThread)) { + VMCheckBoundNotification(); + } break; #endif default: