Devel December 2021

devel@sel4.systems

22 participants
27 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

seL4 developer hangout/video call
by Gerwin Klein 25 Jan '22

25 Jan '22

Hi seL4 devs, a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat. The idea for this is to be: - informal, about 1h - for technical discussions about seL4 and related repositories - anyone can join - every two weeks, initially for 3 times, then we can decide how we like it At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds. To provide a starting topic, one thing we'd be interested in is: seL4 boot code There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues. The first hangout is on - Sydney: Wed, Nov 3, 8am - Central Europe: Tue, Nov 2, 10pm - US East Coast: Tue, Nov 2, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

2 9

sel4test AARCH64 on imx8mm-evk
by Zippy Manaic 07 Jan '22

07 Jan '22

Hi, I have tried running sel4test built for AARCH64 (https://docs.sel4.systems/Hardware/imx8mm.html) on my imx8mm-evk dev board. I am on the 12.1.0 branch of sel4test-manifest.git. Firstly I have to add "set(KernelAArch64SErrorIgnore ON)" to my build config in order to get the tests running and unfortunately things go awry during the test run ... Starting test 47: FRAMEEXPORTS0001 Running test FRAMEEXPORTS0001 (Test that we can access all exported frames) Pagefault from [FRAMEEXPORTS0001]: read fault at PC: 0x41c4ec vaddr: 0x11000000, FSR 0x92000210 Register of root thread in test (may not be the thread that faulted) Register dump: pc: 0x41c4ec sp: 0x100118a0 spsr: 0x80000040 x0: 0x11000000 x1: 0x11000000 x2: 0x55 x3: 0x15 x4: 0xe6 x5: 0x0 x6: 0x0 x7: 0xffffffffffffffff x8: 0x10011a48 x16: 0x0 x17: 0x0 x18: 0x0 x29: 0x100118a0 x30: 0x41c9f0 x9: 0x2b x10: 0x2b x11: 0xffffffff x12: 0x0 x13: 0x0 x14: 0x0 x15: 0x0 x19: 0xe7 x20: 0x8 x21: 0x11000000 x22: 0x0 x23: 0x0 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 tpidr_el0: 0x616f60 tpidrro_el0: 0x0 Failure: result == SUCCESS at line 291 of file /host/projects/sel4test/apps/sel4test-driver/src/testtypes.c Error: result == SUCCESS at line 217 of file /host/projects/sel4test/apps/sel4test-driver/src/main.c ... Starting test 55: IPC1001 Running test IPC1001 (Test SMP inter-AS seL4_Send + seL4_Recv) KERNEL DATA ABORT! Faulting instruction: 0xffffff804001e2ac FAR: 0xffffff80bf800020 ESR (DFSR): 0x96000210 halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 20 Is this something that should just work? Or am I missing something. Cheers, Zippy

3 9

Question about the Real-time of the SEL4.
by 刘跃 Jeff Liu 01 Jan '22

01 Jan '22

Hi; As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event based model? Then why not use the thread based kernel? As far as I know, VxWorks and QNX are thread based. SeL4's view is that for non preemptive kernel, real-time performance focuses on WCET, and the faster kernel does not guarantee the real-time performance of the system. I partially agree with this view. I want to know if there are real-time comparison data?, The comparison test with VxWorks or QNX is about the real-time performance of the system. the worst case interrupt latency is the sum of both the longest region with interrupts disabled, and the time to dispatch an interrupt to a user thread. How are these two parts of time calculated? Is it the method of WCET static analysis? And Then how to improve the interrupt response time, What is the specific method to reduce interrupt latency? I think most users of seL4 are more concerned about this. I look forward to communicating and discussing with you, experts. Thanks;

2 1

Some questions about group of camkes (adjust the format)
by yadong.li 28 Dec '21

28 Dec '21

Hi * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 * Our camkes project test below, clien1 and client2 in the same group: " import <std_connector.camkes>; procedure MyInterface { void print(in string message); } component Client { control; uses MyInterface iface; } component Server { provides MyInterface iface; } assembly { composition { group g { component Client client_1; component Client client_2; } component Server server; connection seL4RPCCall conn(from g.client_1.iface, from g.client_2.iface, to server.iface); } configuration { client_1.iface_attributes = 11; client_2.iface_attributes = 22; } } * 1. We test function in group (a single address space): * the client code below: " #include <camkes.h> int run(void) { char *name = get_instance_name(); iface_print(name); return 0; } " * the server code below: " #include <camkes.h> #include <stdio.h> void iface_print(const char *name) { printf("[%s] ping, the badge is [%d]\n", name, iface_get_sender_id()); } " * From the cameks project, we have two client, they are client_1 and client_2, they have the same they can all “iface_print” to access server function，In this scene，we have two quesiton: * Question 1. After compiled the test project, we found in the symbol table of g_group_bin, we have two "iface_print" symbol, they have different address even though they have the same name, it look like the componet can call their own "iface_print", I think in a single address space, component like thread, Why two symbols with the same name(iface_print) will not conflict in one address space * Question 2: when client access server, we offer the _attributes(badge) for the interface of client, by test, the two client can call their own "iface_print", but the server can only recevice one badge 22, below is our test: " [client_2] ping, the badge is [22] [client_1] ping, the badge is [22] " * The attribute(badge) of client1 is covered by the attribute(badge) of client2, The iface_print of two client have only one capability to access IPC endpoint object * We can not understand in single address space,the "iface_print" of two component is behavior as one or two different ? * 2. We test function in global variable (a single address space): * We found whether global variables are initialized will have completely different behavior， out test code below: * scene1 :Client code below: " int temp_value; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } " * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is bss section, the temp_value of client1 and the temp_value of client2 have the same virtual address, and if the client2 change the value, client1 can perceive the change， test as below： " at start, in client_1, the temp_value address is [0x659e70], value is [0x0] at start, in client_2, the temp_value address is [0x659e70], value is [0x0] at last, in client_2, the temp_value address is [0x659e70], value is [0x12345] at last, in client_1, the temp_value address is [0x659e70], value is [0x12345] " * scene2 :Client code below: " int temp_value = 1; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } " * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is data section, the temp_value of client1 and the temp_value of client2 have the different virtual address, and if the client2 change the value, client1 can not get the change， test as below： " at last, in client_2, the temp_value address is [0x445ba8], value is [0x12345] at last, in client_1, the temp_value address is [0x444008], value is [0x1] " * The code of scene1 and scene2 are almost the same, except whether temp_value is initialized， the bss section or data section，but the symbol table completely different, scene1 the symbol table of g_group_bin has only one "temp_value" symbol, But scene1 the symbol table of g_group_bin has two symbols named temp_value, we also do not understand why the same name symbols of global variable should be one or two in a single address of group. It looks like random. Thank you very much

2 1

Some questions about group of camkes
by yadong.li 24 Dec '21

24 Dec '21

Hi * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 * Our camkes project test below, clien1 and client2 in the same group: import <std_connector.camkes>; procedure MyInterface { void print(in string message); } component Client { control; uses MyInterface iface; } component Server { provides MyInterface iface; } assembly { composition { group g { component Client client_1; component Client client_2; } component Server server; connection seL4RPCCall conn(from g.client_1.iface, from g.client_2.iface, to server.iface); } configuration { client_1.iface_attributes = 11; client_2.iface_attributes = 22; } } * 1. We test function in group (a single address space): * the client code below: #include <camkes.h> int run(void) { char *name = get_instance_name(); iface_print(name); return 0; } * the server code below: #include <camkes.h> #include <stdio.h> void iface_print(const char *name) { printf("[%s] ping, the badge is [%d]\n", name, iface_get_sender_id()); } * From the cameks project, we have two client, they are client_1 and client_2, they have the same they can all “iface_print” to access server function，In this scene，we have two quesiton: * Question 1. After compiled the test project, we found in the symbol table of g_group_bin, we have two "iface_print" symbol, they have different address even though they have the same name, it look like the componet can call their own "iface_print", I think in a single address space, component like thread, Why two symbols with the same name(iface_print) will not conflict in one address space * Question 2: when client access server, we offer the _attributes(badge) for the interface of client, by test, the two client can call their own "iface_print", but the server can only recevice one badge 22, below is our test: [client_2] ping, the badge is [22] [client_1] ping, the badge is [22] * The attribute(badge) of client1 is covered by the attribute(badge) of client2, The iface_print of two client have only one capability to access IPC endpoint object * We can not understand in single address space,the "iface_print" of two component is behavior as one or two different ? * 2. We test function in global variable (a single address space): * We found whether global variables are initialized will have completely different behavior， out test code below: * scene1 :Client code below: int temp_value; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is bss section, the temp_value of client1 and the temp_value of client2 have the same virtual address, and if the client2 change the value, client1 can perceive the change， test as below： at start, in client_1, the temp_value address is [0x659e70], value is [0x0] at start, in client_2, the temp_value address is [0x659e70], value is [0x0] at last, in client_2, the temp_value address is [0x659e70], value is [0x12345] at last, in client_1, the temp_value address is [0x659e70], value is [0x12345] * scene2 :Client code below: int temp_value = 1; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is data section, the temp_value of client1 and the temp_value of client2 have the different virtual address, and if the client2 change the value, client1 can not get the change， test as below： at last, in client_2, the temp_value address is [0x445ba8], value is [0x12345] at last, in client_1, the temp_value address is [0x444008], value is [0x1] * The code of scene1 and scene2 are almost the same, except whether temp_value is initialized， the bss section or data section，but the symbol table completely different, scene1 the symbol table of g_group_bin has only one "temp_value" symbol, But scene1 the symbol table of g_group_bin has two symbols named temp_value, we also do not understand why the same name symbols of global variable should be one or two in a single address of group. It looks like random.

1 0

Can't locate VM at virtual 0?
by Richard Clark 22 Dec '21

22 Dec '21

My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark

2 1

vm physaddr != virtual?
by Richard Clark 22 Dec '21

22 Dec '21

1 0

mapping tutorial answers?
by Richard Clark 22 Dec '21

22 Dec '21

I'm interested in the ANSWERS to the MAPPING tutorial. I have my own virtual/physical memory management system and need only the ability to map a specific physical address to a specific virtual address. I can find no such thing in all the sel4 code that I have, but it appears that the mapping tutorial is what I need. Does anyone have this? (preferably arm64 and/or x64) Richard Clark

1 0

sel4-sys support
by kgugala＠antmicro.com 16 Dec '21

16 Dec '21

Hi All, We’ve been working on reviving the sel4-sys Rust crate and getting it usable again. Currently, we have it working correctly with RISC-V, we’re working on ARM (including aarch64) and X86. We’d like to contribute this work, but to have it landed we need to extend the test suite to include crate tests - especially the syscalls API. During the build, the crate generates the syscalls functions accessible from Rust code based on seL4 config. We use standard sel4test-tests suite to handle the tests: * We build the crate as static library * Sel4test is built with `-DLibSel4FunctionAttributes=public` and while linking we overwrite the original symbols with the ones from a static library from the crate This allows us to run the standard test suite against Rust syscall stubs. For now the crate generates the syscall stubs with Rust flavor, so functions signatures between Rust and C do not match. To handle this we additionally generate a thin glue code adopting Rust signatures to the C ones. We generate the Rust syscalls with a slightly modified version of the `syscall_stub_gen.py` script - we copied it into the crate’s codebase. Copying the code doesn’t seem to be the best idea - we’d need to maintain the code in both places - seL4 kernel and the crate. We’d like to merge the Rust generator with the current set of tools - is this something you’d be willing to land in the kernel code? If not, how would you see the way forward here? Thanks and best regards Karol

4 5

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2021