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: