October 2022 - Devel - lists.sel4.systems

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

18 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 30 Oct '22

30 Oct '22

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

Cross Core IPC
by Sid Agrawal 23 Oct '22

23 Oct '22

Hi, I came across Gernot Heiser's blog post on "How to use seL4 IPC" [1]. The article explicitly says that doing cross-core IPC is a bad idea. This statement led to a series of questions for me, which I hope you guys can help me with. Scenario ------------ We have a system with two cores. Let's say that a physical memory server is running on core0, my application is on core1, and they are somehow pinned to those cores. The application wants some physical memory (frame capabilities) from the memory server. Questions ------------- Q1. Will the application be able to invoke the endpoint given that the TCB which will respond to it is on a separate core? If yes, will sending a capability back via cross-core IPC be allowed? I did not read anything in the manual which said otherwise. Q2. Why is a cross-core IPC a bad idea? This might be a loaded question, but I am not able to appreciate the badness of the idea :) Q3. What would be the right way to do it? For example, in Barrelfish(limited experience from a course), the application(on core1) would make an IPC to a monitor running on the same core1. This monitor did synchronization with another monitor running on the other core(core0) via a shared memory region (all in user space). That monitor(core0) then sent an IPC to the memory server running on core0. And then back again via the monitors. Best, Sid [1] https://microkerneldude.org/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/

3 2

Suitability for a project
by James Hillman 19 Oct '22

19 Oct '22

Hi Sel4 developers, I am new to this forum and hoping this is the right place to bounce my project idea off. I typically use FPGA to enforce security in my products but there are lots of reasons why FPGAs are not suitable for all use cases. I have also used low end microcontroller where one can review all the code to understand the security risks. My latest project however involves two USB processes (one for each physical connection) with high throughput expectations. And to pass data streams at high typical throughput between them. Due to the wide range of USB type of devices I fear this would be too much code to review - it feels very OS like. Note, I don't need a GUI, it's headless. So I'm interested in sel4 as I could run the processes in Linux VMs if I understand sel4 correctly. And whilst it's not the smallest processors I think they need to be more powerful to support the speeds. So this is fine . I am unsure how much of this project is already done, mainly thinking the usb driver perspective. Thanks in advance, Best wishes James

5 10

new RFC: seL4 Device Driver Framework
by Gerwin Klein 19 Oct '22

19 Oct '22

A new RFC has just landed: https://sel4.atlassian.net/browse/RFC-12 If you have any feedback, please comment there. Cheers, Gerwin

8 16

Re: Suitability for a project
by James Hillman 18 Oct '22

18 Oct '22

Thanks Gernot. Thoughts on throughput rates thats might be achieved?

1 0

Re: Suitability for a project
by James Hillman 18 Oct '22

18 Oct '22

I was interested to see the Google news re. KataOS which I suspect confirms that my sort of requirement / entry point is someway out. I was also reading about ARM Morello / CHERI work. Although I appreciate this is taking a different, perhaps flawed, path of some new hardware memory protection. Appreciate any feedback you can humour me with.

2 1

seL4 dev hangout reminder
by Gerwin Klein 17 Oct '22

17 Oct '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Oct 19, 6am (UTC), Topics: (open) * Sydney: Wed, Oct 19, 5pm * Central Europe: Wed, Oct 19, 8am * US Pacific Time: Tue, Oct 18, 11pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Devel Digest, Vol 171, Issue 3
by Isaac Beckett 07 Oct '22

07 Oct '22

> From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] new RFC: seL4 Device Driver Framework > To: sel4 <devel(a)sel4.systems> > Cc: "tsc-members(a)sel4.systems" <tsc-members(a)sel4.systems> > Message-ID: <55BB3266-24A1-488B-A623-5B912461AD7F(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > A new RFC has just landed: https://sel4.atlassian.net/browse/RFC-12 > > If you have any feedback, please comment there. > > Cheers, > Gerwin Ooh, exciting. I wonder if something similar to Mesa could be implemented for graphics, to ease porting existing Mesa drivers.

1 0

High-throughput asyncrhonous driver API?
by Andrew Warkentin 05 Oct '22

05 Oct '22

I remember talk in one of the developer hangouts I was in about a proof of concept for a high-throughput asynchronous driver layer for seL4 (presumably based on notifications). Has code for this been released anywhere? I'm going to be starting on my own IPC transport layer and I want to include asynchronous message passing as an option.

1 0