> Not documented on the seL4 manual
It is, albeit briefly :) "Of the threads eligible for scheduling, the
highest priority thread in a runnable state is chosen."
It would be appropriate for the tutorial to note the expected change
in the scheduler state, as this can be unexpected when one is first
working with seL4 or a similar priority based system (including
SCHED_FIFO and friends in POSIX).
Cheers
Anna.
On Wed, Nov 27, 2024 at 10:08 AM Ivan Velickovic via Devel
<devel@sel4.systems> wrote:
>
> 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
> _______________________________________________
> Devel mailing list -- devel@sel4.systems
> To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
