Devel July 2017

devel@sel4.systems

17 participants
13 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

VGA buffer as stdout
by Michal Podhradsky 31 Aug '17

31 Aug '17

Hello, I have a question about standard output. I have a camkes component than can write into text-mode VGA buffer (basically it follows this simple example http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like to be able to redirect the kernel messages during startup to be printed on screen using VGA buffer. Once another component (either Linux in a VM, or some other camkes app) will initialize, it will be able to take control over the screen output (and for example show login window etc). My questions is - is this possible with seL4? And if so, what would it entail? I guess in the minimal version, I would have to provide a different implementation of seL4_DebugPutChar, is that correct? The VGA standard seems to define the buffer to be at 0xB8000, so it should be consistent between x86 platforms. Regards Michal

5 11

Can I run Android on camkes-arm-vm with tk1 board?
by li94575 05 Aug '17

05 Aug '17

Hi, Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel? I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below: [ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000) [ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.761443] [ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5-00024-gec4c02c-dirty #122 [ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14) [ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220) [ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4) [ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0) [ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754) [ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c) [ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4) [ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20) [ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 Is this a problem that current VMM does not support FPU? or other reasons caused the problem？

2 11

network on seL4
by Gábor Székely 03 Aug '17

03 Aug '17

Hi, I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32. I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62 Regards, Gábor Székely

4 4

rump kernel test, compilation issues
by Steven Harp 31 Jul '17

31 Jul '17

A couple of issues building the latest seL4 NetBSD rumpkernel demoapps, hello-ia32-x86_64_qemu_defconfig / hello-x86_64-x86_64_qemu_defconfig. (Ref: https://github.com/SEL4PROJ/rumprun-sel4-demoapps ) 1. In libsel4muslcsys sys_morecore.c: > /host/libs/libsel4muslcsys/src/sys_morecore.c:248:16: error: ‘vaddr’ undeclared (first use in this function) > return vaddr; > ^ Speculatively, should it return: (long) placement_vaddr ? 2. In rumprun/platform/sel4/entry.c > entry.c:91:9: error: implicit declaration of function 'allocman_add_untypeds_from_timer_objects' [-Werror=implicit-function-declaration] > allocman_add_untypeds_from_timer_objects(allocator, env->custom_simple.timer_config.hw.to); Not sure where this function should be found... Same results in native build (Xenial) and in docker build container. Any suggestions warmly appreciated. // Steve

2 1

Recursive call to malloc crash system
by Fabrizio Bertocci 27 Jul '17

27 Jul '17

Hi all, I have a system configured to use dynamic heap through the vspace. I'm working with 5.2.0 and using pc99 simulator through qemu. Everything is occurring in the root task, as I haven't even completed my bootstrapping code. In this configuration, whenever my code calls malloc() and there is a low memory condition (where there is not enough space on the heap to fulfill my request), malloc() end up calling __expand_heap(). Here it first attempts to expand the heap through brk syscall, then if fails uses mmap() to attempt to get more pages from the virtual memory. In both cases (brk and mmap) end up calling a function in the vspace that attempts to make available new pages. Unfortunately the code in the libself4utils/src/vspace/vspace.c, end up calling malloc() for the sel4utils_res structure. As you expect, we are already in a no-memory condition, so a subsequent call to malloc() might end up calling __expand_heap() and so on... (depending on the bytes left on the heap, this nested malloc might succeed if the initial block was larger than the size of sel4utils_res structure). So, everything loops until the whole system crash because of stack overflow. Why vspace uses malloc() to dynamically allocate those structures, causing the whole system to fail? To test, I have changed the implementation in vspace.c to use a static buffer pool, and it seems it solve my issue, but am I doing something wrong in the bootstrap code ? Any help is appreciated, Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

3 4

Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1"
by tj5527 23 Jul '17

23 Jul '17

Another problem when making sel4. The make program complains Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1". [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup stack will use a locally installed GHC For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec stack build --only-dependencies Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1" Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 1 How can I fix this? Thank you. Ubuntu 16.04 LTS GNU Make 4.1 gcc version 5.4.0 20160609

3 4

Sydney `taste of seL4' miniconference/developer day
by Peter.Chubb＠data61.csiro.au 19 Jul '17

19 Jul '17

Hi Folks, Next January 22--26, linux.conf.au will be in Sydney, Australia. We're planning on submitting a proposal for a one-day miniconference to be held in conjunction with the main conference. We'd like to line up potential speakers now, before submitting. If you are doing something cool and open source with seL4, and would like to speak at that miniconference, please let me know. linux.conf.au is one of the best grass-roots open-source and Linux conferences around; if you're doing anything cool that's open source with seL4 (or with Linux), then I'd encourage you to submit a proposal to the main conference as well, at https://linux.conf.au/ Peter Chubb -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)

1 0

Question on endpoint cap write permission
by Jimmy Brush 13 Jul '17

13 Jul '17

Hello, in the 6.0 manual section 3.1.4 the table shows that Write permission on an endpoint cap permits sending to the endpoint. however, in section 4.2.2 it says without the Write permission on the RECEIVING endpoint cap, any cap sent over IPC gets diminished. Am I missing something? It seems the Write permission is overloaded to mean two different things. This would seem to imply that to receive an undiminished capability via IPC you must have both send and receive permission to the endpoint you are receiving against. Which would mean if you wanted to limit someone to only receiving and never sending against an endpoint by giving them an endpoint cap with only Read permission, they would necessarily also NEVER be able to receive an undiminished capability. Thanks, JB

4 5

Compile problems about camkes-vm project
by deng.chao1＠zte.com.cn 11 Jul '17

11 Jul '17

SGkgZXZlcnlvbmU6DQoNCiAgSSB0cnkgdG8gcnVuIHZtIG9uIHNlTDQuIA0KDQogIEkgaGF2ZSBk b3dubG9hZGVkIFZNIHByb2plY3QgdXNpbmcgInJlcG8gaW5pdCAtdSBodHRwczovL2dpdGh1Yi5j b20vc2VMNC9jYW1rZXMtdm0tbWFuaWZlc3QuZ2l0Ii4gDQoNCiAgSSB1c2UgY29tbWFuZHM6DQoN CiAgICAgIG1ha2UgY21hMzRjcl90d292bV9kZWZjb25maWcNCg0KICAgICAgbWFrZSBzaWxlbnRv bGRjb25maWcNCg0KICAgICAgbWFrZSANCg0KdG8gY29tcGlsZSB0aGUgcHJvamVjdCwgYnV0IGhl cmUgcmVwb3J0cyBwcm9ibGVtcy4NCg0KICBUaGUgZmlyc3QgcHJvYmxlbSBpcywgaXQgY2FuIG5v dCBmaW5kIGxpYnBpY290Y3AuIEkgaGF2ZSBjaGVjayB0aGUgc291cmNlIGNvZGUsIGl0IGRvZXNu J3QgaW5jbHVkZSBkaXJlY3RvcnkgbGlicy9saWJwaWNvdGNwLy4NCg0KU28gSSBnZXQgcmlkIG9m IHRoZSBsaWJwaWNvdGNwIHBhcnQgYnkgY29tbWVudCBpdCBpbiB0aGUgS2NvbmZpZyBmaWxlLg0K DQogIE5leHQsIHRoZSBvdGhlciBwcm9ibGVtIGFjY3VycyBhcyBibG93aW5nOg0KDQoJIi9ob21l L2RlbmdjaGFvL21qL2NhbWtlcy12bS90b29scy9jYW1rZXMvY2Fta2VzLm1rOjEzNzogL2hvbWUv ZGVuZ2NoYW8vbWovY2Fta2VzLXZtL2J1aWxkL3g4Ni9wYzk5L2NtYTM0Y3JfdHdvdm0vY2Fta2Vz LWdlbi5tazogTm8gc3VjaCBmaWxlIG9yIGRpcmVjdG9yeQ0KDQogCVtHRU5dIGNhbWtlcy1nZW4u bWsNCg0KCUVSUk9SOkNBbWtFUzovaG9tZS9kZW5nY2hhby9tai9jYW1rZXMtdm0vYXBwcy9jbWEz NGNyX3R3b3ZtL3ZtLmNhbWtlczoyMzoxOTogICAgICAgICBjb21wb25lbnQgRWNobyBlY2hvDQoN CglFUlJPUjpDQW1rRVM6ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIF5eXl5eXg0KDQoJRVJST1I6 Q0Fta0VTOm5vbi1vcHRpb25hbCBpbnRlcmZhY2UgZWNoby50aW1lciBpcyBub3QgY29ubmVjdGVk DQoNCgltYWtlWzFdOiAqKiogWy9ob21lL2RlbmdjaGFvL21qL2NhbWtlcy12bS9idWlsZC94ODYv cGM5OS9jbWEzNGNyX3R3b3ZtL2NhbWtlcy1nZW4ubWtdIGVycm9yIDI1NSINCg0KICANCg0KICBJ IGhhdmUgdHJpZWQgY29uZmlnIHRoZSBwcm9qZWN0IHRvIGNtYTM0Y3Jfc2luZ2xldm1fZGVmY29u ZmlnIG9yIGNtYTM0Y3JfdWJ1bnR1X2RlZmNvbmZpZywgYWxzbyByZXBvcnMgdGhlIHNhbWUgZXJy b3IuDQoNCiAgQW5kIHRoZSBjMTYyX3R3b3ZtIGNvbmZpZywgc2VlbXMgaXQgaGFkIGFsc28gYmVl biByZW1vdmVkIGZvciB0aGUgY2Fta2VzLXZtIHByb2plY3Q/DQoNCiAgQ291bGQgYW55b25lIHJl bHkgbWUgb24gdGhlIGtpbmRuZXNzPw0KDQoJCQkJCQkJCSAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgIHlvdXJzIERlbmdDaGFv

2 1

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel July 2017