- Devel - lists.sel4.systems

Any reliable way to determine if a thread is suspended?
by Andrew Warkentin 28 Dec '22

28 Dec '22

Is there any reliable way to determine if a thread is suspended? seL4_TCB_Suspend() succeeds even if the thread was already suspended. I can force all calls to seL4_TCB_Suspend() and seL4_TCB_Resume() to go through a wrapper that updates a user-level flag (since my OS manages pretty much all capabilities in the root server and will only expose TCBs to regular user processes through a special filesystem); however, this leaves a race when a thread is suspended due to a fault instead of an API call (since the thread will already be suspended before the fault handler updates the "thread running" flag). My initial use for checking if a thread is running is to allow easy atomic updates of some metadata (shared between the root server and the non-root thread, and optionally shared between threads) for my IPC transport layer that implements Unix-like file descriptors on top of seL4 endpoints (and eventually notifications). To add an FD to a thread's list, the root server allocates a copy of the endpoint (and reply if the FD is server-side) into the thread's CSpace, suspends the thread, updates the metadata (which includes the underlying capabilities), and then resumes the thread if it was running. Obviously, I don't want to resume threads that weren't running in the first place. I don't want to use locks here since the root server can't trust regular user processes. Another use is to allow cancelling any in-progress transfers on FDs when they get closed and returning a status to the waiting threads, which I am planning to do by replacing the endpoint with a copy of a global "clunk endpoint" associated with a thread that repeatedly sends a "file descriptor closed" message (actually there will be two such threads - one for clients, and one for servers) and then resuming the thread.

1 0

problem Ethdriver 82574 on Qemu X86_64
by reza yazdanparast 25 Dec '22

25 Dec '22

Hi. I'm working on a new camkes-based project. This project is simulated by using Qemu, on a Q35 machine for X86_64 arch and e1000e eth. I am using an intel controller driver (82574 controller) for network communication. My project has been built successfully and the intel network driver has been initialized. But when using the network in my application in Qemu, no network packet is sent and received! Qemu command: ``` sudo qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu host, -netdev tap,id=netdev0,ifname=tap0,script=no,downscript=no -device e1000e,id=nic0,netdev=netdev0,mac=52:55:00:d1:55:01 -nographic -serial mon:stdio -m size=4G -device intel-iommu -kernel ./target/debug/images/kernel-x86_64-pc99 -initrd ./target/debug/images/capdl-loader-image-x86_64-pc99 ``` . Appendix: Create tap0 command: ``` export TAP_DEV=tap0 sudo ip tuntap add dev $TAP_DEV mode tap sudo ip addr flush dev $TAP_DEV sudo ip addr add 10.10.100.1/24 brd 10.10.100.255 dev $TAP_DEV sudo ip link set dev $TAP_DEV addr 02:00:ca:fe:01 sudo ip link set dev $TAP_DEV up ``` . how to fix this problem? Thank you.

1 0

any fun holiday hacks with sel4?
by ember arlynx 25 Dec '22

25 Dec '22

merry christmas :) i've been thinking about reviving some rusty robigalia-ish things. how are you all doing, this stormy sunday? -- ember

1 0

next seL4 TSC meeting on Fri 16 Dec (15 Dec in US and Europe)
by Gerwin Klein 16 Dec '22

16 Dec '22

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 16 Dec, 8am - Central Europe: Tue, 15 Dec, 10pm - US West Coast: Tue, 15 Dec, 1pm See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/5510249963 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - election (or re-election) of TSC chair - split C-Parser/AutoCorres out from l4v repository - RFCs: - SMC https://sel4.atlassian.net/browse/RFC-9 - MCS: Improve constraints on grant via reply https://sel4.atlassian.net/browse/RFC-13 - MCS: set fault and timeout handler parameters while configuring TCBs https://sel4.atlassian.net/browse/RFC-11 - The seL4 Core Platform https://sel4.atlassian.net/browse/RFC-5 - The seL4 Device Driver Framework https://sel4.atlassian.net/browse/RFC-12 - Ability to build additional bootloaders inside the seL4 build system https://sel4.atlassian.net/browse/RFC-4 - SIG chair nominations - discuss process for establishing SIGs If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 1

Reminder seL4 developer hangout
by Birgit Brecknell 12 Dec '22

12 Dec '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Dec 14, 6am (UTC), Topics: (open) * Sydney: Wed, Dec 14, 5pm * Central Europe: Wed, Dec 14, 7am * US Pacific Time: Tue, Dec 13, 10pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Call for nominations for Special Interest Group Chairs
by Gerwin Klein 05 Dec '22

05 Dec '22

