For SMP seL4, the kernel uses a CLH lock. This is a FIFO lock which treats all of the cores as equal. Every core should eventually be scheduled.
However, I’m currently running MULTICORE0004 on 8 cores and it’s been running for over 16 minutes. Either there’s a bug somewhere, or it’s just completely stuck with bus contention. While thinking about this I realised that low-prio threads on some cores can basically DOS high-prio threads on other cores.
So my question here is, should the kernel lock respect priorities?
Bonus question, on MCS, what happens if a thread consumes it’s entire budget spinning on the lock? Notionally for real-time systems you can calculate the locking bound offline, but this doesn’t make that much sense for a mixed criticality system.
This isn’t as easy to answer as it seems. We have a partitioned scheduling model, which means that priority assignments on different cores are independent of each other. It doesn’t make much sense to say that thread A on core 0 has higher prio than thread B on core 1.
I suspect that FIFO is a reasonable locking policy under those circumstances, at least it allows (in principle) reasoning about worst-case blocking time.
In practice this would mean that our notion of preemption points would not only have to check for interrupts but also for pending lockers from other cores (which we don’t have ATM).