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

Fix VGIC and VPPI maintenance handling

Browse source 
Fix a bug in VGIC Maintenance/VPPI logic that allowed a thread to be
simultaneously BlockedOnReply and in the release queue.

Co-authored-by: Alwin Joshy <joshyalwin@gmail.com>
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
This commit is contained in:
Krishnan Winter 2025-06-24 10:36:18 +10:00 committed by Indan Zupancic
parent dec87e641a
commit 6dbe58ef0c
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -110,11 +110,16 @@ void VPPIEvent(irq_t irq)
* 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 the current thread does *not* have budget, as indicated by its
* presence in the release queue, this interrupt is ignored for now.
* As it is a level-triggered interrupt it shall be re-raised
* (and not lost).
*
* Additionally, if we have already received a timeout fault due to
* 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 (thread_state_get_tcbQueued(NODE_STATE(ksCurThread)->tcbState)) {
if (!isSchedulable(NODE_STATE(ksCurThread))) {
return;
}
#endif
@ -141,7 +146,7 @@ void VGICMaintenance(void)
#ifdef CONFIG_KERNEL_MCS
/* See VPPIEvent for details on this check. */
if (thread_state_get_tcbQueued(NODE_STATE(ksCurThread)->tcbState)) {
if (!isSchedulable(NODE_STATE(ksCurThread))) {
return;
}
#endif