portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix MCS / ARM64 VCPU interrupt interaction

Browse source 
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 <benno@brkawy.com>
This commit is contained in:
Ben Leslie 2021-04-19 05:22:03 +00:00 committed by Gerwin Klein
parent 5fd9619fb5
commit c64867ebdf
1 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/arch/arm/object/vcpu.c
View file

@ -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