> For example, the 2 UML diagrams that you linked look fairly different
> depending on whether you’re on single-core or multi-core.
Yes, and a diagram can be easily used to highlight
a) the critical chain of events for a successful communication,
b) which links in this chain are relying on sche
Hi Gernot,
thank you for the prompt and elaborate answer. A few quick comments
I fully agree with your stance on being approachable/guiding through the
Microkit Tutorial.
That's why I suggested not to solving the issue (e.g. by buffering) part of the
tutorial, but to mention that there might be
> 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 ge
> 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 fir
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
On 26 Nov 2024, at 03:18, Wanja.Zaeske--- via Devel wrote:
>
> Hi together,
>
> during the proceedings of the last seL4 summit I participated in a discussion
> about Microkit usability. In particular we were talking about common patterns
> for IPC in Microkit, potential pitfalls and how the Mi
