Explain scheduling better #18
Description
Some of the tutorial relies on a property of the seL4 MCS scheduler that a microkit_notify to a PD of higher priority will cause a context-switch.
This is implicit and should instead be explained or we should link to an appendix or something in the manual where we go into details of why this works in the first place.
Also budgets and periods need to be explained better, with diagrams.
Reasoning about MCS scheduling is not easy for beginners and so we have to provide something.