On 26 Nov 2024, at 03:18, Wanja.Zaeske--- via Devel <devel@sel4.systems> 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 Microkit Tutorial > introduces some of them implicitly (by requiring the user to apply them). At > some point Kent suggested to put the topic on the mailing list, so here we go > đ.
Hi Wanja, Constructive suggestions on improving the documentation are always welcome ;-) I guess the Microkit tutorial needs to strike a balance between being highly approachable (which is its prime objective) and guiding people in the right direction with complete information. Thatâs not trivial, and may require auxiliary documentation for the more advanced user. Also, at this time the Microkit documentation clearly doesnât attempt to be independent of the kernel documentation. (This *may* be a worthwhile goal eventually for those who really just require the much simpler Microkit abstractions, but you want to avoid repeating too much, as this creates consistency problems. Eg I donât think the Microkit docs should aim to replace the sDDF docs.) > When initially playing through the Microkit Tutorial, I assumed that the > budget/period of a protection domain were providing uninterrupted time-slots. > I was thus slightly surprised, when I found out that sending a notification > to a higher priority PD would immediately preempt my current PD. Now, this on > its own is not problematic, Gernot simply commented my mistake with "Yes, > priorities are observed". However: Itâs not only not problematic, itâs essential ;-) > When playing the Microkit tutorial, I understood the way to solve Part 2 > (Serial Server to Client Communication) to be as follows: > > * [serial server] write received char to shared buffer. > * [serial server] notify client. > * [client] read char from shared buffer. > > This is also the current approach found in the provided solution [1]. This > works in some (most!) cases, but it is not reliable. It could be that chars > get lost, due to the serial server overwriting the buffer before it was > consumed form the client. Keep in mind that this only mirrors what happens in hardware: If software doesn't consume input from the serial port quickly enough, youâll lose characters. 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. Importantly, sDDF drivers are, as far as possible, policy free. A direct implication of this is that buffering isnât the driverâs job, itâs policy that should be done in another component (separation of concerns). Meaning the driver just reflects the fact that input characters get lost if you donât consume them quickly enough. And loss can be prevented by appropriate assignment of priorities. The serial driver section in the sDDF document is right now mostly AWOL (as there are a number of others, Iâve got a bunch of device class specs sitting on my desk waiting to be reviewedâŚ) There is discussion of priorities in the general part of the sDDF doc: §4.3.1 specifies that the driver should be higher prio than the virtualiser, and §4.3.2 similarly says that the virt should be higher prio than the client. But there really needs to be more info on serial drivers. I repeat, more/better documentation is definitely a good idea (incl diagrams!). But itâs also important that this documentation is driven by (and reflective of) the principles behind the design, rather than being a collection of recipes. We need to help the developer to get the right mental model of the system. Outsiders like you can certainly help this progress. (We do the same with our students, but their ânoviceâ status tends to vanish rather quickly ;-) Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
