In general I will say that that the Microkit manual and tutorial could be improved to give people a better mental model around how scheduling works on Microkit and the MCS version of seL4.
I think, there is a finite number of relevant IPC scenarios. Maybe one can build a tool to verify them (something something Promela?) and display them graphically (something something PlantUML Timing Diagrams?). This could either be used to fill a chapter in the Microkit Manual ("Common IPC Patterns, their Behavior and Pitfalls"?), or exposed as small (Web?) GUI Tool. Maybe this could become part of a student thesis even?
The main hurdle I’ve found with reasoning about how things are going to get scheduled in seL4 (although this problem is probably not unique to seL4) is that the answer is often ‘it depends on the rest of the system’. So, having a bunch of properties/rules that people can refer to quickly might not actually be realistic or it may actually be misleading. For example, the 2 UML diagrams that you linked look fairly different depending on whether you’re on single-core or multi-core. I think the first step would be to actually understand all the properties of the scheduler, for example the property mentioned about signalling to a higher priority PD is not documented in the seL4 kernel manual (from my brief reading of the scheduling section, I might be wrong). This makes me think about what other properties are missing from the kernel manual.
The other key thing to keep in mind (and maybe this needs to be emphasised more in the Microkit documentation) is that the core idea behind the seL4 device driver framework (sDDF) is that the driver has one and only one job: translating a hardware-specific *device* interface to a hardware-independent *device class* interface. Meaning an sDDF driver *only* provides a minimal hardware abstraction. This a great enabler of simplicity of sDDF drivers, making them a fraction of the size of Linux drivers, and easy to write.
The Microkit tutorial implements a very basic serial driver, it is not based on sDDF.
I hope the above might spark some thought on improving accessibility of Microkit.
I’ve made [1] but I’m not sure when I’ll get around to it. [1]: https://github.com/au-ts/microkit_tutorial/issues/18 Ivan