Devel October 2016

devel@sel4.systems

24 participants
30 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

Does anyone use recycle?
by Adrian.Danis＠data61.csiro.au 03 Nov '16

03 Nov '16

Hi All, If you do not know what recycle is and/or have not used it then you can probably ignore this e-mail. We are considering removing the recycle operation from cnodes, and replacing it with a 'revoke badges' operation. Currently the semantics of recycle are ill defined but can generally be summed up as "put an object back into its initial state". It turns out this is not particularly useful, and is completely unused by us. The proposal is to remove this and have an invocation that will only operate on endpoints and will remove any badged versions of that endpoint, hence the name 'revoke badges'. This is the current semantics of recycling an endpoint, and we see this as the only useful thing recycle does, hence the desire to keep it around. Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal. Adrian

5 11

need ideas
by Vasily A. Sartakov 02 Nov '16

02 Nov '16

Hello. I have a problem. It is a very complicated problem. I understand that It is hard to give an advice without looking into the sources. But I am stuck and need some ideas in ‘brainstorm’ format as an input for me. So, here is the problem: There are many tests from sel4test suit are working. This is how does it look like: http://pastebin.com/vvnDaUe9 Unfortunately, I found several configurations of the tests, which causes crashes with stable and different symptoms. One of them is looking following: 11 #include <sel4test/test.h> 12 #include "../test.h" 13 #include "../helpers.h" 14 15 #define MIN_EXPECTED_ALLOCATIONS 100 16 17 18 19 20 21 22 23 int test_allocator(env_t env) 24 { 25 /* Perform a bunch of allocations and frees */ 26 vka_object_t endpoint; 27 int error; 28 29 for (int i = 0; i < MIN_EXPECTED_ALLOCATIONS; i++) { 30 error = vka_alloc_endpoint(&env->vka, &endpoint); 31 test_assert(error == 0); 32 test_assert(endpoint.cptr != 0); 33 vka_free_object(&env->vka, &endpoint); 34 } 35 36 return sel4test_get_result(); 37 } 38 DEFINE_TEST(TRIVIAL0001, "Ensure the allocator works", test_allocator) 39 DEFINE_TEST(TRIVIAL0002, "Ensure the allocator works more than once", test_allocator) as you might see, this is little bit modified version of trivial.c tests. Usual, when I am testing all tests, there is no problem with this test. But when I am running this file alone, I have a problem. Also, you might see, that there are several free lines with numbers from 16 to 22. I made this not accidental, it is a source of error. If the test_allocator(env_t env) is lockated in the 23rd line, this tests has no problem. But if I add one more free line, I have an error like this: Starting test suite sel4test Starting test 0: TEST_TRIVIAL0001 TEST_TRIVIAL0001 726:trap!, address error on store! $0 : 0 fffffff8 7 10089000 $4 : 6a6ffc 3f 0 ffffffff $8 : 1 7 1 20 $12 : 70f 0 2 6ae $16 : 6a6ffc 5a6a50 ffffff30 6a6ffc $20 : 3f 5a6e58 5a6a50 6a6fdc $24 : 20 41bab0 0 0 $28 : 0 100848d8 fffffffe 41faf0 Hi : 20 Lo : 0 epc : 41f818 fi : 41f814 ra : 41faf0 Status: 20000002 Cause : 414 Config: 80008482 BadVaddr: f which means, that the test-drivers (I know the ASID) tries to store something to the address 0x0000000f by the instruction located in the 0x41f818 (EPC). Also, it is failed before the starting of trivial.c test! This is what I on the address: 0041f7b4 <unbin>: 41f7b4: 8c83000c lw v1,12(a0) 41f7b8: 27bdffd8 addiu sp,sp,-40 41f7bc: 8c820008 lw v0,8(a0) 41f7c0: afb0001c sw s0,28(sp) 41f7c4: 00808021 move s0,a0 41f7c8: afbf0024 sw ra,36(sp) 41f7cc: 1462000e bne v1,v0,41f808 <unbin+0x54> 41f7d0: afb10020 sw s1,32(sp) 41f7d4: 00a03021 move a2,a1 41f7d8: 00002021 move a0,zero 41f7dc: 0c107afa jal 41ebe8 <.pic.__ashldi3> 41f7e0: 24050001 li a1,1 41f7e4: 3c04005a lui a0,0x5a 41f7e8: 00022827 nor a1,zero,v0 41f7ec: 24846a50 addiu a0,a0,27216 41f7f0: 0c107dac jal 41f6b0 <a_and> 41f7f4: 00038827 nor s1,zero,v1 41f7f8: 3c04005a lui a0,0x5a 41f7fc: 02202821 move a1,s1 41f800: 0c107dac jal 41f6b0 <a_and> 41f804: 24846a54 addiu a0,a0,27220 41f808: 8e030008 lw v1,8(s0) 41f80c: 8e02000c lw v0,12(s0) 41f810: 8fbf0024 lw ra,36(sp) 41f814: 8fb10020 lw s1,32(sp) 41f818: ac430008 sw v1,8(v0) I am quite sure that there is no problem here with unbin function, and the problem somewhere with contexts, or alignment or something else. Also, I am mapping this area RO, so I am also sure that there is no corruption of the user-space regions. Also, I see, that there is a correlation between size of the image and faults: 1349892 ./sel4test-tests.bin_23 1349900 ./sel4test-tests.bin_24 The border line is 1349900 if I have a size of the image below the value -- there is no problem. Unfortunately, 1349900 is not a 'round' value, somehow related to TLB sizes of something else what I know. Also, I should mention, that 'key' variable wich changes when I add new line is an argument of _sel4test_failure: mips-mti-linux-gnu-objdump -d sel4test-tests.bin_23 > bin23.asm mips-mti-linux-gnu-objdump -d sel4test-tests.bin_24 > bin24.asm diff -ua bin23.asm bin24.asm Disassembly of section .init: @@ -3143,7 +3143,7 @@ 4030f0: 3c050043 lui a1,0x43 4030f4: 2484c248 addiu a0,a0,-15800 4030f8: 24a5c964 addiu a1,a1,-13980 - 4030fc: 2406001f li a2,31 + 4030fc: 24060020 li a2,32 403100: 0c107b51 jal 41ed44 <_sel4test_failure> 403104: 0000f021 move s8,zero 403108: 8fbf0074 lw ra,116(sp) @@ -3383,7 +3383,7 @@ 4034b0: 2484c950 addiu a0,a0,-14000 4034b4: 24a5c964 addiu a1,a1,-13980 4034b8: 0c107b51 jal 41ed44 <_sel4test_failure> - 4034bc: 24060020 li a2,32 + 4034bc: 24060021 li a2,33 4034c0: 03c01021 move v0,s8 4034c4: 8fbf0074 lw ra,116(sp) 4034c8: 8fbe0070 lw s8,112(sp) That is all that I have now. Any ideas? Now I do not see any other choice but to gradually reduce the amount of code with keeping this 'border' situation, until I will not have very small set of system functions. Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 3

