- Devel - lists.sel4.systems

Call For Presentations for the seL4 Summit 2025
by Birgit Brecknell 17 Feb '25

17 Feb '25

Call For Presentations [0] for the seL4 Summit 2025 [1] - Share your seL4 work - Share your seL4 experience - Share your seL4 thoughts Check the full Call For Presentations [0]. To propose a talk, upload an abstract of one page or less by 21 April 2025 to the submission portal [2]. Also note the open invitation for a 5-minute slot to talk about your seL4 deployment [3]. [0] https://sel4.systems/Foundation/Summit/2025/cfp [1] https://sel4.systems/Foundation/Summit/2025/ [2] https://form.jotform.com/250436091673861 [3] https://sel4.systems/Foundation/Summit/2025/cfp#sel4-deployment 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

seL4 developer hangout reminder
by Birgit Brecknell 17 Feb '25

17 Feb '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 18 Feb, 9:00pm 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

seL4 developer hangout reminder
by Birgit Brecknell 03 Feb '25

03 Feb '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 5 Feb, 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

Running seL4 on bare-metal x86_64 PC
by saftab.rashid＠gmail.com 30 Jan '25

30 Jan '25

Hi, I am very new to sel4 and I am trying to run it bare-metal on an Intel Xeon x86_64 machine. I am following the instructions here PC99 | seL4 docs. I can run seL4 using the ./simulate script which runs the kernel under QEMU. However, I would like the run seL4 natively on my machine. After the build, I have the following images in the images/ directory. kernel-x86_64-pc99 sel4test-driver-image-x86_64-pc99 I have created a Grub2 menu entry by copying these images under /boot. However, when I boot using the created menu entry I get a black screen and I also see no output on the serial port. My Grub2 menu entry is as follows menuentry “Load seL4 VM” --class os { load_video insmod gzio insmod part_msdos insmod ext2 set root=‘(hd0,msdos2)’ multiboot /boot/kernel-x86_64-pc99 module /boot/sel4test-driver-image-x86_64-pc99 } I have also tried the multiboot2 protocol as I have an UEFI-supported system but it also doesn’t work. After booting into the seL4 VM I get a black screen and there is no output on the serial port. Any Idea what I am doing wrong?

1 0

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

seL4 developer hangout reminder
by Birgit Brecknell 20 Jan '25

20 Jan '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 21 Jan, 9:00pm 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

reclaiming root server memory frames
by Yanfeng Liu 18 Jan '25

18 Jan '25

Dear experts, I am wondering how seL4 app can reclaim some root server memory frames at later stage of bootstrapping? Regards, yf

1 1

seL4 developer hangout reminder
by Birgit Brecknell 06 Jan '25

06 Jan '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 8 Jan, 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

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