Devel July 2017

devel@sel4.systems

17 participants
12 discussions

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

L4Re IPC share memory that share file in one Linux filesystem and be visible to other Linuxes
by Joyce Peng(彭美僑) 05 Jul '17

05 Jul '17

Hi L4, I want to share a file in one Linux filesystem and be visible to other Linuxes that all run on top Fiasco.OC. It seems an IPC communication between L4re vm tasks. And access a file in Linux filesystem is a mechanism with kernel block device driver. But I only notice two char device drivers that use L4re library l4shmc in L4linux. It is l4ser_shm and l4shmnet. May you give some information about this work how to work. Thanks. Joyce Peng(彭美僑)

2 1

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel July 2017