Devel November 2022

devel@sel4.systems

3 participants
5 discussions

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

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 20 Nov '22

20 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

Reminder seL4 developer hangout
by Birgit Brecknell 14 Nov '22

14 Nov '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Nov 16, 6am (UTC), Topics: (open) * Sydney: Wed, Nov 16, 5pm * Central Europe: Wed, Nov 16, 7am * US Pacific Time: Tue, Nov 15, 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

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel November 2022