- Devel - lists.sel4.systems

i.MX7 Support?
by Steven Johnston 19 Aug '17

19 Aug '17

Has anyone had luck running the seL4test suite with an i.MX7 processor? I acquired a Toradex Colibri board (https://www.toradex.com/computer-on-modules/colibri-arm-family/nxp-freescal…) and am testing it out. Using the docker environment when I brew a seL4test config file either by hand or through menuconfig results in a 'libplatsupport' failure. There is platform support for the i.MX7 in the kernel source and imx7/armv7-a/cortex-a7 options in the seL4 git Makefile. Using the following make options results in another failure on multiple #error defines: "TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx7 ARMV=armv7-a CPU=cortex-a7 make" Thanks for any help or direction you can point me in, Steve

1 0

rumprun + rust + camkes
by Michal Podhradsky 18 Aug '17

18 Aug '17

Hello Kent, I extended the rumprun+rust example (available in this PR <https://github.com/seL4/camkes/pull/4>) with a simple camkes connection between the rumprum camkes component and a serial server component, as shown below (full code here <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/r…> ): * composition {* * component rumprun_platform_layer rrpl;* * component rumprun_rust hello1;* * RUMPRUN_META_CONNECTION(hello1, rrpl)* * component rumprun hello2;* * RUMPRUN_META_CONNECTION(hello2, rrpl)* * component Server server;* * connection seL4SharedData conn(from hello1.camkes_buffer, to server.buffer);* * connection seL4Notification simpleEvent1(from hello1.camkes_ev, to server.ev);* * connection seL4Notification simpleEvent2(from server.ev1, to hello1.camkes_ev1);* * }* I added a simple rust program <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/c…> (running on rumprun_rust): *fn main() {* * println!("Hello rust!");* * unsafe {* * camkes_ev_emit();* * }* * println!("Waiting for event!");* * unsafe {* * camkes_ev1_wait();* * }* * println!("Got event!");* *}* *#[no_mangle]* *extern {* * fn camkes_ev_emit();* * fn camkes_ev1_wait(); * *}* In order to compile the cargo project, I added a build.rs script <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/c…> to package the generated camkes object file (camkes.o) into an archite that cargo can link against. The problem is, that the generated camkes.c file contains its own main function: *int USED main(int argc UNUSED, char *argv[]) {* * assert(argc == 2);* * assert(strcmp(argv[0], "camkes") == 0);* * int thread_id = (int)(uintptr_t)(argv[1]);* * return post_main(thread_id);* *}* which collides with the *fn main()* defined in rust. (I get *multiple definition of `main'* error). How is this handled in rumprun_ethernet <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_ethern…> example? There is also a main function for the rumpkernel component <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_ethern…>, and the main() from camkes, but the compilation process handles this correctly. Could you point me in the right direction? Regards Michal

2 6

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

rumprum and camkes
by Michal Podhradsky 05 Aug '17

05 Aug '17

Hello all, mostly Kent, I read your blog post about rumpkernels on sel4: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbs… and after experimenting with the rumprun apps (such as the ethernet one <https://github.com/seL4/camkes/tree/master/apps/rumprun_ethernet>) I think it is a great addition to sel4. So I have few questions. I need to run two different rumpkernels, each with its own address space, connected only through dataports/events. 1- does the current rumpkernel backend support having this separation? According to your thesis <http://www.disy.cse.unsw.edu.au/theses_public/16/kentm.pdf>, all rumpkernel threads run in a single sel4 thread - is that correct? 2- Right now, I can combine multiple rumprun components in one application (lets say *runmprun_hello* and *rumprun_pthreads*). butI can have only one rumprun_platform_layer per application, correct? An example below: *assembly {* * composition {* * component rumprun_platform_layer rrpl;* * component rumprun hello;* * RUMPRUN_META_CONNECTION(hello, rrpl)* * component rumprun_pthreads pthreads;* * RUMPRUN_META_CONNECTION(pthreads, rrpl)* * }* * configuration {* * hello.rump_config = {"cmdline": "hello World!" };* * RUMPRUN_COMPONENT_CONFIGURATION(hello, 0)* * pthreads.rump_config = {"cmdline": "./pthreads_test 4" };* * RUMPRUN_COMPONENT_CONFIGURATION(pthreads, 1)* * }* *}* If I instantiate another *rumprun_platform* component, it wont compile. 3 - how can I go around defining/adding my own rumpkernels? Lets say I want to build a rumpkernel with rust support <https://github.com/rumpkernel/rumprun-packages/tree/master/rust> (you have an sel4 example here <https://github.com/SEL4PROJ/rumprun-sel4-demoapps/tree/master/userapps/rust>) and integrate it with the rumprun_hello <https://github.com/seL4/camkes/blob/master/apps/rumprun_hello/rumprun_hello…> app. Regards Michal

2 1

camkes-vm cma34cr_picotcp doesn't build
by Michal Podhradsky 05 Aug '17

05 Aug '17

Hello, when I do a fresh init of the camkes-vm repository: *repo init -u https://github.com/seL4/camkes-vm-manifest <https://github.com/seL4/camkes-vm-manifest>* *repo sync* and then I want to build the cma34cr_picotcp app: *make clean* *make make cma34cr_picotcp_defconfig* *make silentoldconfig* *make* I get the following error: *Makefile:76: *** No CAmkES application selected. Stop.* Do you guys have any CI server set up? If not, I would be happy to help set something up, this is not the first time an existing configuration doesn't build. Regards Michal

2 2

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