On Tue, Jul 23, 2024, 8:15 PM Gerwin Klein via Devel
If the first thread is round-robin, that means it is always the highest priority thread as soon as it gets started, and the second thread never gets started at all, because the sel4test setup thread does not run any more (since the first thread is always ready).
Keeping the setup thread priority high until after both round-robin threads are started (and then dropping it) shows the correct round robin behaviour for me.
I noticed a similar issue, but I have all the threads at the same priority and the scheduler seems to be behaving more like a FIFO scheduler than a round-robin one. I haven't actually looked at the scheduler code all that much yet so I'm not quite sure what's going on. I am using a fork rather than seL4 itself, but this was happening before I started making major changes.