[seL4] Re: On Common IPC Patterns in Microkit

It is, albeit briefly :) "Of the threads eligible for scheduling, the highest priority thread in a runnable state is chosen.”

Ah okay thanks for pointing that out. I guess I was looking for something more explicit but it makes sense that the kernel manual would be talking about things more generally rather than specific things like ‘what happens if you signal’. Would you say all the properties of the scheduler are documented in the manual currently? If so I’ll start by reading it closely and seeing what applies to Microkit systems. Ivan