Configuring Process Issue
by Andrew Mine 28 Oct '16

28 Oct '16

Hi I am working with Zynq based seL4 and currently have written an app which configures two processes using sel4utils_configure_process. Both my other processes are apps that are also elf files generated during the build. I have noticed that when I am configuring two processes in the root task as 102: sel4utils_process_t process1,process2; 103: error = sel4utils_configure_process(&process1, &vka, &vspace, seL4_MaxPrio, PROCESS1_IMAGE_NAME); 104: assert(error == 0); 105: 106: error = sel4utils_configure_process(&process2, &vka, &vspace,seL4_MaxPrio, PROCESS2_IMAGE_NAME); 107: assert(error == 0); The code compiles but I get a runtime error as _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object@object.h:51 Failed to allocate object of size 4096, error 1 _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark new_pages_at_vaddr@vspace.c:325 Failed to allocate page load_segment@elf.c:82 ERROR: failed to allocate frame by loadee vka: 10 _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark sel4utils_elf_load_record_regions@elf.c:272 Failed to load segment sel4utils_configure_process_custom@process.c:550 Failed to load elf file _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark sel4utils_configure_process_custom@process.c:593 Could not clean up vspace Assertion failed: error == 0 (latest-sel4-tutorial/apps/zynq-comm/src/main.c: main: 107) If I remove any one of the process from the root process, it actually works and my process gets launched. I am assuming there is some conflict when the elf is being loaded as both processes are elf files. Regards Andrew

1 0

CallWithMRs is an unexercised code path
by Jeff Waugh 27 Oct '16

27 Oct '16

Hi all, Last night I opened two pull requests to begin fixing the CallWithMRs code path on x86_64 and aarch32. syscall_stub_gen.py couldn't generate x86_64 stubs for the CallWithMRs / non-IPCBuffer path. That didn't surprise me too much, as x86_64 support is relatively new. Then I discovered that libsel4 *always* [1] uses the IPCBuffer path. Hrm. Changing that prompted a quick fix to aarch32's apparently unused, long since even built CallWithMRs. (Similar fixes might be needed in some of the other functions.) The test suite failed with it on aarch32, which I could poke at in more depth, but it worked fine for x86_64. So… what's the status of the *WithMRs functions? Based on my understanding of the source (particularly the new helper functions) and assembly output, they're destined for the chopping block, right? Thanks, Jeff [1] hard coded --buffer parameter to syscall_stub_gen.py in libsel4/Makefile, since late 2015

2 6

Build Error
by Andrew Mine 27 Oct '16

27 Oct '16

