- Devel - lists.sel4.systems

VMM ARM SMP support
by Joyce Peng(彭美僑) 22 Aug '17

22 Aug '17

Hi seL4, I see below link to know VMM support SMP at Q3’17. I want to know does it ready and has any restriction? Thank you. https://sel4.systems/Info/Roadmap/ Low-level Userland Status Date Feature Location deferred to Q3’17 SMP-capable virtual-machine monitor (VMM) master Joyce.Peng (彭美僑)

1 0

Re: [seL4] mpu vs mmu
by Thomas Dundon 21 Aug '17

21 Aug '17

Thanks for the information. Looking at eChronos now. > > ---------- Forwarded message ---------- > From: <Ihor.Kuz(a)data61.csiro.au> > To: <devel(a)sel4.systems> > Cc: > Bcc: > Date: Sun, 20 Aug 2017 23:57:34 +0000 > Subject: Re: [seL4] mpu vs mmu > > > On 21 Aug 2017, at 8:05 am, Gernot.Heiser(a)data61.csiro.au wrote: > > > > On 21 Aug 2017, at 03:00, Thomas Dundon <dundon.thomas(a)gmail.com> wrote: > >> > >> Does an MPU, e.g. on a Cortex M3, provide enough functionality to > support seL4? > > > > No, it doesn’t. The seL4 model is fundamentally based on the ability to > virtualise hardware resources. > > > > If you don’t have that, then you can’t dod much more than a > memory-protected RTOS. If you’re after an RTOS with a (not yet complete) > verification story, look at eChronos: https://ts.data61.csiro.au/ > projects/TS/echronos/ > > > > In particular we have some work in the pipeline that adds (ARM > Cortex-M3/4) MPU support to eChronos (it’s currently in the process of > being code-reviewed and will be released after that). > > Ihor. > > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > >

1 0

mpu vs mmu
by Thomas Dundon 21 Aug '17

21 Aug '17

Does an MPU, e.g. on a Cortex M3, provide enough functionality to support seL4? Thanks, Tom

3 2

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