Hello,
the time spend by a vCPU TCB (tcbTimeSlice) seems to be not
accounted/updated by the seL4 kernel on a timer ticks, which leads to
starvation of other TCBs running on the same or lower priority level.
In one of our test setups, if once a vCPU runs and doesn't give up its
timeslice willful (e.g. guest goes in while loop and thereby not causing
a VM exit to be handled by the VMM), all other TCBs (normal threads and
vCPUs) on the same timeslice are not considered to be scheduled again,
since tcbTimeSlice of the vCPU stays full forever.
Following patch seems to fix the issue. Can you please have a look and
verify that it is correct ? Or should it be solved on another place in
the kernel differently.
Just out of curiosity, why is a separate thread state in the scheduler
for x86 (CONFIG_VFX) required that is not needed for scheduling of a
vCPU on ARM ? I didn't expect the scheduler thread states to be
different between hardware architectures in seL4.
Cheers,
--
Alexander Boettcher
Genode Labs
https://www.genode-labs.com - https://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 2b98c80..966276b 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -437,8 +437,11 @@ scheduleTCB(tcb_t *tptr)
void
timerTick(void)
{
- if (likely(thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState) ==
- ThreadState_Running)) {
+ switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState)) {
+ case ThreadState_Running:
+#ifdef CONFIG_VTX
+ case ThreadState_RunningVM:
+#endif
if (NODE_STATE(ksCurThread)->tcbTimeSlice > 1) {
NODE_STATE(ksCurThread)->tcbTimeSlice--;
} else {
@@ -446,6 +449,10 @@ timerTick(void)
SCHED_APPEND_CURRENT_TCB;
rescheduleRequired();
}
+ break;
+ default:
+ /* no tick updates */
+ break;
}
if (CONFIG_NUM_DOMAINS > 1) {
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