At this year's seL4 summit the community expressed strong interest in starting a number of special interest groups (SIGs) around seL4 and in particular around the following topics: - Virtual machines and virtual machine monitors (SIG VMM) - Drivers (SIG Drivers) - Multicore design + verification (SIG Multicore) The multicore verification topic also showed large overlap with interest in user-level verification at the summit. One suggestion would be to cover both topics in that SIG. To start these SIGs, we are calling for the nomation of a chair for each of them. Anyone can nominate anyone from the seL4 community, including themselves. If there is more than one nomination who is willing to do the job for a specific SIG, we will organise a vote and if possible appoint a chair + vice-chair (for backup). The appointement will be confirmed by the technical steering committee TSC. The main job of the chair of a SIG will be (lightweight) moderatation, keeping the conversation going, and to be a point of contact with the TSC. An initial task for the chair would be to lead the discussion on what the SIG will be about in more detail and what it wants to achieve. Examples could be: - to coordinate concrete work - to discuss the topic of the SIG - to make recommendations to the TSC - to work together on RFCs on the topic of the SIG This should result in a short description that we can use on the seL4 website and discourse groups for the SIG to describe what its purpose is. We suggest that the main communciation medium for SIGs be the seL4 discourse forum, where each SIG could have its own topic area, but we are happy for SIGs to self-organise differently if they prefer. Please send nominations to Gerwin Klein <kleing(a)unsw.edu.au>. Please indicate which SIG they are for. Cheers, Gerwin (seL4 TSC chair)

1 0

[FOSDEM'23] Submit talk for the "Microkernel and Component-based OS" devroom
by Razvan Deaconescu 05 Dec '22

05 Dec '22

Hi. I am Razvan Deaconescu, I'm from University POLITEHNICA of Bucharest (working on Unikraft unikernel) and I'm managing the "Microkernel and Component-based OS" devroom[2] at FOSDEM'2023[1]. The devroom will take place in person, at FOSDEM'23, in Brussels, on Sunday, February 5, 2023. If you have an interesting topic to talk about it would be great if you made a submission. This is something easy to do, takes about 15-20 minutes on Pentabarf[3]. The deadline for submission is today, Friday, December 2, 2022. [1] https://fosdem.org/2023/ [2] https://fosdem.org/2023/schedule/track/microkernel_and_component_based_os/ [3] https://penta.fosdem.org/submission/ Razvan

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 28 Nov '22

28 Nov '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Nov 29, 9pm (UTC), Topics: (open) * Sydney: Wed, Nov 30, 8am * Central Europe: Tue, Nov 29, 10pm * US Pacific Time: Tue, Nov 29, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Survey about the seL4 summit 2023's location
by June Andronick (seL4 Foundation) 21 Nov '22

21 Nov '22

Dear seL4 friends, With the great success of the seL4 summit 2022 behind us, we are now already looking at the seL4 summit 2023! This should happen around Sep/Oct 2023. We have started investigating options for the location, and we would like your feedback. We would very much appreciate if you could fill in this very short survey to tell us your opinion between USA (likely Minneapolis) and Australia (likely Sydney) or any other feedback you have: https://forms.gle/k4XxYaYeudYUie9U8 <https://forms.gle/k4XxYaYeudYUie9U8> Please do so by Nov 22nd 2022. Feel free to forward to anyone you believe may want to attend the summit next year. Many thanks! June -- June Andronick CEO of the seL4 Foundation https://sel4.systems/Foundation

1 1

Experimental project on seL4 microbenchmarking
by Nataliya Korovkina 19 Nov '22

19 Nov '22

Hi seL4 friends, I’d like to share an experimental project on seL4 microbenchmarking inspired with my experience with sel4bench suite. Your thoughts on the concept and its practical use will be greatly appreciated. Motivation (informal) Measuring execution times of short code paths, which we can meet in seL4 microbenchmarking, is a good way to immerse oneself into the domain of compiler and microarchitectural optimizations. Implementation of “early processing” measurement methodology in sel4bench suite (for Notification delivery case, as a trial step; PR #26) was an amazing experience in that respect. So, I gladly share the work highlights to explain my motivation. First, latencies of some microarchitectural events can be comparable with execution time of a measured code path. So, if microarchitectural event not planned by a benchmark design happens during a measuring period, deviation of the observed value considerably increases. Second, the both kinds of optimizations of instrumental code cause instability of measured values from one measurement iteration to another. Third, debugging the instrumental code is very challenging. Injection of diagnostic code into it changes effects of the both types of optimizations; therefore, initially witnessed symptoms effectively transform to other ones. When you think about how to control optimizations effects, the situation appears uninspiring, considering the need to treat various microarchitectures and optimization features. As a result, the situation left me with the question on hands: how to distance a benchmark design from necessity to control optimizations effects in instrumental code that impair repeatability? Eventually, it reduced to the foundational one: What we measure, and Why? This experimental work is attempt to find and try the solution for the challenge: designing more predictable measurement context. The work was published in github. Description paper https://github.com/malus-brandywine/sel4KanataBench-papers/blob/main/Kanata… Project repository https://github.com/malus-brandywine/sel4KanataBench Project manifest repository https://github.com/malus-brandywine/sel4KanataBench-manifest Tables of data collected on four TS platforms: files KBenchTable-xxxx.pdf in https://github.com/malus-brandywine/sel4KanataBench-papers Thank you!

1 0