Hi I have used sel4-tutorial branch earlier and was able to build and run earlier. I realized that my branch is way behind, so I have cloned the new branch into a separate folder and am compiling for zynq device. I get the following build error: [apps/hello-1] building... [HEADERS] [STAGE] autoconf.h [CC] src/main.o [CC] src/util.o [LINK] hello-1.elf sel4tutorials/stage/arm/zynq7000/lib/libsel4.a: error adding symbols: Archive has no index; run ranlib to add one collect2: error: ld returned 1 exit status make[1]: *** [hello-1.elf] Error 1 make: *** [hello-1] Error 2 Is anyone else facing this issue? I am using arm-none-eabi-gcc for compiling. Regards Andrew

2 1

Allocman Error
by Neelesh Vemula 26 Oct '16

26 Oct '16

Hi I have created a new process from the root/init task. In the new process I have the following code for initializing the allocman as below: vka_t vka; allocman_t *allocman; vspace_t vspace; #define ALLOCATOR_STATIC_POOL_SIZE ((1 << seL4_PageBits) * 10) UNUSED static char allocator_mem_pool[ALLOCATOR_STATIC_POOL_SIZE]; #define ALLOCATOR_VIRTUAL_POOL_SIZE ((1 << seL4_PageBits) * 100) int main(int argc, char **argv) { allocman = bootstrap_use_current_1level(SEL4UTILS_CNODE_SLOT, CONFIG_SEL4UTILS_CSPACE_SIZE_BITS, 0, (1u << CONFIG_SEL4UTILS_CSPACE_SIZE_BITS), ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); allocman_make_vka(&vka, allocman); vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n"); I have the following definition structure shared as enum sel4utils_cspace_layout { /* * The root cnode (with appropriate guard) */ SEL4UTILS_CNODE_SLOT = 1, /* The slot on the cspace that fault_endpoint is put if * sel4utils_configure_process is used. */ SEL4UTILS_ENDPOINT_SLOT = 2, SEL4UTILS_PD_SLOT = 3, FREE_SLOT = 4, }; This particular program has compiled for zynq-7000 platform and when running it I get the following output in the stdout : Just entered the user function vka_alloc_object@object.h:51 Failed to allocate object of size 16, error 1 Assertion failed: error == 0 (/apps/zynq-comm-user/src/main.c: main: 71) I have been not able to figure out why this error is occurring. I can only guess that the allocman was not initialized properly. Can someone help me with what I may have done wrong? Regards Neelesh Vemula

2 1

Exynos Arndale 5420 support
by Yevgeny Lavrov 26 Oct '16

26 Oct '16

Hello. Exynos Arndale 5250 is listed as seL4 supported ARM devices. I would like to know if seL4 also supports Exynos Arndale 5420 board, and if it does, then would the process of mounting seL4 onto Arndale 5420 be the same as with 5250? Thanks

2 1

seL4 Call Issue
by Chris Guikema 26 Oct '16

26 Oct '16

Hello, I am working on a lock system using templates (based on what is found here: https://github.com/seL4/camkes/tree/master/apps/mutex). This system can work, but there are some issues with the components just going back and forth when calling the locks. I believe this is an issue with multiple components using the same endpoint to communicate with the "lock server" and the calls getting pre-empted by other threads. Here are the system calls that are used to hit the endpoint with the (un)lock request. seL4_Send(/*? ep ?*/, info); info = seL4_Recv(/*? ep ?*/, NULL); And in the lock server: seL4_MessageInfo_t info = seL4_Recv(/*? ep ?*/, &sender); ...do locking things seL4_Send(/*? ep ?*/, info); So in order to prevent preempting by other threads, I went and changed the (un)lock request system call to info = seL4_Call(/*? ep ?*/, info); Using print statements, I was able to determine that the lock server receives the proper message on the endpoint and performs the locking operations. However, when it reaches the seL4_Send operation, the system locks up. This shouldn't be the case, because one component is waiting on the endpoint with the seL4_Call, and the other is sending information on the same endpoint, especially when having separate Send & Recv statements works. Am I doing something incorrect? Thanks for your help, Chris Guikema

1 0

Starting Threads in New seL4Utils processes.
by Richard Habeeb 25 Oct '16

25 Oct '16

Hello all, I am using seL4Utils to create some new processes. For these I am also transferring capabilities to some untyped kernel memory so that those processes can start their own worker threads and make endpoints. I've managed to get those threads started; however, I am a bit confused about how the CSpace is laid out now. My problem is that I want these worker threads to have capabilities to an endpoint created by the child process, but I can't figure out how to copy the cap. This is my TCB configure line. error = seL4_TCB_Configure(THREAD_2_CAP, seL4_CapNull, seL4_MaxPrio, SEL4UTILS_CNODE_SLOT, seL4_NilData, SEL4UTILS_PD_SLOT, seL4_NilData, ipc_buffer_vaddr, THREAD_2_IPC_BUF_CAP); Any guidance is appreciated. Thanks. -- Richard Habeeb Research Assistant, Computer Science, USF http://habeebr.bitbucket.org/

1 1

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel October 2016