December 2024 - Devel - lists.sel4.systems

CDT traveling
by Yanfeng Liu 18 Dec '24

18 Dec '24

Dear experts, I am trying to understand the memory usage of a running seL4 demo with help of GDB. I am wondering how I can travel the Capability derivation tree starting from original untyped objects and see how memory are used. I noticed that `mdb_node_t` has `mdbPrev` and `mdbNext` pointer fields but not sure how can they be used to travel the capability derivation tree? Regards, yf

2 10

On Common IPC Patterns in Microkit
by Wanja.Zaeske＠dlr.de 16 Dec '24

16 Dec '24

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 😊. 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: 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. The specific details if this works depend upon the combination of: * Data size (not-so-critical with one byte, but more data means more time is required to consume the buffer form the client) * Budget/Period of the client (can the client read all data before it is preempted by exhaustion of its budget in the current period) * Hardware Performance (same as above) * Priorities (if the serial server is higher priority and gets triggered by another hardware event before the client can consume the char, it gets lost again) This is problematic: the details of the scheduling are not very explicit in the manual (roughly one half of a page), but the first example of IPC taught via the tutorial relies on a lot of implicit circumstance on how PDs are scheduled to function correctly. Now I have three suggestions to improve upon this. 1. In the tutorial, explicitly mention the possibility of using the same notification channel in the opposite direction for a read-ACK. If another serial interrupt comes, but no ACK was received, just log an error. The point is not, to introduce ring-buffers and a the machinery for robust communication -- that would like explode the scope for a simple tutorial. Rather, the point is to teach people that this IPC mechanism may silently fail (as in chars get dropped). 2. For certain scheduling + IPC scenarios, examples with a graphical representation would be good. Here are two examples: Sending data to a higher priority PD (via notifications + shared memory) [2] and sending data to a lower priority PD (via notification + shared memory + ACK notification) [3]. Please bear with me, my talent to intuitive graphical representation is of limited nature, this for sure could be made better looking. In the end, I'd like to have an engineer short on time quickly look up the current scenario (sharing data bi-/unidir?, other PD is strictly higher prio/lower prio?, silent loss of data tolerable or not?, ...) from a table, take a look at the timing diagram and pick the correct approach for the task at hand. Microkit does not provide very sophisticated IPC APIs, and that is good! It keeps Microkit small, and the API IMHO provides everything needed, for synchronous and asynchronous communication, for large and small data, ... But composing the IPC correctly is not trivial, so anything we can to take sharp edges of the experience without bloating the API should be considered. 3. 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? I hope the above might spark some thought on improving accessibility of Microkit. Kind Regards, Wanja [PlantUML diagram] [PlantUML diagram] [1] https://github.com/au-ts/microkit_tutorial/blob/6733b7864217831e4e77616647e… [2] https://www.plantuml.com/plantuml/uml/VL9DYzim4BthLppIGoxP49kwWHvADlHOIYc5F… [3] https://www.plantuml.com/plantuml/uml/XLDDYzim4BthLpnosKisnA4Ecq9BjlHOIkbbp… —————————————————————————— Deutsches Zentrum für Luft- und Raumfahrt (DLR) Institut für Flugsystemtechnik | Sichere Systeme & Systems Engineering | Lilienthalplatz 7 | 38108 Braunschweig Wanja Zaeske Telefon 0531 295-1114 | Fax 0531 295-2931 | wanja.zaeske(a)dlr.de<mailto:wanja.zaeske@dlr.de> DLR.de<http://www.dlr.de/>

6 7

address of L1 CNode Cap
by Yanfeng Liu 12 Dec '24

12 Dec '24

Dear experts, When reading section 3.3.2 of the latest seL4 manual, it says: > Figure 3.3 depicts an example CSpace. In order to illustrate these ideas, we determine the address of each of the 10 capabilities in this CSpace. I guess the total number of 10 is made of 3 caps for CNode types and 7 for non- CNode ones A~G as shown in diagram. However, in the following graph, the address of the L1 CNode Cap is missed. Thus I am curious what the address for that L1 CNode Cap? Regards, yf

2 2

seL4 developer hangout reminder
by Birgit Brecknell 09 Dec '24

09 Dec '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 11 Dec, 7:00am UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0