From c64867ebdff00c4c2fd3145560457269483a5cd4 Mon Sep 17 00:00:00 2001 From: Ben Leslie Date: Mon, 19 Apr 2021 05:22:03 +0000 Subject: [PATCH] Fix MCS / ARM64 VCPU interrupt interaction See: https://github.com/seL4/seL4/issues/346 for details. VPPIEvent and VGICMaintenance handling is updated to first check that the current thread has budget. If it does not have budget the interrupts are ignored. As interrupts are level-triggered this effectively just delays the interrupts. The check for budget is based on determining if the current thread is enqueued. This occurs if (and only if) the current thread has had a budget check that is expired. Signed-off-by: Ben Leslie --- src/arch/arm/object/vcpu.c | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/arch/arm/object/vcpu.c b/src/arch/arm/object/vcpu.c index 2e497ee94..997e6f238 100644 --- a/src/arch/arm/object/vcpu.c +++ b/src/arch/arm/object/vcpu.c @@ -109,6 +109,20 @@ void vcpu_restore(vcpu_t *vcpu) void VPPIEvent(irq_t irq) { +#ifdef CONFIG_KERNEL_MCS + /* If the current task is currently enqueued it will not be able to + * correctly receive a fault IPC message. This may occur due to the + * budget check that happens early in the handleInterruptEntry. + * + * If the current thread does *not* have budget this interrupt is + * ignored for now. As it is a level-triggered interrupt it shall + * be re-raised (and not lost). + */ + if (thread_state_get_tcbQueued(NODE_STATE(ksCurThread)->tcbState)) { + return; + } +#endif + if (ARCH_NODE_STATE(armHSVCPUActive)) { maskInterrupt(true, irq); assert(irqVPPIEventIndex(irq) != VPPIEventIRQ_invalid); @@ -129,6 +143,13 @@ void VGICMaintenance(void) uint32_t eisr0, eisr1; uint32_t flags; +#ifdef CONFIG_KERNEL_MCS + /* See VPPIEvent for details on this check. */ + if (thread_state_get_tcbQueued(NODE_STATE(ksCurThread)->tcbState)) { + return; + } +#endif + /* We shouldn't get a VGICMaintenance interrupt while a VCPU isn't active, * but if one becomes pending before the VGIC is disabled we might get one * when returning to userlevel after disabling the current VCPU. In this