Hello Liam, On 2024-07-22 14:56, liam.vervecken@gmail.com wrote:
But it seems instead only the first thread gets scheduled, and it never allows the second thread to get any CPU time.
This could happen if the port is broken and you don't get any timer interrupts. To verify if this is happening, you could add a debug print to getActiveIRQ() in src/arch/riscv/machine/hardware.c at line 117 where it set irq = KERNEL_TIMER_IRQ;
I found that if I call seL4_SchedContext_Consumed(sched_context_thread) periodically in the threads they will switch if the budget has expired. It doesn't make much sense to me why this is the case, I thought they would switch automatically once their budget is expired and that seL4_SchedContext_Consumed() was simply used to keep track of this. I'm hoping it can offer some clue as to what I'm doing wrong.
Calling most system calls should have the same effect, as the kernel does a time and budget check for all non-fastpath syscalls. Greetings, Indan