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.