Devel September 2022

devel@sel4.systems

12 participants
9 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

Entry of user program
by mincheol＠vt.edu 30 Sep '22

30 Sep '22

Hi, I am trying to benchmark seL4's cross core IPC. I was able to run the IPC tutorial program and am now trying to run the server and the client on different VCPU. I found seL4_TCB_SetAffinity() but need to know the entry point of user program. Can anyone point it out for me? Mincheol

2 1

I need help with the IPC tutorial
by mincheol＠vt.edu 30 Sep '22

30 Sep '22

Hi, I can't figure out what to code in server.c for the ipc tutorial. What can I code after "// TODO use cap transfer to send the badged cap in the reply" line in the tutorial template (server.c) Can anyone share the fully working source.c?

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 30 Sep '22

30 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Oct 4, 9pm (UTC), Topics: (open) * Sydney: Wed, Oct 5, 8am * Central Europe: Tue Oct 4, 11pm * US Pacific Time: Tue, Oct 4, 2pm 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

Raspberry Pi SMP?
by dave＠synergy.org 30 Sep '22

30 Sep '22

Hello, Is there any intent to enable SMP on the Raspberry Pi? I am using the Raspberry Pi 3B+. I'd like to be able to use all 4 CPUs. Thanks, David

2 2

Support for Sel4 Project
by simone cataldo 29 Sep '22

29 Sep '22

Good morning, We are a small test team, investigating seL4 microkernel to evaluate its use it as core component for a novel “open avionics” drone concept. Essentially, we are starting from scratch, basing ourselves on the provided tutorials such as “hello world”. We were trying to modify its source code for evaluating basic thing simple functions, basic programs and custom libraries. However, it looks like the memory allocation is static and embedded in the original project: once we increase the complexity of the program it evidently causes trouble. We have not found any documentation about how to set the memory allocation at compile time, and how to include external dependencies (i.e. static libraries). We would like to have some guideline to get us started and direction to some in-depth documentation to acquire enough knowledge to build a full project of our own. We are looking forward to hearing from you soon. Best regards, Simone CATALDO

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 19 Sep '22

19 Sep '22

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

Proper seL4 APi/ABI design
by Eric Jacobs 17 Sep '22

17 Sep '22

Jumping off from the recent thread, I was curious if anyone had any thoughts about how to optimally design API's for seL4. I noticed we had a bit of info about what not to do (don't do long IPC, don't implement Posix, don't use messaging as synchronization, etc.) Are there any shining examples of what _to_ do with an API? Thanks, -Eric

5 11

Reminder seL4 developer hangout
by Birgit Brecknell 05 Sep '22

05 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Sep 6, 10pm (UTC), Topics: (open) * Sydney: Wed, Sep 7, 8am * Central Europe: Wed, Sep 7, 12 midnight * US Pacific Time: Tue, Sep 9, 3pm 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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel September 2022