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

Fix MCS / ARM VCPU interrupt interaction, try 3

Browse source 
Restore the schedule queue check of commit c64867e from PR #352,
which was accidentally undone when adding a similar check for the
release queue in PR #1486.

Resolves issue #1645.

Signed-off-by: Indan Zupancic <indan@nul.nu>
This commit is contained in:
Indan Zupancic 2026-05-21 23:37:45 +01:00 committed by Gerwin Klein
parent ae11cf1450
commit 232471e90f
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -111,7 +111,8 @@ void VPPIEvent(irq_t irq)
* budget check that happens early in the handleInterruptEntry.
*
* If the current thread does *not* have budget, as indicated by its
* presence in the release queue, this interrupt is ignored for now.
* presence in either the scheduling or release queue, this interrupt
* is ignored for now.
* As it is a level-triggered interrupt it shall be re-raised
* (and not lost).
*
@ -119,7 +120,8 @@ void VPPIEvent(irq_t irq)
* our timeslice having ended, and we have a timeout fault handler for
* this thread, we do not want to overwrite that with our VCPU fault.
*/
if (!isSchedulable(NODE_STATE(ksCurThread))) {
if (thread_state_get_tcbQueued(NODE_STATE(ksCurThread)->tcbState) ||
!isSchedulable(NODE_STATE(ksCurThread))) {
return;
}
#endif
@ -146,7 +148,8 @@ void VGICMaintenance(void)
#ifdef CONFIG_KERNEL_MCS
/* See VPPIEvent for details on this check. */
if (!isSchedulable(NODE_STATE(ksCurThread))) {
if (thread_state_get_tcbQueued(NODE_STATE(ksCurThread)->tcbState) ||
!isSchedulable(NODE_STATE(ksCurThread))) {
return;
}
#endif