- Devel - lists.sel4.systems

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

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

malloc & errno
by Fabrizio Bertocci 05 Jul '17

05 Jul '17

Hi all, I am facing a puzzling problem related to muslc. While running some tests with the ia32 simulator (qemu), have noticed that whenever I call malloc() and I run out of memory (because my morecore buffer is too small), I am getting some kernel crash. I have traced the issue to the place where errno is set to -ENOMEM. Referencing to errno is platform-dependent and end up calling a function that retrieve the struct pthread associated and access errno as one of the field of the struct pthread. What is the correct process to set up a heap from the root task in such a way that we can call malloc() and correctly handle error conditions through errno? I am pretty sure I am doing something wrong in my initialization code (I have based my main(0 on the code from the tutorials), because I am also having other problems with malloc(). (even after I increase my heap area). For example, in some cases a call to malloc() end up calling a cascade of functions that eventually (from inside muslc) end up calling again malloc(). As consequence it enters in an infinite loop that stop only after it exhaust the initial stack. I could not find any clear example that show how to correctly set up a system to use muslc. Can anyone point me to a good example that shows how to bootstrap a system for the 5.2.0 branch? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1

make: stack: Command not found
by tj5527 04 Jul '17

04 Jul '17

A newbie question. I follow the link [1] trying to build sel4 with qemu. But when `make`ing the binary, it throws error message `make: stack: Command not found`. I `apt-get install stacks` but it still fails with the same error. What packages should I install for making sel4 with Ubuntu 16.04 LTS, GNU Make 4.1, and gcc version 5.4.0 20160609? Thanks [Error Message] -- Build files have been written to: /path/to/sel4/stage/x86/pc99/accelerator ninja: no work to do. [apps/vm] building... [HEADERS] [STAGE] autoconf.h [apps/vm] done. [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup make: stack: Command not found Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/path/to/sel4/projects/capdl/capDL-tool' Makefile:53: recipe for target '/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL' failed make: *** [/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL] Error 2 [1] https://wiki.sel4.systems/Hardware/Qemu

1 1

elfloader-tool
by Yevgeny Lavrov 30 Jun '17

30 Jun '17

Hi Is there any instruction on how to compile and use elfloader-tool? More specifically: I want to link seL4 image with other image to try out on i.MX6 platform. Thanks

2 1

vmm documentation
by Mike Clark 29 Jun '17

29 Jun '17

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc? That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

4 17

Why armel for the seL4 ARM VMM?
by John Backes 27 Jun '17

27 Jun '17

I was curious why the ARM VMM for the TK1 only seems to support the use of armel based distributions? Does special care need to be taken in the VMM to handle guest floating point instructions if the OS is armhf based? - John

2 1

How does the seL4 kernel revoke frame cap?
by Norrathep Rattanavipanon 24 Jun '17

24 Jun '17

Hello, I was wondering when we call seL4_cnode_delete on a (mapped) frame cap, does the kernel also handle unmapping the frame (in addition to withdrawing authority) as well? Or the user-space has to ensure that the frame is unmapped first before calling delete? I tried my code without unmapping that frame when deleting the cap and it seems to work fine. So I guess the kernel handles that? Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 5

Tutorial app hello-camkes-mcs not working
by Nicholas VanderStel 24 Jun '17

24 Jun '17

I've been able to build and run the hello-camkes-mcs example app from the camkes-mcs-tutorials.xml manifest both on a SabreLite board and in QEMU. However, when I try to run the app with the budget and period values given in the solution file, the client tasks don't appear to be running as they should. See the output from running on the SabreLite here: https://pastebin.com/RM0aisyF After that point it seems to hang. I tried smaller budget & period values and have been able to get one client task running, but the second task doesn't appear to be running. Has anyone been able to run this example with different results? Thanks, Nick VanderStel

1 0

Help with libethdriver
by Fabrizio Bertocci 22 Jun '17

22 Jun '17

Hi all, I am facing an issue with our existing project (currently based on seL4 1.0). I am in the process of migrating our project to the latest version of seL4. After all the required changes I am facing a problem I need some help. In our code, we use libplatsupport for timer & serial I/O as well as the libethdriver in order to use the network interface of the IMX6 board. The problem appears that the IOMUX device registers are mapped twice. A first time from libplatsupport (and never released): -> sel4platsupport_new_io_ops() -> calls: mux_sys_init() -> calls the macro: MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); This end up mapping the device region IMX6_IOMUXC: 0x20e0000 - 0x20e100 (size_bits=12). So far so good... but then they are mapped again from the ethernet driver: ethif_new_lwip_driver_no_malloc() -> call my initialization fn -> call ethif_imx6_init() -> call setup_iomux_enet() that end up mapping again the region @ IOMUXC_PADDR = 0x20e1000 This second time, the mapping function _utspace_split_alloc fails because apparently the region 0x20e000 has been already mapped (and is not in the regions available). If I comment out the call to mux_sys_init() in libsel4platsupport_new_io_ops() my ethernet driver successfully initialize (but clearly that's not the correct workaround). Any suggestions? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1

Questions about TK1-SOM Memory Management
by Daniel Wang 22 Jun '17

22 Jun '17

Hi Adrian, Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)? I can see the dev_p_regs[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization? Here is the booting procedure according to my understanding, could you take a look and see if I got it right? 1. the code start at the ELF-loader main() (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code _start, which setup up vector table and kernel stack; then init_kernel(); then try_init_kernel() calls map_kernel_window() I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything? Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch? (deleted diagram due to size limit) Thanks -Dan

2 3

drivers in seL4
by 杰尔米 22 Jun '17

22 Jun '17

Hi all， I want to know more about the mechanism of device driver in seL4. How does seL4 support userspace drivers? if I want to write a driver(e.g. serial port) base on seL4, how to do that? can any one help? Best Regards! Jeremy

3 2

Questions about TK1-SOM Memory Management
by Daniel Wang 20 Jun '17

20 Jun '17

Hi all, I’m trying to get a better understand about the implementation details of seL4 for TK1-SOM. Most of the code are very clear, but I’m little confused on the available physical memory in TK1-SOM. I’m wondering why In the hardware.c file (/kernel/src/plat/tk1/machine/hardware.c), the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } instead of 0x80000000 - 0xffffffff? Thank you very much! -Dan

2 1

Linux binaries constructed by Buildroot cannot run on tk1 board
by li94575 20 Jun '17

20 Jun '17

Hi， I use Buildroot 2016.08.1 with the config "buildroot_tk1_initrd_defconfig" to compile linux-tegra(https://github.com/SEL4PROJ/linux-tegra/tree/sel4), everything goes well. But the linux binary cannot output any logs, camkes-arm-vm stops at “Starting VM”. Can anyone tells me where might be wrong? I have tried using cross-compiler arm-none-linux-gnueabi-(2014.05) to compile linux-tegra, and that linux binary can work.

2 4

seL4test with 4.0, 5.1 failed on Ubuntu
by Daniel Wang 16 Jun '17

16 Jun '17

Hi all, I’m testing the new versions of seL4 (,4.0, 5.0, 5.1, etc.) using the sel4test-manifest. I tried both Ubuntu 16 and Ubuntu 14. For 3.2 version both I32 and KZM_simulation built just fine. However for the higher version (4.0. 5.1, 5.2) only I32 built properly. KZM_simulation keep failing on both Ubuntu 14 and 16. Anyone has the similar issues? Thanks -Dan FYI: [apps/sel4test-tests] done. [KERNEL] [MKDIR] src/arch/arm/api [PBF_GEN] arch/object/structures.pbf [PBF_GEN] arch/api/shared_types.pbf [PBF_GEN] plat/machine/hardware.pbf [PBF_GEN] api/types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] arch/api/shared_types_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/arm/armv/armv6/machine_asm.s_pp [AS] src/arch/arm/armv/armv6/machine_asm.o [CPP] src/arch/arm/32/halt.s_pp [AS] src/arch/arm/32/halt.o [CPP] src/arch/arm/32/head.s_pp [AS] src/arch/arm/32/head.o [CPP] src/arch/arm/32/idle.s_pp [AS] src/arch/arm/32/idle.o [CPP] src/arch/arm/32/traps.s_pp [AS] src/arch/arm/32/traps.o [CPP] src/arch/arm/32/hyp_traps.s_pp [AS] src/arch/arm/32/hyp_traps.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘doFlush’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1929:10: error: ‘ARMPDClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1929:10: note: each undeclared identifier is reported only once for each function it appears in /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1930:10: error: ‘ARMPageClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1933:10: error: ‘ARMPDInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1934:10: error: ‘ARMPageInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1937:10: error: ‘ARMPDCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1938:10: error: ‘ARMPageCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1941:10: error: ‘ARMPDUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1942:10: error: ‘ARMPageUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMPageDirectoryInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2217:10: error: ‘ARMPDClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2218:10: error: ‘ARMPDInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2219:10: error: ‘ARMPDCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2220:10: error: ‘ARMPDUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMPageTableInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2335:21: error: ‘ARMPageTableUnmap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2344:41: error: ‘ARMPageTableMap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMFrameInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2440:10: error: ‘ARMPageMap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2562:10: error: ‘ARMPageRemap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2680:10: error: ‘ARMPageUnmap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2699:10: error: ‘ARMPageClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2700:10: error: ‘ARMPageInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2701:10: error: ‘ARMPageCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2702:10: error: ‘ARMPageUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2772:10: error: ‘ARMPageGetAddress’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMMMUInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2818:45: error: ‘ARMASIDControlMakePool’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2887:45: error: ‘ARMASIDPoolAssign’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/Makefile:566: recipe for target 'kernel_final.s' failed make[1]: *** [kernel_final.s] Error 1 tools/common/project.mk:254: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2

2 2

seL4_Fault_t and friends seems to be missing in user libsel4
by Alexander Boettcher 15 Jun '17

15 Jun '17

Hello, if I compile and link seL4 5.2.0 ARCH=x86 PLAT=pc99 SEL4_ARCH=x86_64 make and I finally try to use the generated syscall/libsel4 headers, the compiler complains about missing seL4_Fault types and functions in libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/faults.h like seL4_Fault_t seL4_Fault_tag seL4_Fault_VMFault_new and a lot more. These structs and functions seems to be generated only for the kernel side, e.g. in kernel_final.c they show up, but there are no traces of them on the user level side. Do I just miss a configuration option ? Thanks, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 4

[Camkes] Is there any way to declare hierarchical header files and does CamKES support C++ boost preprocessor?
by Tran Cuong 14 Jun '17

14 Jun '17

Hello everybody, I'm conducting a C-project, in which the code is utilizing boost library to define several macros. This source code is running well in Linux and using only standard C library (I had tested this libraries individually by some mini-programs on CamKES). My project is organized as follows: - Top folder: + "components" folder contains my c code + "include" folder contains 1 .h file boost1.h and 1 folder test ++ sub-folder "test" contains 1 file boost2.h ++ content of boost1.h is just include "test/boost2.h" + "Makefile" is declared as below: TARGETS := $(notdir ${SOURCE_DIR}).cdl ADL := tst-macro.camkes Client_CFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/*.c)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/plat/${PLAT}/*.c)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/arch/${ARCH}/*.c)) Client_ASMFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/crt/arch-${ARCH}/crt0.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/*.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/arch/${ARCH}/*.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/plat/${PLAT}/*.S)) Client_HFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/include/*)) include ${PWD}/tools/camkes/camkes.mk - This above Makefile, I imitated from another application, and when I compiled the project, there are some errors related to directory of "test/boost2.h". I suspect that there is something wrong with Client_HFILES declaration, since maybe it is only valid for a list of .h files, not for hierarchical folders. - I really want to dive into CamKES, but I only have a little knowledge about this. My project is due so I hope to get some positive advice from you for 2 questions: + The right way to declare multi-level libraries as in my example. + Besides, does CamKES support boost preprocessing lib. Currently I'm using the toolchain arm-none-eabi- Thank all of you for the time and attention. Dinh-Cuong -- ------------------- TRAN Dinh Cuong (Mr) Email : cuongtd4(a)gmail.com

2 2

Trustworthy and mixed critical
by Jonathan C Day 14 Jun '17

14 Jun '17

Dear all, The first of these terms has an... interesting history. In a nutshell, it's not always used appropriately. Clearly that's not going to be the case with SEL4, but what exactly is meant? Mixed critical is another term that I'm cautious over. It's not completely clear to me if the mixing refers to relaxed constraints for utilisation reasons or something else. (Correct me if I'm mistaken, but I don't think SEL4 implements FLASK, which would be the obvious way to provide differing constraints, relaxed constraints within the trusted computing model. It's totally the wrong level.) I have absolutely no doubt SEL4 will retain all the provable integrity ever claimed (by anyone involved), but this experimental-proto-main branch confuses me on what fundamentally changes. Jonathan Day

2 1

Compilation of seL4 kernel 5.2.0
by Alexander Boettcher 14 Jun '17

14 Jun '17

Hello, I want to compile just the seL4 kernel (5.2.0) and tried it by invoking: alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make but the compile fails (attached below). Do I need to setup/configure something beforehand ? It seems some defines are not set. The host is a 64bit Ubuntu 16.04 LTS. Thanks, Alex. alex@max:~/sel4.git$ git log commit 3695232f9603af60d56f97072082d90f30e98b0e Author: Kent McLeod <Kent.Mcleod(a)data61.csiro.au> Date: Wed May 31 17:21:29 2017 +1000 update VERSION file to 5.2.0 alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make [MKDIR] arch/object [PBF_GEN] arch/object/structures.pbf [PBF_GEN] plat/32/plat_mode/machine/hardware.pbf [PBF_GEN] 32/mode/api/shared_types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/32/plat_mode/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/x86/32/machine_asm.s_pp [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s_pp [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s_pp [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/multiboot.s_pp [AS] src/arch/x86/multiboot.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp In file included from ./include/arch/x86/arch/fastpath/fastpath.h:14:0, from src/arch/x86/32/c_traps.c:15: ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:137:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:168:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:198:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:238:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ Makefile:729: recipe for target 'kernel_all.c_pp' failed make: *** [kernel_all.c_pp] Error 1 rm plat/32/plat_mode/machine/hardware_gen.h 32/mode/api/shared_types_gen.h src/arch/x86/32/machine_asm.s_pp src/arch/x86/32/traps.s_pp src/arch/x86/multiboot.s_pp arch/object/structures_gen.h src/arch/x86/32/head.s_pp -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 2

seL4-test on Beaglebone black
by Fabrizio Bertocci 14 Jun '17

14 Jun '17

Hi, I am posting this email as reference to anyone who want/need to run seL4 on a BeagleBone Black (BBB). The post at https://wiki.sel4.systems/Hardware/Beaglebone is great, unfortunately even if I followed exactly those instructions, I ended up hitting some walls here and there. I eventually managed to solve those issues and run successfully seL4test on my BBB. First of all the build system. I have tried unsuccessfully to find arm-linux-eabi for CentOS 7 (my preferred distribution for building on Linux), but apparently is an easy-to-find only on Ubuntu... so I ended up creating a VM with Ubuntu 16.04. If someone knows how to get arm-linux-eabi on CentOS please let me know... Unfortunately even with Ubuntu not everything went as smooth as I hoped. It appears that Python "past" module is no longer available for 16.04, so build fails on kernel/tools/lex.py. According to the comment right before the failing import statement, it appears this module is just declared but not used, so commenting it out (or removing it entirely) would fix this issue: #from past.builtins import cmp One more issue: when using either one of the following configurations as start point: - bamboo_bbone_black_debug_xml_defconfig - bbone_black_debug_xml_defconfig The build system will end up producing a binary image and not an ELF image. Producing an ELF image can be more useful if you want to use objdump to get a disassembly (for debugging later). So I changed the configuration with: make menuconfig Navigate to: Tools -> Build elfloader -> Boot image type and select "ELF Boot Image" instead of "Binary Boot Image" Save your configuration then build: make Now manually convert the produced ELF image in a binary: arm-linux-gnueabi-objcopy --output-target binary images/sel4test-driver-image-arm-am335x sel4test.bin then copy the file 'sel4test.bin' onto the SD card formatted as FAT32 Now, in my BBB (rev A5A) if I try to follow the instructions from the wiki page previously mentioned, I get a crash right away (illegal instruction). The problem is that in my BBB the uBoot environment variable ${loadaddr} is set to 0x80200000 and not 0x82000000 (the start address of the produced image). BBB have RAM mapped from address 0x80000000 to 0x9FFFFFFF (512Mb), so running from 0x82000000 is ok. So to load and run, use instead: fatload mmc 0 0x82000000 sel4test.bin go 0x82000000 That's it. Test should load and run successfully: Test suite passed. 220 tests passed. 220/220 tests passed. All is well in the universe. Hope this help saving some time... Regards, Fabrizio

1 0

Important note for CAmkES users
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We've just released CAmkES 3.0.0 (release notes<https://wiki.sel4.systems/CAmkES%203.0.0>), and with it, all changes staged on our development branch, CAmkES Next, have been merged into the "master" branch of the camkes-tool repo (https://github.com/seL4/camkes-tool) We'll be continuing to develop CAmkES on its "master" branch, and cease making new commits to the "next" branch. # What this means for you As CAmkES 3.0.0 is incompatible with older versions of CAmkES, any projects tracking the master branch of camkes-tool will probably not build after this change. Also, as all new development is now being done on the master branch, any projects tracking the next branch of camkes-tool will no longer receive updates. If you're in either category, you'll need to update your project's repo manifest. # Migration Instructions If your project tracks either the "master", or "next" branch of the camkes-tool, you'll need to update your project's manifest. To check if this applies to you, look in your projects repo manifest xml file (typically in .repo/manifest.xml at the top level of your project) for the line: <project name="camkes-tool.git" path="tools/camkes"> (this implicitly tracks "master") OR <project name="camkes-tool.git" path="tools/camkes" revision="master"> OR <project name="camkes-tool.git" path="tools/camkes" revision="next"> If your manifest has either of those lines, take a look at the migration guide in the CAmkES 3.0.0 release notes: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating It covers a range of different scenarios and explains how to change your manifest so your project will continue to work. If the camkes-tool revision in your manifest specifies a particular version of CAmkES (e.g. 'revision="camkes-2.3.1"'), you don't need to migrate.

1 0

Pre-release of mixed criticality seL4 extensions
by Anna.Lyons＠data61.csiro.au 13 Jun '17

13 Jun '17

= seL4-5.2.0-mcs = The first round of mixed-criticality extensions for seL4 are now available for your perusal and usage. This is a prerelease of features that are currently our candidate for verification. They are *not* verified and most likely contain bugs. If you encounter any, please report them ;) We have more features in development coming, but this is the first lot. = Release Notes = Detailed release notes can be found on our wiki: https://wiki.sel4.systems/seL4%205.2.0-mcs = Upgrade Notes = This version is not compatible with seL4 5.2.0, but forks the API based on that kernel version. Branches are available in most of our libraries to use, and CAmkES and capdl already have support for this pre-release on their latest release and master branch. = Major Changes = A summary of major changes can be found at: https://wiki.sel4.systems/seL4%205.2.0-mcs#Highlights A tutorial covering the new features can be found at: https://wiki.sel4.systems/seL4%205.2.0-mcs = Source Code = https://github.com/seL4/seL4/tree/5.2.0-mcs = Full Change Log = Use: git log 5.2.0..5.2.0-mcs

1 0

Announcing CAmkES 3.0.0
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We're pleased to announce the release of CAmkES 3.0.0. This is a major release, which contains all work from our development branch, also known as CAmkES Next. Future development on CAmkES will occur on the "master" branch. Importantly, this means no further commits will be made to the "next" branch, so users will need to update their manifests to point at the "master" branch, or alternatively, the "camkes-3.0.0" tag created with this release. = Release Notes = Detailed release notes can be found on our wiki: https://wiki.sel4.systems/CAmkES%203.0.0 = Upgrade Notes = Dependencies for running CAmkES have changed since the previous release. Instructions for installing dependencies on several linux distros can be found here: https://wiki.sel4.systems/CAmkES#Build_dependencies If you were tracking the master branch of the camkes-tool in your project, you'll need to modify your project's manifest for it to continue to work. Migration instructions for a variety of situations can be found at: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating = Major Changes = A summary of major changes can be found at: https://wiki.sel4.systems/CAmkES%203.0.0#New_Features = Examples = mkdir camkes-examples && cd camkes-examples repo init -u https://github.com/seL4/camkes-manifest.git -m default-3.0.x.xml repo sync tests/x86-simple.tcl # builds and runs simple example = Source Code = https://github.com/seL4/camkes-tool/ = Full Change Log = Use: git log camkes-3.0.0...$(git merge-base camkes-2.3.1 camkes-3.0.0) = More Details = Manual: https://github.com/seL4/camkes-tool/blob/camkes-3.0.0/docs/index.md Wiki: https://wiki.sel4.systems/CAmkES Enjoy!

1 0

Missing pico_device.h
by Michal Podhradsky 09 Jun '17

09 Jun '17

Hello, the recent commits in broke the build of util_libs <https://github.com/seL4/util_libs/commits/master> broke the build of camkes- <https://github.com/seL4/camkes-vm>vm <https://github.com/seL4/camkes-vm>. To recreate the error, do: mkdir test_defaultcd test_defaultrepo init -u https://github.com/seL4/camkes-vm-manifest.gitrepo sync make cleanmake optiplex9020_defconfigmake silentoldconfigmake You will get: *In file included from /test_default/libs/libethdrivers/src/pico_dev_eth.c:15:0:/test_default/stage/x86/pc99/include/ethdrivers/pico_dev_eth.h:16:26: fatal error: pico_device.h: No such file or directorycompilation terminated.* Regards Michal

1 0

Temporally disable write-access on memory pages
by Norrathep Rattanavipanon 09 Jun '17

09 Jun '17

Hello, I have a question regarding the best way to temporally disable write-access on memory pages. Suppose in the user-space, there are two processes: initial user-space process and process A, which is created by the initial process. Process A has its own virtual memory space. Now we want to find a way to enforce the memory inside process A to be temporally R/O to process A (since we want to have the initial process compute a function on that memory snapshot.) Currently, what we are doing now is to lock all memory pages of process A by calling the "remap" function inside the initial process. But then we realize that doing that does not help much. Since process A owns capabilities to its memory pages, process A also can call "remap" function to unlock the locked memory pages (please correct me if it's wrong). This will cause the memory to be inconsistent when computing a function on that memory. My question is is there anyway to enforce how a page locking (make it R/O) works in seL4 so that ONLY the entity that locked the page can unlock it? For example, in this case, we want to make sure that only the initial process can unlock the pages that he locked earlier. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 2

Fwd: k_vmm_manager: failed on sel4 hypervisor connection
by Michal Podhradsky 08 Jun '17

08 Jun '17

Hello all, I am running camkes-vm on x86 architecture, following the example on wiki https://wiki.sel4.systems/CAmkESVM#Cross_VM_Connectors with the exception that I want to invoke the stringReverse component <https://github.com/podhrmic/camkes-vm/tree/master/components/StringReverse> . I am running the optiplex9020_defconfig example with only one VM, and when I start booting the guest linux system, I see the following error: *[ 1.282326] dataport: loading out-of-tree module taints kernel.* *[ 1.290615] dataport: module license 'unspecified' taints kernel.* *[ 1.306854] Disabling lock debugging due to kernel taint* *[ 1.319664] dataport initialized with major number 247* *vmm_vmcall_handler:55 | Failed to find handler for token:2* *[ 1.325411] incorrect event context magic number (expected 42, got -677408512)insmod: can't insert '/lib/modules/4.8.16/kernel/drivers/vmm/consumes_event.ko': Operation not ermitted* *[ 1.337441] emits_event initialized with major number 245* *[ 1.356391] k_vmm_manager: failed on sel4 hypervisor connection |-1|* Then when I log into linux and call `string_reverse <https://github.com/podhrmic/camkes-vm/tree/master/linux/pkg/string_reverse>` program, I get the following error: *# string_reverse * *[ 8.360164] BUG: unable to handle kernel paging request at d881f2c0* *[ 8.360164] IP: [<d00a69f0>] chrdev_open+0xab/0x100* *[ 8.360164] *pde = 17867067 *pte = 00000000 * *[ 8.360164] Oops: 0000 [#1]* *[ 8.360164] Modules linked in: emits_event(PO) dataport(PO)* *[ 8.360164] CPU: 0 PID: 691 Comm: string_reverse Tainted: P O 4.8.16 #1* *[ 8.360164] task: d79c9740 task.stack: d6ae0000* *[ 8.360164] EIP: 0060:[<d00a69f0>] EFLAGS: 00010286 CPU: 0* *[ 8.360164] EIP is at chrdev_open+0xab/0x100* *[ 8.360164] EAX: d881f2c0 EBX: 00000000 ECX: d79b0d00 EDX: 00000000* *[ 8.360164] ESI: d79b0d00 EDI: d6add808 EBP: d6ae1e10 ESP: d6ae1df8* *[ 8.360164] DS: 007b ES: 007b FS: 0000 GS: 0033 SS: 0068* *[ 8.360164] CR0: 80050033 CR2: d881f2c0 CR3: 16ad9000 CR4: 00102690* *[ 8.360164] DR0: 00000000 DR1: 00000000 DR2: 00000000 DR3: 00000000* *[ 8.360164] DR6: fffe0ff0 DR7: 00000400* *[ 8.360164] Stack:* *[ 8.360164] d7ac9be0 d7ac9be0 00000001 d7ac9be0 d6add808 00000000 d6ae1e30 d00a2370* *[ 8.360164] d6ae1e28 d7ac9be8 d00a6945 d7ac9be0 d69db010 d7462d80 d6ae1e4c d00a2cf8* *[ 8.360164] d79c2b80 d79c2b80 00000000 d6ae1ebc d7462d80 d6ae1eb0 d00ae159 d6ae1e64* *[ 8.360164] Call Trace:* *[ 8.360164] [<d00a2370>] do_dentry_open+0x197/0x216* *[ 8.360164] [<d00a6945>] ? cdev_put+0x1a/0x1a* *[ 8.360164] [<d00a2cf8>] vfs_open+0x45/0x4e* *[ 8.360164] [<d00ae159>] path_openat+0x822/0x970* *[ 8.360164] [<d007a468>] ? __alloc_pages_nodemask+0x11c/0x770* *[ 8.360164] [<d00ae2d8>] do_filp_open+0x31/0x77* *[ 8.360164] [<d00b6293>] ? __alloc_fd+0xbb/0xfe* *[ 8.360164] [<d00a2e56>] do_sys_open+0x54/0xc7* *[ 8.360164] [<d00a2ee1>] SyS_open+0x18/0x1a* *[ 8.360164] [<d0000ee1>] do_fast_syscall_32+0x7a/0xb8* *[ 8.360164] [<d047831f>] sysenter_past_esp+0x40/0x6a* *[ 8.360164] Code: 11 89 f0 e8 e1 fa ff ff 83 f8 01 19 db 31 d2 83 e3 fa 89 d0 e8 4d ff ff ff 85 db 75 59 8b 46 28 85 c0 75 0c* *[ 8.360164] EIP: [<d00a69f0>] chrdev_open+0xab/0x100 SS:ESP 0068:d6ae1df8* *[ 8.360164] CR2: 00000000d881f2c0* *[ 8.360164] ---[ end trace 46873a57a343e435 ]---* *[ 8.376285] string_reverse (691) used greatest stack depth: 6496 bytes left* *Killed* which seems like the program is trying to access memory that it is not supposed to. If I follow the example from wiki (here https://wiki.sel4. systems/CAmkESVM#Cross_VM_Connectors ) I get the same error, but triggered by `print_client` program. Have you seen a problem like this before? How do I correctly load the kernel module? Regards Michal

2 5

Using linux-tk1-debian on camkes-arm-vm
by Mike Clark 05 Jun '17

05 Jun '17

I have seL4 running on a TK1 using linux-tk1-initrd. I'd like to get the linux-tk1-debian version running to load the userspace off of the emmc drive of the TK1. FWIW, I did flash the TK1 to the latest verison, R21.5. The default DTS has root=/dev/mmcblk0p2 in the bootargs. When booting with this, I get a kernel panic. I also tried changing that to root=/dev/mmcblk0p1 (since that partition was the larger one on the emmc). It also gives a kernel panic, albeit a different message. With mmcblk0p1, the message I get is: [ 10.092841] EXT2-fs (mmcblk0p1): error: couldn't mount because of unsupported optional features (240) [ 10.102749] EXT4-fs (mmcblk0p1): couldn't mount as ext3 due to feature incompatibilities [ 10.137427] EXT4-fs (mmcblk0p1): mounted filesystem with ordered data mode. Opts: (null) [ 10.145696] VFS: Mounted root (ext4 filesystem) on device 179:1. [ 10.162679] devtmpfs: mounted [ 10.165845] Freeing unused kernel memory: 252K (c0aa9000 - c0ae8000) [ 10.224352] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.224352] [ 10.233480] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5 #1 [ 10.240429] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.246713] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.254457] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.261330] [<c009247c>] (panic) from [<c002566c>] (complete_and_exit+0x0/0x1c) [ 10.268627] [<c002566c>] (complete_and_exit) from [<00000000>] ( (null)) [ 10.275408] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 With mmcblk0p2, the message I get is: [ 10.095124] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.102907] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.111127] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.118994] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.126711] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.134472] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.142167] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.149983] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.159891] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.167669] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.175842] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.183743] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.191391] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.199146] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.206813] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.214653] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.222551] Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) [ 10.230976] CPU: 0 PID: 1 Comm: swapper Tainted: G W 4.3.0-rc5 #1 [ 10.238184] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.244462] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.252205] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.259079] [<c009247c>] (panic) from [<c0aaa238>] (mount_block_root+0x21c/0x230) [ 10.266554] [<c0aaa238>] (mount_block_root) from [<c0aaa368>] (mount_root+0x11c/0x124) [ 10.274459] [<c0aaa368>] (mount_root) from [<c0aaa4bc>] (prepare_namespace+0x14c/0x194) [ 10.282451] [<c0aaa4bc>] (prepare_namespace) from [<c0aa9dec>] (kernel_init_freeable+0x1c0/0x1d0) [ 10.291315] [<c0aa9dec>] (kernel_init_freeable) from [<c07c4b20>] (kernel_init+0x8/0xe8) [ 10.299397] [<c07c4b20>] (kernel_init) from [<c000f4d8>] (ret_from_fork+0x14/0x3c) [ 10.306959] ---[ end Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) Is there a guide for how to setup the emmc on the TK1 to boot using linux-tk1-debian? Will an older version of the TK1 image from Nvidia work or do I need to do a custom debian install (like this https://wiki.debian.org/InstallingDebianOn/NVIDIA/Jetson-TK1)?

2 3

Running Linux on top of seL4
by Daniel Wang 05 Jun '17

05 Jun '17

Hi all, Is there any guide about how to run Linux on top of seL4? Or has anyone done that before that can give me some hints? Thanks -Dan

4 6

Re: [seL4] 回复： camkes-manifest project make failed for arm
by Hesham.Almatary＠data61.csiro.au 02 Jun '17

02 Jun '17

Hi Talos, Are you following some instructions or getting started guides? e.g. camkes getting started guide [1] is using kzm config (arm_simple_defconfig). You can know which target at the time you're configuring the project by: 1) reading the *_defconfig you ran make with, 2) make menuconfig, 3) or after this from the .config file from where you run make *_defconfig or make menuconfig. Hope that helps. [1] https://sel4.systems/Info/CAmkES/GettingStarted.pml Best, Hesham ________________________________ From: talos <2486580938(a)qq.com> Sent: Friday, June 2, 2017 1:42 PM To: Almatary, Hesham (Data61, Kensington NSW) Subject: 回复： [seL4] camkes-manifest project make failed for arm Hi Hesham, How could I get which targets I used? Thanks for your patient! ------------------ 原始邮件 ------------------ 发件人: "Hesham.Almatary";<Hesham.Almatary(a)data61.csiro.au>; 发送时间: 2017年6月2日(星期五) 中午11:11 收件人: "talos"<2486580938(a)qq.com>; 抄送: "devel"<devel(a)sel4.systems>; 主题: Re: [seL4] camkes-manifest project make failed for arm Hi Talos, Thanks for reporting this. It seems like it’s an issue with KZM (ARMv6) targets which I assume you’re using? I submitted a fix, should be public on GitHub soon. Meanwhile, you can use the following patch to get around this error. diff --git a/include/util.h b/include/util.h index d6afdbb..4b05430 100644 --- a/include/util.h +++ b/include/util.h @@ -11,7 +11,6 @@ #ifndef __UTIL_H #define __UTIL_H -#define BIT(n) (1ul << (n)) #define MASK(n) (BIT(n)-1ul) #define IS_ALIGNED(n, b) (!((n) & MASK(b))) #define ROUND_DOWN(n, b) (((n) >> (b)) << (b)) @@ -23,6 +22,7 @@ #ifndef __ASSEMBLER__ #define NULL ((void *)0) +#define BIT(n) (1ul << (n)) #define PACKED __attribute__((packed)) #define NORETURN __attribute__((__noreturn__)) @@ -131,6 +131,10 @@ CONST popcountl(unsigned long x) } #define POPCOUNTL(x) __builtin_popcountl(x) +#else /* __ASSEMBLER__ */ + + +#define BIT(n) (1 << (n)) Cheers, Hesham On 2 Jun 2017, at 10:41 am, Hesham.Almatary(a)data61.csiro.au<mailto:Hesham.Almatary@data61.csiro.au> wrote: Hi Talos, This might be because of this change [1] to the kernel. Since this change has passed on our local machines, I'd be interested to know which toolchain version are you using (specifically binutils)? [1] https://github.com/seL4/seL4/commit/1930cf2e44908cb8faa5b315651bdb1958102f8f Cheers, Hesham ________________________________ From: Devel <devel-bounces(a)sel4.systems<mailto:devel-bounces@sel4.systems>> on behalf of talos <2486580938(a)qq.com<mailto:2486580938@qq.com>> Sent: Friday, June 2, 2017 9:59 AM To: devel Subject: [seL4] camkes-manifest project make failed for arm When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks! _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel

1 0

camkes-manifest project make failed for arm
by talos 02 Jun '17

02 Jun '17

When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks!

2 2

Re: [seL4] Devel Digest, Vol 37, Issue 2
by talos 02 Jun '17

02 Jun '17

Dear Hesham This is binutils information 2.26.1-1ubuntu1~16.04.4 Thanks ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Fri, Jun 2, 2017 08:56 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 37, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Running multiple VMs under ARM and C++ under SeL4? (John Backes) 2. camkes-manifest project make failed for arm (=?ISO-8859-1?B?dGFsb3M=?=) 3. Re: camkes-manifest project make failed for arm (Hesham.Almatary(a)data61.csiro.au) 4. Re: Running multiple VMs under ARM and C++ under SeL4? (Adrian.Danis(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 1 Jun 2017 11:41:49 -0500 From: John Backes <john.backes(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] Running multiple VMs under ARM and C++ under SeL4? Message-ID: <CAGzTpxHy_b+RWx33=xXv=vyEAwRttE3no-S21hwhqtBX6ZRG-w(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" Does the ARM VMM currently support running multiple virtual machines. Also, as a side question, how hard would it be to compile general C++ code that makes heavy use of the standard template library for use in a camkes component? I assume this would be non-trivial? - John -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170601/5de7f205/attachmen…> ------------------------------ Message: 2 Date: Fri, 2 Jun 2017 07:59:34 +0800 From: "=?ISO-8859-1?B?dGFsb3M=?=" <2486580938(a)qq.com> To: "=?ISO-8859-1?B?ZGV2ZWw=?=" <devel(a)sel4.systems> Subject: [seL4] camkes-manifest project make failed for arm Message-ID: <tencent_0DEA523F71A09CF508392575(a)qq.com> Content-Type: text/plain; charset="iso-8859-1" When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170602/a0e0e40f/attachmen…> ------------------------------ Message: 3 Date: Fri, 2 Jun 2017 00:41:15 +0000 From: <Hesham.Almatary(a)data61.csiro.au> To: <2486580938(a)qq.com>, <devel(a)sel4.systems> Subject: Re: [seL4] camkes-manifest project make failed for arm Message-ID: <1496364075337.38653(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Talos, This might be because of this change [1] to the kernel. Since this change has passed on our local machines, I'd be interested to know which toolchain version are you using (specifically binutils)? [1] https://github.com/seL4/seL4/commit/1930cf2e44908cb8faa5b315651bdb1958102f8f Cheers, Hesham ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: Friday, June 2, 2017 9:59 AM To: devel Subject: [seL4] camkes-manifest project make failed for arm When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170602/516c7463/attachmen…> ------------------------------ Message: 4 Date: Fri, 2 Jun 2017 00:56:24 +0000 From: <Adrian.Danis(a)data61.csiro.au> To: <john.backes(a)gmail.com>, <devel(a)sel4.systems> Subject: Re: [seL4] Running multiple VMs under ARM and C++ under SeL4? Message-ID: <ad050360-e6ef-eeb2-7130-dc66fb368f51(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi John, The ARM VMM does not currently support multiple virtual machines, this is something we are working on adding. To properly use the C++ standard template library you would need to build a cross compiler for a CAmkES system based seL4 system. This is something we have never done. Whether this is trivial or not depends entirely upon whether you find building cross compilers trivial or not. Adrian On Fri 02-Jun-2017 2:41 AM, John Backes wrote: Does the ARM VMM currently support running multiple virtual machines. Also, as a side question, how hard would it be to compile general C++ code that makes heavy use of the standard template library for use in a camkes component? I assume this would be non-trivial? - John _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170602/c454560f/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 37, Issue 2 ************************************

1 0

Running multiple VMs under ARM and C++ under SeL4?
by John Backes 02 Jun '17

02 Jun '17

Does the ARM VMM currently support running multiple virtual machines. Also, as a side question, how hard would it be to compile general C++ code that makes heavy use of the standard template library for use in a camkes component? I assume this would be non-trivial? - John

2 1

The path where the kernel jumps to apps
by shijun zhao 31 May '17

31 May '17

Hi, I’m tracing the path where sel4 kernel jumps to an application, such as hello-1. >From the Makefile for apps I know that the entry of the hello-1.bin is *_sel4_start* which is defined in the sel4_crt0.S (the directory is sel4_tutorials/projects/sel4_libs_libsel4platsupport/src/arch/arm). The *_sel4_start* function first calls a C function called *sel4_InitBootInfo*, and finally jumps to the *_start* function which is defined in the crt0.S. However the *_start* in crt0.S calls the sel4_InitBootInfo again. What confuses me is that the sel4_InitBootInfo function requires an input argument passed by R0, however the R0 has been set to zero in the _sel4_start function, so I think the calling of sel4_InitBootInfo in the _start will not run correctly. Or is the path where the kernel jumps to the app (_sel4_start->_start->main) wrong? I paste referred codes below: */******sel4_crt0.S********************/* _sel4_start: /* Setup a stack for ourselves. */ ldr sp, =_stack_top /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */ bl seL4_InitBootInfo ............ mov r0, #0 // *The R0 is modified, so it doesn't store the bootinfo structure anymore!* ............ /* Now go to actual _start */ ldr pc, =_start */*********crt0.S********************/* _start: /* Setup a stack for ourselves. */ ldr sp, =_stack_top */* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */* * bl seL4_InitBootInfo //Since R0 has been modified by _sel4_start, sel4_InitBootInfo will not run correctly.* /* Call constructors and other initialisation functions. */ bl _init /* Call main. */ bl main b exit Best Regards, Shijun Zhao

2 2

How to prove correctness of my own program?
by Adam Badura 30 May '17

30 May '17

I expect this might be (or even probably is) a bad place to ask this but at the same time I didn't find any better coming from the Contact Information page (http://sel4.systems/contact/) I'm working on a conference paper (not sure if I will make it but still trying to - code::dive <http://codedive.pl/> if anyone would be interested) about proving program correctness. Considering my own knowledge in the field and expected knowledge of the audience there would be nothing new in that paper - more like an update on what is the current state of the field. Yet I wanted to supply also some examples. As main example I would like to show proof (or at least parts of it) of correctness (adherence to specification) of C++ code, possibly reduced to C code if need be. After research in this topic and finding this project some time ago it felt natural to reuse its tools. But I fail to do so. Could you possibly guide me? Using your tools and techniques what should I do to prove correctness of some piece of code. I think source code level would be more than enough - for this task no need to verify binary in any form. As a side example I would like to show how your proves look like. I'm not sure what you are generating / writing as a proof (that gets later verified automatically). I imagine a sequence of something. Some formulas in natural deduction perhaps? Or something else? Whatever that would be I guess it must be pretty long so it is not like I would show and analyze it all but instead would like to somehow let the audience "feel the size". If - as I expect - this is not the right place to ask and you cannot help me with above questions, could you at least point me to where to ask them? Adam Badura

2 1

camkes-arm-vm not registering GPIO?
by Steven Johnston 30 May '17

30 May '17

Hi All, I am playing around with the capabilities of the camkes-arm-vm project pn the Tegra TK1 and and wondering if someone else has come across this issue. It looks like GPIO functionality is not available in the buildroot. I can confirm the GPIO source is present and is being built: camkes-arm-vm/libs/libplatsupport/rc/plat/tk1/gpio.c camkes-arm-vm/libs/libplatsupport/plat_include/tk1/platsupport/plat/gpio.h [CC] src/plat/tk1/gpio.o The expected sysfs support is not present and looking and the relevant dmesg: # dmesg | grep gpio [ 0.057543] gpiochip_add: GPIOs 0..255 (tegra-gpio) failed to register [ 1.485061] input: gpio-keys as /devices/soc0/gpio-keys/input/input0 Any thoughts on what could be causing GPIO to the failing to register? Steven

2 4

About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites
by Jesse-SC Chou (周書正) 26 May '17

26 May '17

Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse

2 2

CapDL Spec Error
by Chris Guikema 22 May '17

22 May '17

Hello All, Has anyone come across this error before? [GEN] imx6_net.cdl While forming CapDL spec: failed to find dataport symbol 'camkes router router_send_buf data' in ELF router_group_bin make[1]: *** [imx6_net.cdl] Error 255 make[1]: *** Deleting file `imx6_net.cdl' make: *** [imx6_net] Error 2 Thanks, Chris Guikema

2 4

Blog post: seL4, CAmkES, and L4v dependencies
by Luke.Mondy＠data61.csiro.au 19 May '17

19 May '17

Hello all, We have published a blog post about how we manage software dependencies within Trustworthy Systems, and how it has been adapted to produce a relatively user-friendly interface. It is relevant for people both new and old to the seL4 ecosystem, as it simplifies and compartmentalises the elaborate software dependencies sometimes required to get things to build. You can read the blog post here: https://research.csiro.au/tsblog/getting-started-sel4-camkes-l4v-dependenci… If you have any feedback or changes you would like made, please let us know on the GitHub repo. Cheers, Luke -- Luke Mondy, Systems Administrator, Trustworthy Systems DATA61 | CSIRO M +61 0415 281 991 | https://ts.data61.csiro.au

1 0

Is there has any seL4 project support ARM Cortex-A7 ?
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi Everyone, Is there has any seL4 project support ARM Cortex-A7 ? I found seL4 official projects in below link. https://github.com/seL4 https://github.com/SEL4PROJ I use sel4test project that repo from https://github.com/seL4/sel4test-manifest.git And I found Xilinx zynq7000 support ARM Cortex-A9 in sel4test like below. File: sel4test/projects/sel4test/master-configs/zynq7000_release_xml_defconfig # # seL4 System # # CONFIG_ARCH_X86 is not set CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y # CONFIG_ARM1136JF_S is not set # CONFIG_ARM_CORTEX_A8 is not set CONFIG_ARM_CORTEX_A9=y # CONFIG_ARM_CORTEX_A15 is not set # CONFIG_PLAT_EXYNOS54XX is not set I can’t find seL4 project support ARM cortex-A7. Does anyone find it? Thanks, Joyce Peng

3 3

sel4test data abort when boot strap test program
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi all, I tried to run seL4 test suite on my ARM Cortex-A7 target board. There is no error message when boot up seL4 kernel and boot strap test program on seL4 user land. But I got a “data abort” message after call sel4utils_map_page(..vaddr) and do memset(vaddr, 0, PAGE_SIZE_4K); There are some debug information list below. <1> I add debug message before the program that happen data abort diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c index c366a35..70d378a 100644 --- a/libsel4utils/src/vspace/bootstrap.c +++ b/libsel4utils/src/vspace/bootstrap.c @@ -107,13 +107,13 @@ static void *alloc_and_map(vspace_t *vspace, size_t size) { error = sel4utils_map_page(data->vka, data->vspace_root, frame.cptr, vaddr, seL4_AllRights, 1, objects, &num); + LOG_ERROR("my-hacker\n"); if (error) { vka_free_object(data->vka, &frame); LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error); return NULL; } + LOG_ERROR("my-hacker alloc_and_map() before memset vaddr=0x%x\n",vaddr); /* Zero the memory */ memset(vaddr, 0, PAGE_SIZE_4K); <2>Printed messages: ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p5 paddr=[20000000..2051881f] ELF-loading image 'kernel' paddr=[22000000..22032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[22033000..22463fff] vaddr=[8000..438fff] virt_entry=15f50 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() alloc_and_map@bootstrap.c:111 my-hacker alloc_and_map@bootstrap.c:119 my-hacker alloc_and_map() before memset() vaddr=0xdf7fe000 <3>When happen data abort, the value of CPU registers: r1:0 r3:0xdf7fe000 lr:0xcbe8 <4>Objdump sel4test-driver. 0000cbc8 <memset>: cbc8: e3520000 cmp r2, #0 cbcc: e92d4030 push {r4, r5, lr} cbd0: 08bd8030 popeq {r4, r5, pc} cbd4: e0803002 add r3, r0, r2 cbd8: e6ef1071 uxtb r1, r1 cbdc: e3520002 cmp r2, #2 cbe0: e5431001 strb r1, [r3, #-1] cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6 It seems to write virtual address 0xdf7ff000. <5>The virtual address 0xdf7fe000 is not map in page table It seems sel4utils_map_page() not create page table for user land program correctly. Can anyone help me, how to solve this problem? Thanks! Joyce Peng(彭美僑)

4 12

seL4 on Cortex-A5
by Andrew Gacek 19 May '17

19 May '17

Is there any support for seL4 on the Cortex-A5? -Andrew

3 2

Change Access Right to Memory Pages
by Norrathep Rattanavipanon 04 May '17

04 May '17

Hello, I have some questions about how to change access rights in seL4. (I'm using native seL4, not camkes) 1) Currently, I'm using seL4_ARCH_Page_Remap to change an access right (from R/W to R/O) to a specific page (of other processes) at run-time. I'm doing as follows: seL4_CPtr frame = vspace_get_cap(&(p.vspace), p.thread.stack_top-1); // only for the stack int error = seL4_ARCH_Page_Remap(frame, ppd.cptr, seL4_CanRead, seL4_ARCH_Default_VMAttributes); Am I doing it correctly? The code seems to work fine for me but I just want to double check. 2) If my understanding in 1) is correct, the remap function only takes 1 cap at a time. So if I want to modify access rights of many pages, do I have to call the remap function multiple times? Or is there a more efficient way to do so? 3) I am also curious how the kernel handles the remap function. Does it simply flip/change some bits? Or does it involve page-related operations as well? e.g. unmap that page first and then remap the same region with a new access right? I guess it should be the former but I need to be sure about that. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 7

seL4 Upgrading Issues
by Chris Guikema 04 May '17

04 May '17

Hello, I have developed an Ethernet application using CAmkES 2.2 and seL4 3.2. Because we are going to open-source the design and other documentation, I thought it would be a good idea to upgrade to the latest version of seL4 and CAmkES. I can pull the latest kernel and merge the compatible libraries with my changes and get everything to compile; however, when I load it on the board it fails... Failed to find any untyped capable of creating an object at address 0x20c4000 Failed to find a way to map address 0x20c4000 Failed to find any untyped capable of creating an object at address 0x20c8000 Failed to find a way to map address 0x20c8000 Failed to find any untyped capable of creating an object at address 0x20e0000 Failed to find a way to map address 0x20e0000 Failed to find any untyped capable of creating an object at address 0x21bc000 Failed to find a way to map address 0x21bc000 Here is my CAmkES configuration which sets up the Ethdrivers cnode and untypes. Keep in mind this works with seL4 3.2 ethdriver.simple = true; ethdriver.cnode_size_bits = 12; ethdriver.simple_untyped20_pool = 4; ethdriver.heap_size = 0; ethdriver.mmios = "0x02188000:0x4000:12, 0x021BC000:0x4000:12, 0x020E0000:0x4000:12, 0x020A4000:0x4000:12, 0x020B0000:0x4000:12, 0x020C4000:0x4000:12, 0x020C8000:0x1000:12"; Can anyone see the problem? Thanks, Chris Guikema

2 2

Re: [seL4] Memory protections within userspace and hardware/driver support
by Devin Harper 03 May '17

03 May '17

Hi, I read the whole FAQ. Does the "bug-free" protections for privacy apply to within each app of the same Linux virtual machine (overcoming memory bugs built in apps), between apps of the same Linux virtual machine (overcoming memory bugs built in the Linux kernel/GNU distro), or merely between different virtual machines (allowing any Linux kernel/GNU distro to be compromised, just not allowing them to compromise each other)? Furthermore, do I understand correctly that sel4 will only work on a few pieces of computer hardware, or will it work on everything the Linux kernel supports (has drivers for)? If sel4 will work on everything the Linux kernel supports (has drivers for), then do the same bug-free promises hold true on those hardwares in addition to the hardwares sel4 has already been tested on? Thanks!

2 1

Can I running camkes-arm-vm on HiKey board
by li94575 02 May '17

02 May '17

Hi all, Now, only exynos5 and tk1 are supported for running virtualised Linux on seL4. If I want to port it to HiKey board, is this possible?

3 2

questions about TK1 VM
by PX 01 May '17

01 May '17

Hi, all I have some questions about TK1 VM. I want to save the execution status of the TK1 VM. First, I stop the VM, then I use the function, seL4_TCB_ReadRegisters() to read the VM's registers into a buffer. Here are my questions: 1. Before I call the function, seL4_TCB_ReadRegisters(), do I need to flush TLB of CPU? If so, where is the library I need to check for this function? 2. The register values in the structure, seL4_UserContext, are VMM's physical addresses or virtual addresses? Best wishes Peng

2 1

sel4test failing TEST_SCHED0004 on iMX6
by Robert Kaiser 20 Apr '17

20 Apr '17

Hi all, I just tried to run the test suite on iMX6. Using the current version from github, I got this result: ---------------------------- ..... Test suite failed. 200/202 tests passed. 200/202 tests passed. *** FAILURES DETECTED *** ---------------------------- Further checking into the log shows this: ---------------------------- ..... Starting test 51: TEST_SCHED0004 TEST_SCHED0004 Running test SCHED0004 (Test threads at all priorities) _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object_at_maybe_dev@object.h:46 Failed to allocate cslot: error 1 new_pages_at_vaddr@vspace.c:331 Failed to allocate page sel4utils_configure_thread_config@thread.c:77 ipc buffer allocation failed Assertion failed: error == 0 ([.....]/seL4test/apps/sel4test-tests/src/helpers.c: create_helper_thread: 346) Failure: result == SUCCESS at line 343 of file [.....]/seL4test/apps/sel4test-driver/src/main.c Failure: Test check failure (see log). at line 0 of file ..... ---------------------------- The same test is run a second time further down below the log, giving the same result. I tested this on two different IMX6 platforms (SabreLite and Wandboard). Both showed identical results. Is this a known problem? Cheers Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postanschrift/Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

smaccm/sel4arm-vmm-manifest complie problem
by 高文博 19 Apr '17

19 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and complie it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao. -- 高文博数据通信科学技术研究所

2 1

smaccm/sel4arm-vmm-manifest compile problem
by 高文博 15 Apr '17

15 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and compile it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao.

1 0

how to debug libsel4allocman
by Vasily A. Sartakov 14 Apr '17

14 Apr '17

Greetings I am using a 4.0 compatible seL4 snapshot derived from mainline several months ago as a base for seL4/MIPS port. Currently, I am debugging sel4tests. My goal — make everything working before moving to hardware. By «everything» I mean different configurations of the system (optimization flags, syscall attributes, fast/slow path, etc). For example, most stable build uses «CONFIG_LIB_SEL4_INLINE_INVOCATIONS», less stable build, which I am debugging now, uses «CONFIG_LIB_SEL4_PUBLIC_SYMBOLS». This configuration crashes at the start when I am trying to allocate memory for the first test: Starting test suite sel4test Starting test 0: TEST_TRIVIAL0001 TEST_TRIVIAL0001 b24e68 b0cc4c b0cc2c b0cc2c sel4test-tests 0 0 * Loading segment 00400000-->005748a4 * Loading segment 00575000-->00689d84 alloc->num_cspace_slots = 30 alloc->num_cspace_slots = 29 alloc->num_cspace_slots = 28 alloc->num_cspace_slots = 27 alloc->num_cspace_slots = 26 alloc->num_cspace_slots = 25 alloc->num_cspace_slots = 24 alloc->num_cspace_slots = 23 alloc->num_cspace_slots = 22 alloc->num_cspace_slots = 21 alloc->num_cspace_slots = 20 alloc->num_cspace_slots = 19 alloc->num_cspace_slots = 18 alloc->num_cspace_slots = 17 alloc->num_cspace_slots = 16 alloc->num_cspace_slots = 15 alloc->num_cspace_slots = 14 alloc->num_cspace_slots = 13 alloc->num_cspace_slots = 12 alloc->num_cspace_slots = 11 alloc->num_cspace_slots = 10 alloc->num_cspace_slots = 9 alloc->num_cspace_slots = 8 alloc->num_cspace_slots = 7 alloc->num_cspace_slots = 6 alloc->num_cspace_slots = 5 alloc->num_cspace_slots = 4 alloc->num_cspace_slots = 3 alloc->num_cspace_slots = 2 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark alloc->num_cspace_slots == 0_refill_watermark:374 slota = 0 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark alloc->num_cspace_slots == 0_refill_watermark:374 slota = 0 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark I see, that: 243: error = alloc->cspace.alloc(alloc, alloc->cspace.cspace, slot); returns the error, and then we allocating memory from the watermark. In other builds (for example, with CONFIG_LIB_SEL4_INLINE_INVOCATIONS attributes), I do not see this issue - there are no errors on return. So, I need to debug function to be sure that I am receiving in the kernel proper arguments and so one, but I do not understand how this part of the code works. Do you have any documentation, or slides or just simple diagrams how this allocator work? What functions are responsible for generating error return, where exactly allocation is performed and how to debug this. Thank you.

1 0

Questions about userspace memory allocation
by Daniel (Xiaolong) Wang 11 Apr '17

11 Apr '17

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? Thanks -Dan

2 1

Questions about Userspace memory allocation
by Daniel Wang 09 Apr '17

09 Apr '17

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? Thanks -Dan

1 0

Creating process from not root process
by rad021993＠yandex.ru 02 Apr '17

02 Apr '17

Hi all, I try to create process (process2) from not root process (process1). Process1 has own cspace and vspace (fields 'create_cspace' and 'create_vspace' are set to true in process1' config). I try to create process2 like in the root process (4-th example in sel4 tutorials), but I can't obtain bootinfo to create allocman. As I understood it, this info available only from root process. Also I found function to create allocman via bootstrap function (like in example_bootstrap.c), but I also need to get process1' vspace and cspace to attach them to allocman. I do not understand, how I can get the needed info. Could you tell me how I can do it? Best regards, Rinat Dobrokhotov

2 1

Re: [seL4] Devel Digest, Vol 35, Issue 1
by talos 01 Apr '17

01 Apr '17

Re: 1. Re: errors when make camkes-tutorials-manifest the output of ls -al for my .stack directory: drwxrwxr-x 4 talos talos 4096 3月 29 17:19 .stack my username is talos Thanks ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sat, Apr 1, 2017 06:29 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 35, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: errors when make camkes-tutorials-manifest (Stephen.Sherratt(a)data61.csiro.au) 2. Announcing seL4 5.0.0 (Kent.Mcleod(a)data61.csiro.au) 3. Creating process from not root process (rad021993(a)yandex.ru) 4. Confusion with various memory address (Daniel (Xiaolong) Wang) ---------------------------------------------------------------------- Message: 1 Date: Fri, 31 Mar 2017 03:46:28 +0000 From: <Stephen.Sherratt(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] errors when make camkes-tutorials-manifest Message-ID: <1490931983542.96806(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Talos, Are you the owner of /home/talos/.stack ? For comparison, the output of ls -al for my .stack directory: drwxr-xr-x 10 ssteve ssteve 4096 Jan 24 15:25 .stack My username is ssteve. You could also try renaming your .stack directory so stack can create a new one for you. Cheers, Stephen ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: Thursday, 30 March 2017 9:28 PM To: devel Subject: [seL4] errors when make camkes-tutorials-manifest Hi, When I made this tutorials, there was an error; You are not the owner of '/home/talos/.stack/'. Aborting to protect file permissions. Retry with '--allow-different-user' to disable this precaution How can I do this, thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170331/b3b2c08e/attachmen…>

1 0

Confusion with various memory address
by Daniel (Xiaolong) Wang 01 Apr '17

01 Apr '17

Hi all, I have a probably a dumb question that need some clarification. I was reading the kernel source code and I’m little bit confused with the three data type: paddr_t, pptr_t, vptr_t and the following three data struct related to them. typedef struct region { pptr_t start; pptr_t end; } region_t; typedef struct p_region { paddr_t start; paddr_t end; } p_region_t; typedef struct v_region { vptr_t start; vptr_t end; } v_region_t; Based on how those are being used I assume the paddr_t and p_region are data struct for physical address, vptr_t and v_region are for virtual address. According to the following functions seem that the translation between physical address to pptr_r is by adding/subtracting a offset. But I’m confused with the pptr_t and region I wonder what are those for? Tank you very much! static inline void* CONST ptrFromPAddr(paddr_t paddr) { return (void*)(paddr + physMappingOffset); } static inline paddr_t CONST addrFromPPtr(void* pptr) { return (paddr_t)pptr - physMappingOffset; } static inline region_t CONST paddr_to_pptr_reg(p_region_t p_reg) { return (region_t) { p_reg.start + physMappingOffset, p_reg.end + physMappingOffset }; } static inline p_region_t CONST pptr_to_paddr_reg(region_t reg) { return (p_region_t) { reg.start - physMappingOffset, reg.end - physMappingOffset }; } Thanks -Dan

2 1

Announcing seL4 5.0.0
by Kent.Mcleod＠data61.csiro.au 31 Mar '17

31 Mar '17

We are pleased to announce the release of 5.0.0 of seL4. Listed below are a few of the key changes in this release: Below are the changes to the seL4 ABI and API: Generic changes: * Add missing case to seL4_getFault (seL4_Fault_DebugException) * Explicitly pack bootinfo data structures * Modify FinalizeLog syscall - Now returns a number of entries in the log * Extend bootinfo to support potentially arbitrary additional structures * Deprecate bootinfo management in libsel4 - a replacement, platsupport_get_bootinfo can be found in libsel4platsupport x86 specific changes: * Pass VBE information from multiboot through bootinfo * Remove PAE support x86-64 specific changes: * VT-x related cap and object definitions added * seL4_VMEnter syscall added arm specific changes: * ARM-HYP: VCPU interface for manipulating banked registers added * plat: added nvidia tx1 support * ARM-HYP: Add support for save/restore of debug registers * Add aarch64 implementation = Upgrade notes = * This release breaks both API and ABI and is not source compatible with the earlier versions. = Full changelog = Use {{{git log 4.0.0..5.0.0}}} in https://github.com/seL4/seL4 = More details = See the 5.0.0 manual (http://sel4.systems/Info/Docs/seL4-manual-5.0.0.pdf) included in the release for detailed descriptions of the new features. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/5.0.0.tar.gz [9e143c75c68edcaefc5506caea341890 5.0.0.tar.gz] Contributors: Adrian Danis Hesham Almatary Amirreza Zarrabi Kent McLeod Jack Suann Kofi Doku Atuah Amirreza Zarrabi Donny Yang Anna Lyons Stephen Sherratt Partha Susarla Thomas Sewell Frank Li Jeff Waugh Berkus Decker Corey Richardson Kent Mcleod Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Kent McLeod Kernel engineer DATA61 | CSIRO E kent.mcleod at data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

errors when make camkes-tutorials-manifest
by talos 31 Mar '17

31 Mar '17

Hi, When I made this tutorials, there was an error; You are not the owner of '/home/talos/.stack/'. Aborting to protect file permissions. Retry with '--allow-different-user' to disable this precaution How can I do this, thanks!

2 1

Allocation manager and processes
by Rinat Dobrokhotov 28 Mar '17

28 Mar '17

Hi all, 1. Could you check if my thoughts are right? The allocation manager is global object and there is only one instance for whole system. If I need in creation kernel objects I should create _one_ allocman above some array of memory. 2. I have the first question because I work with processes now. In the root process I create two different processes based on the elf image via allocman. Then I try to manage (suspend, change priority, etc.) process1 by process2. But I can't get process1 object from process2 because both of them belong to root process and belong to root process' memory space. As I understand it, I should copy cap which belongs to process1 to process2, then I will be able to manage them. Could you tell me if I am right? -- Best regards, Rinat Dobrokhotov

2 1

CapDL & RT
by Richard Habeeb 23 Mar '17

23 Mar '17

Hello all, I see that the master branch of CapDL has some support for the RT kernel, but I am having some trouble building it against the current public sel4 RT branch. Which version of the RT kernel does capDL work with? Or, is it still a work in progress? Thanks, Richard -- Richard Habeeb Research Assistant, Computer Science, USF PGP: https://goo.gl/VhmGGu https://habeebr.bitbucket.io/

2 1

sel4 kernel boot problem on i.mx6q board
by shijun zhao 21 Mar '17

21 Mar '17

Hi everyone, I am running sel4 on i.mx6q sabre board. I use the sabre_debug_xml_defconfig config file. However, the image stops at "Jumping to kernel-image entry point..." when I run it on the board. Following is the printed messages: ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2030081f] ELF-loading image 'kernel' paddr=[80000000..80032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[80033000..80406fff] vaddr=[10000..3e3fff] virt_entry=203d0 Enabling MMU and paging Jumping to kernel-image entry point... There are some warnings during compilation, all of which are caused by arm-none-eabi/bin/ld. And I see that the sel4 wiki shows how to solve the warnings: *To fix, do make menuconfig visit seL4 Libraries→Build musl C Library and untick libmuslc use precompiled archive then do make clean and attempt to rebuild.* However, there is no *Build musl C library* in my menuconfig, and there are only *libmuslc *and *libsel4muslcsys *options in the seL4 libraries. Can anyone tell me how to solve this problem? Thanks! Best Regards, Shijun

2 4

Help accessing physical address on zynq7000
by Brandon, Jeffrey - 0553 - MITLL 21 Mar '17

21 Mar '17

Hello, I've been getting started with seL4 on the zynq7000 and I am looking for resources on how to read/write physical memory for memory mapped io purposes. If there is a relevant tutorial or manual to reference I haven't come across it yet so I wanted to ask here. Any other guidance as to how to think about and work with capabilities would be useful at this stage. I'm working with a modified version of the sel4test repository. Looking at that I found env.simple (simple_t defined https://github.com/seL4/seL4_libs/blob/a1c031b0885dec4ddf1ee1f8866bcd23dcca6 ac3/libsel4simple/include/simple/simple.h) which seems to contain function pointers for some relevant functions to what I'm trying to do, but I am not entirely sure how to go about using them. What needs to be initialized first and how do I go about that? Any guidance greatly appreciated, Thanks. Jeff Brandon Associate Staff MIT Lincoln Laboratory 05-53 Secure Resilient Systems and Technology Ph: 781.981.9233

2 1

TK1 VMM SMMU Translation Error
by Enrique Leon 15 Mar '17

15 Mar '17

Hello All, We have recently run into an issue trying to boot the TK1 VMM on a TK1 Jetson board. The kernel tries to run but soon runs into translation errors after a couple of seconds. We are using the non-secure dtb with the initrd image. Here are some of the lines, it continues on like this and never stops. SMMU Address translation error: ID: 1 address: 0x0 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 SMMU Address translation error: ID: 1 address: 0x18fc00 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x SMMU Address translation error: ID: 1 address: 0x912c0 type: 6 direction: 0x0 We had success running the VM using the previous commit from camkes-arm-vmm repo, but the newest commit has introduced this issue. We have isolated it to line 93 in the "vmm_common.camkes" file. Removing "0x54200000:18", // Display A" from the file fixes the problem and we can boot as normal. We are also running Uboot 2010-10-rc5 as suggested by a email on the board. I am still new to working down to this level of code so any help in understanding this problem is appreciated.

3 3

Linux Virtualization on ODROID-XU4
by Norrathep Rattanavipanon 14 Mar '17

14 Mar '17

Hi, I tried to run Linux on top of seL4 in ODROID-XU4 device. I followed the instruction in https://sel4.systems/Community/Devdays/Workshop2016/ihor-sel4ws2016.pdf. I run with normal u-boot. And I got to the part that it printed out: We used 57776 CSlots (11.02% of our CNode) Done; suspending... Initialising UART driver Initialising UART driver Then it stops there. Any idea of what went wrong here? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 2

How to implement RM scheduling on seL4
by wang 07 Mar '17

07 Mar '17

Hello, I'm now studying seL4/seL4test and try to implement the RM scheduling on seL4test. I understand how the RM scheduling works, but just don't know how to make it happen on seL4test. So where can I start? In addition, I put the sel4test driver image on my board and run, it shows "206/206 tests passed. All is well in the universe" at the last line. Does it means that the seL4test project runs correctly? Thanks!

3 3

Using Rump kernels to run unmodified NetBSD drivers on seL4
by Kent.Mcleod＠data61.csiro.au 07 Mar '17

07 Mar '17

Last year for my honors thesis I evaluated rump kernels as a way of running unmodified NetBSD drivers on seL4. This work has recently been pushed out with a corresponding blog post: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbs…. This was done by adding support for the Rumprun unikernel to use seL4 as a target platform. Currently ia32 and x86_64 is supported and we have tested the e1000 network card driver and networking stack using Dell Sandy Bridge and Haswell machines. Rump kernels are a project that allows unmodified NetBSD OS component reuse in other systems (http://rumpkernel.org/) We want to use rump kernels as a way of providing drivers and other OS components such as filesystems and networking stacks on seL4 such as in CAmkES components. Some sample applications can be found here (https://github.com/SEL4PROJ/rumprun-sel4-demoapps) and a link to the thesis can be found here (http://www.disy.cse.unsw.edu.au/theses_public/16/kentm.pdf) Kent McLeod

2 1

ARM timer driver and interrupts
by Wladislav Wiebe 01 Mar '17

01 Mar '17

Hello, I wrote a new timer driver for this timer device: http://www.ti.com/lit/ug/sprugv5a/sprugv5a.pdf I am already able to run the seL4 testsuite successfully, except the interrupt/timer tests. It waits forever @ wait_for_timer_interrupt(env); I've uploaded the driver temporary to: https://github.com/wwladikw/devel/blob/master/timer.c Any idea what could be wrong? I am able to run the timer periodically or as oneshot. The gic_390 interrupt driver in the kernel should also be compatible with the gic_400, for my understanding, right? The SoC I am using contains a Coretex A15. Thanks a lot in advance! Wladislav Wiebe

3 9

Boot Hyp mode in elfloader
by SHI, Yao 27 Feb '17

27 Feb '17

I am trying to boot CAmkES-ARM-VM and got problem in elfloader. I tested Jetson-TK1 and TK1-SOM. The results are same. I've set bootm_boot_mode=nonsec in u-boot and tracked registers in function switch_to_hyp_mode(). 1) Enter switch_to_hyp_mode(), after asm volatile ("mrc p15, 0, %0, c1, c1, 0":"=r"(scr)); ==> scr == 0x100, in which NS==0, HCE==1, SCD==0, SIF==0 2) Then switch_to_hyp_mode() changes NS to 1, so scr==0x101 asm volatile ("mcr p15, 0, %0, c1, c1, 0"::"r"(scr)); 3) switch_to_hyp_mode() changes cpsr to Hyp mode asm volatile ("cps %0\n\t" "isb\n" ::"I"(HYPERVISOR_MODE)); 4) The final step, switch_to_hyp_mode() reads cpsr, asm volatile ("mrs %0, cpsr":"=r"(scr)); ==> scr == 0x6000001da, in which cpsr.M==0x1a, cpsr.I==1, cpsr.F==1, cpsr.A==1 Finally, the process died here. My questions are, 1) Are NS==0 and HCE==1 correct when entering switch_to_hyp_mode() ? 2) Is the final status (cpsr.F==cpsr.I==cpsr.A==1) expected? 3) Any other mistake I might make? Yao

2 4

Clarification on seL4 on RPi3b
by Joseph Adam Powers 23 Feb '17

23 Feb '17

It seems to be necessary for me to use the debug output using a serial cable on UART0 u-boot seems to be waiting for a Ethernet or serial cable connection to finish boot process. I don't have the serial cable so I just need some understanding that that is the case considering that I followed the rest of the instructions on the blog at https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ , newbie question btw.

2 1

RT and domains
by rad021993＠yandex.ru 22 Feb '17

22 Feb '17

Hi, Could you tell me why did you not implement domains in RT kernel version? Are there any difficulties? I'm going to add support of domains, and at the first sight I don't see any difficulties.

3 3

seL4 no longer support zynq7000 board?
by wang 22 Feb '17

22 Feb '17

Hello, https://wiki.sel4.systems/Hardware On this seL4wiki hardware page I find the link of Zynq7000 turns grey, and the page says "This page does not exist yet. You can create a new empty page, or use one of the page templates." So it means seL4 do not support zynq7000 any more? And how can I run seL4/seL4test on zynq7000 board? Thanks!

2 1

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

camkes DMA with predetermined physical addresses
by Gareth Howard 17 Feb '17

17 Feb '17

1 0

Deriving and Revoking IRQControl caps
by Andrew Gacek 16 Feb '17

16 Feb '17

Based on the seL4 manual it sounds like IRQControl caps only support one level of derivation. What is the reason for this restriction? We encountered a case where we wanted to hand out an IRQControl for a specific irq and then later revoke access, but we couldn't do it because the IRQControl for a specific irq is already a derived capability. -Andrew

5 10

imx6 U-Boot Issues
by Chris Guikema 16 Feb '17

16 Feb '17

Hello, I am using the i.mx6 to test a networking example that function in QEMU. To load the application, I am using the u-boot that comes pre-compiled on the micro-sd. I am able to dhcp to my tftpserver and grab the seL4 image, and when I run the "go 20000000" command, I get the following: ## Starting application at 0x20000000 ... AP Kernel returned back to the elf-loader. abort() called. Looking through the code, that error is in non_boot_main, yet that function call is wrapped by #ifdef CONFIG_SMP_ARM_MPCORE Which is undefined. That makes me think that the main() in boot.c is not being accessed and the elfloader isn't being run properly. Is this a u-boot issue, or is it that way I have everything setup? Is it a requirement to use the pre-compiled u-boot binary for the i.mx6? Thanks, Chris Guikema

2 2

CAmkES ARM VM boot on TK1
by SHI, Yao 15 Feb '17

15 Feb '17

Hi, I am trying to run CAmkES ARM VM on TK1. I downloaded built the image using: repo init -u https://github.com/SEL4PROJ/camkes-arm-vm-manifest repo sync make tk1_vm_defconfig make And then ran the image on the hardware. It stopped after loading seL4 in nonsecure HYP mode, Tegra124 (Jetson TK1) # bootelf CACHE: Misaligned operation at range [90000000, 90007408] CACHE: Misaligned operation at range [90007408, 9134c900] CACHE: Misaligned operation at range [9134c900, 9134c908] CACHE: Misaligned operation at range [91350000, 91360820] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001da Then I tried to build a monitor mode image and got this, Tegra124 (Jetson TK1) # bootelf CACHE: Misaligned operation at range [90000000, 90007250] CACHE: Misaligned operation at range [90007250, 9134c710] CACHE: Misaligned operation at range [91350000, 91360820] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..9136081f] ELF-loading image 'kernel' paddr=[80000000..80031fff] vaddr=[e0000000..e0031fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[80032000..8155bfff] vaddr=[10000..1539fff] virt_entry=17580 Enabling MMU and paging Jumping to kernel-image entry point... abort() called. Anyone may tell me the possible problem? Thank you very much. Yao

4 8

Coretex A15 periodic timer interrupts
by Wladislav Wiebe 14 Feb '17

14 Feb '17

Hello, I wonder if the generic timer https://github.com/seL4/util_libs/blob/master/libplatsupport/src/arch/arm/g… can be extended by timer->periodic timer->handle_irq to be able to run the sel4 testsuite which requires timer IRQ's such as https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… Right now I am able to get timer_get_time(env->timer->timer); by using the generic timer, but I am missing the periodic time and the irq handler for the Coretex A15 generic timer implementation. Some ideas if there is some tricky way to get it running? Thanks in advance! - Wladislav Wiebe

1 0

Re: [seL4] SDHC drivers (cont.)
by Norrathep Rattanavipanon 13 Feb '17

13 Feb '17

Hi Siwei, So, I tried the code using Kingston microSDHC but it still couldnt read the card. However, the code works perfectly when loaded from the SD slot (with microSD to SD adapter), instead of the microSD slot. I also found that for some reasons, if mmc dev 1 is used in u-boot, the program wouldnt be able to read/write the micro-sd card. I'm kind of good for now but still curious about that. Do you have any idea what might have caused this? Best, Oak On Mon, Jan 23, 2017 at 11:07 AM, Norrathep Rattanavipanon <nrattana(a)uci.edu > wrote: > Thanks Siwei. I really appreciate your help. > Yeah so I tried your image with three different micro-sd cards and none of > them works (still stuck after printing the card's capacity). > I'll buy Kingston microsdhc class 4 and try on that, will let you know if > it works or not. > > Best, > Oak > > On Mon, Jan 23, 2017 at 12:03 AM, <Siwei.Zhuang(a)data61.csiro.au> wrote: > >> Hi Oak, >> >> >> Here is what exactly I did, >> >> >> $ mkdir sel4-sdcard >> >> $ cd sel4-sdcard >> >> $ repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest.git >> -m sel4-tutorials-master.xml >> >> $ repo sync >> >> $ cd projects >> >> $ git clone https://github.com/SEL4PROJ/projects_libs.git >> >> $ cd ../libs >> >> $ ln -sf ../projects/projects_libs/libsdhcdrivers libsdhcdrivers >> >> $ ln -sf ../projects/seL4_libs/libsel4sync libsel4sync >> >> >> Then, I copied my sdcard app into sel4-sdcard/apps. >> >> The sdcard app directory has Kconfig, Kbuild, Makefile and src/main.c >> >> >> ------------ Kconfig ---------------- >> menuconfig APP_SDCARD >> bool "SD card" >> default y >> depends on HAVE_LIBC >> depends on LIB_SEL4_PLAT_SUPPORT >> depends on LIB_SEL4_VKA >> depends on LIB_SEL4_UTILS >> depends on LIB_UTILS >> depends on LIB_CPIO >> depends on LIB_SEL4 >> depends on LIB_ELF >> help >> SD card app. >> >> >> >> ------------ Kbuild ----------------- >> apps-$(CONFIG_APP_SDCARD) += sdcard >> >> sdcard: common libsel4utils libutils libsel4 libmuslc libsel4muslcsys \ >> libsel4vka libsel4allocman libsel4vspace libsel4simple >> libsel4simple-default \ >> libsel4platsupport libsel4platsupport libcpio libelf \ >> libsel4sync libsdhcdrivers libsel4debug >> >> ------------ Makefile --------------- >> # Targets >> TARGETS := sdcard.bin >> >> ENTRY_POINT := _sel4_start >> >> # Source files required to build the target >> CFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard >> $(SOURCE_DIR)/src/*.c)) >> ASMFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard >> $(SOURCE_DIR)/src/*.S)) >> OFILES := archive.o >> >> # Libraries required to build the target >> LIBS = c sel4 sel4muslcsys sel4vka sel4allocman \ >> platsupport sel4platsupport sel4vspace elf \ >> sel4utils sel4simple utils sel4simple-default cpio \ >> sel4sync sdhcdrivers sel4debug >> #CFLAGS += -Werror >> >> include $(SEL4_COMMON)/common.mk >> >> archive.o: ${COMPONENTS} >> $(Q)mkdir -p $(dir $@) >> ${COMMON_PATH}/files_to_obj.sh $@ _cpio_archive $^ >> >> >> I also edited sel4-sdcard/Kconfig, added the following to the related >> menus, >> >> source "apps/sdcard/Kconfig" >> >> source "libs/libsdhcdrivers/Kconfig" >> >> source "libs/libsel4sync/Kconfig" >> >> >> I've attached the config file, copy it to configs directory, then do >> "make sdcard_defconfig". >> >> I've also attached the binary image that I compiled. >> >> >> Since the u-boot command works, it doesn't seem that the controller is >> disabled. Also try another card if possible, my card is Kingston micro SDHC >> class 4. The driver only implements very basic single block read/write. I'm >> not surprised that it doesn't work for some cards. >> >> >> - Siwei >> >> >> ------------------------------ >> *From:* Norrathep Rattanavipanon <nrattana(a)uci.edu> >> *Sent:* Monday, 23 January 2017 4:59 PM >> *To:* Zhuang, Siwei (Data61, Kensington NSW) >> >> *Subject:* Re: [seL4] SDHC drivers (cont.) >> >> Hi Siwei, >> >> Thank you for helping me out. I am still unable to get it to work even if >> using your code with the latest kernel (4.0) and latest libraries >> (downloaded from https://github.com/SEL4PROJ/sel4-tutorials-manifest >> master branch) >> >> I also tried calling mmc read command in u-boot and it was able to read >> data from the card just fine. >> I'm not really sure how I can check if the host controller works >> properly. Do you mean I can do it in seL4? >> >> Also, is it possible if you can upload the binary image file (and the >> build config) so that I can test on my board really quick? I suspect that >> either I miss something for the build or my micro-sd is not working. >> >> Thank you again for your help, >> Oak >> >> On Thu, Jan 19, 2017 at 11:12 AM, Norrathep Rattanavipanon < >> nrattana(a)uci.edu> wrote: >> >>> Hi Siwei, >>> >>> Yes, I believe mmc_card_capacity returns the correct value (4026531840 >>> <(402)%20653-1840> - my microsd is 4GB). >>> >>> And my code does not do any interrupt handling. In fact, that's all the >>> code in the root userspace process (besides initializing vka, vspace and >>> simple objects) and there is no other process. >>> >>> I also tried using a callback as mmc_block_read's argument, instead of >>> using NULL, but it also does not work. >>> >>> On Wed, Jan 18, 2017 at 8:41 PM, <Siwei.Zhuang(a)data61.csiro.au> wrote: >>> >>>> Hi Oak, >>>> >>>> >>>> Do you get the correct card capacity by calling mmc_card_capacity? If >>>> you don't, you'd need to check if the hardware is enabled in your >>>> bootloader. >>>> >>>> >>>> Are you doing any interrupt handling? As you don't supply a callback >>>> function to mmc_block_read, the read function would block until the >>>> hardware responses. In this case, mmc_block_read handles the interrupt >>>> itself. It would trigger a dead lock if you also handles the interrupt. >>>> >>>> >>>> - Siwei >>>> >>>> >>>> ------------------------------ >>>> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Norrathep >>>> Rattanavipanon <nrattana(a)uci.edu> >>>> *Sent:* Thursday, 19 January 2017 9:54 AM >>>> *To:* Danis, Adrian (Data61, Kensington NSW) >>>> *Cc:* devel(a)sel4.systems; GTS >>>> *Subject:* Re: [seL4] SDHC drivers (cont.) >>>> >>>> Hi Adrian, >>>> >>>> Thank you for the reply. I fix it according to what you suggest but it >>>> still does not solve the problem (still hang at the same place. Do you have >>>> any other suggestions on what I should fix or how I should look into >>>> debugging it? >>>> >>>> Best, >>>> Oak >>>> >>>> On Tue, Jan 17, 2017 at 8:58 PM, <Adrian.Danis(a)data61.csiro.au> wrote: >>>> >>>>> Hi Oak, >>>>> >>>>> I don't know much about SD cards or this driver but it seems to me >>>>> like passing it a physical address of 0 isn't what you want, and whilst I >>>>> know nothing about the mmc hardware it seems reasonable to me that it might >>>>> hang trying to DMA to memory that doesn't exist. There is also the >>>>> additional problem that even if paddr was correct for the first page, there >>>>> is no guarantee that the 5 pages you have allocated are contiguously >>>>> physically even though they will be mapped contiguous virtually. >>>>> >>>>> My recommendation is to use the page dma allocator in >>>>> seL4_libs/libsel4utils/include/sel4utils/page_dma.h, this will >>>>> provide you an easy way to allocate/map pages for the purposes of DMA. So >>>>> instead of >>>>> >>>>> void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); >>>>> uintptr_t paddr = 0; >>>>> >>>>> You would have >>>>> >>>>> ps_dma_man_t dma_man; >>>>> error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); >>>>> void *vaddr = ps_dma_alloc(&dma_man, 5 * PAGE_SIZE_4K, PAGE_SIZE_4K, >>>>> 0, PS_MEM_NORMAL); >>>>> uintptr_t paddr = ps_dma_pin(&dma_man, vaddr, 5 * PAGE_SIZE_4K); >>>>> >>>>> As I said at the start, I don't know if this will actually fix your >>>>> current problem, but it's still something you will need to fix. >>>>> >>>>> Adrian >>>>> >>>>> >>>>> On Wed 18-Jan-2017 6:31 AM, Norrathep Rattanavipanon wrote: >>>>> >>>>> My apology that I have to continue the discussion from the old thread: >>>>> (http://sel4.systems/pipermail/devel/2016-October/001056.html) >>>>> My goal is to read and write data from/to micro sd in SabreLite >>>>> platform. >>>>> I tried both Adrain and Anna's suggestions in that thread and they >>>>> dont seem to fix the problem. Nothing returns error and I also changed >>>>> cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is >>>>> what Anna meant instead of setting 3rd argument of vspace_new_pages). >>>>> >>>>> The code's still stuck inside mmc_block_read function. I tracked it >>>>> down and it seems like BRR and BWR interrupt statuses are never set to 1 >>>>> I add my code below, please let me know if anything is wrong with my >>>>> code. >>>>> >>>>> ps_io_mapper_t io_mapper = {0}; >>>>> error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); >>>>> assert(error == 0); >>>>> >>>>> ps_io_ops_t io_ops = { >>>>> .io_mapper = io_mapper >>>>> }; >>>>> >>>>> sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); >>>>> assert(dev != NULL); >>>>> memset(dev, 0, sizeof(*dev)); >>>>> >>>>> enum sdio_id id = sdio_default_id(); // return id=3 >>>>> error = sdio_init(id, &io_ops, dev); >>>>> assert(error == 0); >>>>> >>>>> mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); >>>>> error = mmc_init(dev, &io_ops, mmc_card); >>>>> assert(error == 0 && mmc_card != NULL); >>>>> >>>>> void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); >>>>> assert(vaddr != NULL); >>>>> >>>>> uintptr_t paddr = 0; >>>>> printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); >>>>> long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here >>>>> printf("read %lu bytes\n", read_len); >>>>> >>>>> >>>>> >>>>> Thanks >>>>> Oak >>>>> >>>>> >>>>> >>>>> -- >>>>> Norrathep (Oak) Rattanavipanon >>>>> M.S. in Computer Science >>>>> University of California - Irvine >>>>> >>>>> >>>>> _______________________________________________ >>>>> Devel mailing listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel >>>>> >>>>> >>>>> >>>> >>>> >>>> -- >>>> Norrathep (Oak) Rattanavipanon >>>> M.S. in Computer Science >>>> University of California - Irvine >>>> >>> >>> >>> >>> -- >>> Norrathep (Oak) Rattanavipanon >>> M.S. in Computer Science >>> University of California - Irvine >>> >> >> >> >> -- >> Norrathep (Oak) Rattanavipanon >> M.S. in Computer Science >> University of California - Irvine >> > > > > -- > Norrathep (Oak) Rattanavipanon > M.S. in Computer Science > University of California - Irvine > -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

seL4 on Zedboard
by Brandon, Jeffrey - 0553 - MITLL 01 Feb '17

01 Feb '17

Hi, I've been trying to get seL4 running on a Zedboard and I was wondering if there was any documentation on how to boot sle4 from an SD card. I've read http://sel4.systems/pipermail/devel/2016-December/001160.html and https://sel4.systems/Info/Hardware/General/ which mentions using ${loadaddr} but that doesn't seem to be defined on the Zedboard's u-boot. So far I've compiled the image targeting the zynq7000 and used the mkimage command from the general hardware page to try u-boot's fastboot, but fastboot doesn't seem to be available on the zynq either. I am a bit of a novice here. I worry that the solution may be simple but I am currently taking shots in the dark. I wanted to ask this list for any resources you may be aware of for getting sel4 test cases running on the Zed. Thanks for the help, Jeff Brandon 05-53 Secure Resilient Systems and Technology

2 3

arm_data_abort_exception
by Wladislav Wiebe 31 Jan '17

31 Jan '17

Hello, has somebody experience with running into arm_data_abort_exception after enabling the MMU/paging and jumping to the kernel image: .. ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4 paddr=[90000000..904b041f] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'sel4test-driver' paddr=[80034000..8042dfff] vaddr=[10000..409fff] virt_entry=1e924 Enabling MMU and paging Jumping to kernel-image entry point... check_data_abort_exception() DFAR = 0xfff01014 DFSR = 0x7 ADFSR = 0x0 abort() called. I've dumped the DFAR/DFSR register -- Relevant config parts about the setup: CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y CONFIG_ARM_CORTEX_A15=y CONFIG_PLAT_KEYSTONE=y Thanks in advance! -- WBR, Wladislav WIebe

2 12

Exposing ticks to the rt API
by Corey Richardson 30 Jan '17

30 Jan '17

Hi Anna, While analyzing some time related APIs, I've noticed that the x86 rt kernel assumes that the tsc frequency is constant and well represented by the measurement made at init by comparing against the PIT. It also exposes only microseconds and uses the internal calibration to convert that to/from ticks. I'm concerned about this behavior. The tsc can have up to 200ppm error if uncalibrated and not temperature controlled, from what I'm able to determine. I'd rather have all the public APIs take ticks and allow user space to determine how their timing requirements best correspond to ticks. This came up when wanting to measure how much running time a process/thread has used. Ideally, it's kept as a running count of ticks. In the current API, one can only observe microseconds consumed, converted by a potentially lossy ticksToUs (lossy when the rate isn't exactly known or tick->us conversion isn't an exact integer multiplication). It'd be more useful for me to have tick count directly. I'm also somewhat concerned with using the PIT to estimate the TSC rate, as I can't find anything about expected error of the PIT, and any slop there will influence all future kernel behaviors until reboot. One potential alternative is the ACPI PM timer or the HPET. Those run at higher frequencies, which would help reduce the error bounds on the rate estimation. Let me know what you think! If it's useful at all, I've written up some stuff about the work that inspired these thoughts: https://gitlab.com/robigalia/meta/blob/master/blog/_drafts/2016-12-23-what-… Merry Christmas, -- cmr http://octayn.net/

4 4

strange code in thread.c
by Berkus 30 Jan '17

30 Jan '17

Hi! Details here https://github.com/seL4/seL4/issues/57 do you guys keep an eye on github activity actually or it’s a bad medium for communcation?

2 1

I2C Driver for BeagleBone (AM335x) for CAmkES
by Richard Habeeb 25 Jan '17

25 Jan '17

Hey all, Has anyone setup I2C on a Beaglebone CAmkES application? Is the code in libplatsupport all that's needed? The i2d_id enum doesn't seem to include all the i2c modules ( https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…) I didn't see an init function for the i2c_bus for am335x; for example, exynos uses the exynos_i2c_init. Any help is appreciated. Thanks, Richard -- Richard Habeeb Research Assistant, Computer Science, USF PGP: https://goo.gl/VhmGGu https://habeebr.bitbucket.io/

1 0

ARM LPAE?
by Wladislav Wiebe 21 Jan '17

21 Jan '17

Hello, I am trying to integrate TI Keystone 2 platform to seL4. What I have done so far is basically an initial port of the Kernel/libs/elfloader/Platform components and introducing a new keystone defconfig. Relevant config parts about the setup: CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y CONFIG_ARM_CORTEX_A15=y CONFIG_PLAT_KEYSTONE=y At the end I am able to generate an image which looks like: $ arm-cortexa15-linux-gnueabihf-readelf -e images/sel4test-driver-image-arm-keystone ELF Header: Class: ELF32 .. Entry point address: 0xc0008000 .. (I am using the same entry point as Linux use it) So far, it stops booting in the elfloader -- output log: .. [ 29.705] ## Starting application at 0xc0008000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4 paddr=[c0008000..c032841f] -> Stop here <- Seems it stops loading @ elf_getMemoryBounds(). I suppose it is related to fact that the physical start address starts @ 0x840000000 which is beyond 32 Bit - so, LPAE support is required. The physical RAM setup looks like: bank 0: addr: 0x840000000 size: 0x17ec5000 (382 MB) bank 1: addr: 0x880000000 size: 0x80000000 (2048 MB) Do you have an idea if this is supposed to be supported on seL4? What should be the "physBase" and the "kernelBase" for such a setup? How should the "static const p_region_t BOOT_RODATA avail_p_regs" looks like? Thanks in advance! -- WBR, Wladislav WIebe

3 10

Re: [seL4] SDHC drivers (cont.)
by Siwei.Zhuang＠data61.csiro.au 20 Jan '17

20 Jan '17

Hi Oak, I tried your code. It works for me except that it seems that you are using old versions of seL4 kernel and libraries. Attached is the code I'm using, I merely add some initialization code to your code. It should work on the latest version of seL4 kernel and related libraries. If the code doesn't work for you. I would suggest, 1. If you are using u-boot, try its mmc command, see if you can access the card. 2. Have a look at the imx6 reference manual, chapter 67.2 and 67.3, check if the host controller is enabled properly. - Siwei ________________________________ From: Norrathep Rattanavipanon <nrattana(a)uci.edu> Sent: Friday, 20 January 2017 6:12 AM To: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: [seL4] SDHC drivers (cont.) Hi Siwei, Yes, I believe mmc_card_capacity returns the correct value (4026531840 - my microsd is 4GB). And my code does not do any interrupt handling. In fact, that's all the code in the root userspace process (besides initializing vka, vspace and simple objects) and there is no other process. I also tried using a callback as mmc_block_read's argument, instead of using NULL, but it also does not work. On Wed, Jan 18, 2017 at 8:41 PM, <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Oak, Do you get the correct card capacity by calling mmc_card_capacity? If you don't, you'd need to check if the hardware is enabled in your bootloader. Are you doing any interrupt handling? As you don't supply a callback function to mmc_block_read, the read function would block until the hardware responses. In this case, mmc_block_read handles the interrupt itself. It would trigger a dead lock if you also handles the interrupt. - Siwei ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Norrathep Rattanavipanon <nrattana(a)uci.edu<mailto:nrattana@uci.edu>> Sent: Thursday, 19 January 2017 9:54 AM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel(a)sel4.systems; GTS Subject: Re: [seL4] SDHC drivers (cont.) Hi Adrian, Thank you for the reply. I fix it according to what you suggest but it still does not solve the problem (still hang at the same place. Do you have any other suggestions on what I should fix or how I should look into debugging it? Best, Oak On Tue, Jan 17, 2017 at 8:58 PM, <Adrian.Danis(a)data61.csiro.au<mailto:Adrian.Danis@data61.csiro.au>> wrote: Hi Oak, I don't know much about SD cards or this driver but it seems to me like passing it a physical address of 0 isn't what you want, and whilst I know nothing about the mmc hardware it seems reasonable to me that it might hang trying to DMA to memory that doesn't exist. There is also the additional problem that even if paddr was correct for the first page, there is no guarantee that the 5 pages you have allocated are contiguously physically even though they will be mapped contiguous virtually. My recommendation is to use the page dma allocator in seL4_libs/libsel4utils/include/sel4utils/page_dma.h, this will provide you an easy way to allocate/map pages for the purposes of DMA. So instead of void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); uintptr_t paddr = 0; You would have ps_dma_man_t dma_man; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); void *vaddr = ps_dma_alloc(&dma_man, 5 * PAGE_SIZE_4K, PAGE_SIZE_4K, 0, PS_MEM_NORMAL); uintptr_t paddr = ps_dma_pin(&dma_man, vaddr, 5 * PAGE_SIZE_4K); As I said at the start, I don't know if this will actually fix your current problem, but it's still something you will need to fix. Adrian On Wed 18-Jan-2017 6:31 AM, Norrathep Rattanavipanon wrote: My apology that I have to continue the discussion from the old thread: (http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 0

seL4 System Utilization / Benchmark
by Andrew Gacek 20 Jan '17

20 Jan '17

Hi, I'm interested in seeing how much of the CPU is being used by the various threads in my (camkes) application. I'd like a simple "Task Manager" style report of the form: 70% idle 25% can_obj_7_0_control_9_tcb 5% can_obj_7_Int_3_0000_tcb 0% can_obj_7_0_fault_handler_15_0000_tcb etc I've tried poking around libsel4bench, but I don't see any obvious way of benchmarking the whole system. From what I can tell, it's mostly designed to get cycle counts from specific code segments. Is that right? What's the best way to go about benchmarking the whole system? It's only for debugging, so I'm willing to make some quick-and-dirty changes to the kernel just to see the results. Thanks, Andrew

4 11

SDHC drivers (cont.)
by Norrathep Rattanavipanon 19 Jan '17

19 Jan '17

My apology that I have to continue the discussion from the old thread: ( http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 3

CAmkES Templates
by Chris Guikema 19 Jan '17

19 Jan '17

Hello, I am working on a CAmkES application attempting to build a seL4 Network Stack. I am basing this on the CAmkES-VM and utilizing UDP Protocol with the lwIP library. During my build process, I get quite a few linking errors like this: undefined reference to `pbuf_alloc' This is odd, because in the templates, the proper header files are being linked in. There are also warnings like this: Warning: no template for ethdriver_1.to.source Even though the connection does exist: connection seL4Ethdriver eth_driver(from router.ethdriver, to ethdriver.client); Is there something obvious I am doing wrong? Thanks Chris

2 2

questions about SMMU on TK1 VMM
by PX 18 Jan '17

18 Jan '17

Hi, I have some questions about the SMMU on the new version of TK1 VMM as follows: 1. In the source code, smmu.c, the IO ASID 1 is assigned to hardware engine, AFI, which is supposed to connect with PCIE devices. However, when I add 1 to vm.smmu in vm.camkes, the VM can not access Ethernet and cause a SMMU translation error. But it works if I add 0 to vm.smmu as suggested by Kent. whats the reason to do so? 2. Each IO device is assigned with an IO space mapping. However, there is no IO ASID associated with these mappings. Does that means these mappings are associated with an IO ASID in the order given in vm.smmu? 3. Is it possible for the VMM to change the IO mapping for a specific device? say, invalidate old mapping and load a new mapping? what's the rough idea to do so? thanks Peng

2 1

questions about PCIE SMMU for tk1 vmm
by PX 16 Jan '17

16 Jan '17

Hi, I am confused by the SMMU management for PCIE device in the updated TK1 VMM. The IO ASID for PCIE device is 0. However, the start IO ASID is from 1 as defined in smmu.h. When initialized, the lookup table, smmu_ioasid_to_pd, has no entry for IO asid 0 at all. I don't understand how the page table for PCIE device is generated and used by SMMU? which part source code should I check ? thanks Peng

2 1

Re: [seL4] quesitons about TK1 VMM
by Kent.Mcleod＠data61.csiro.au 14 Jan '17

14 Jan '17

Hi Peng, Adding the ethernet card requires adding the 0 ASID in the vm.camkes file that I mentioned in the previous email. vm.smmu = [0, 10, 24]; This gives permission for PCIE devices to read and write to memory. I confirmed that on the TK1 Jetson the ethernet port works after this change. You may need to run "ifconfig eth0 up" to enable the device once the image boots. Regards, Kent. ? ________________________________ From: PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 12:13 PM To: Mcleod, Kent (Data61, Kensington NSW) Subject: Re: quesitons about TK1 VMM Kent, I am using NVIDIA Jetson TK1 board. The reason I want to use insecure config is to enable VM Linux to use Ethernet port. I do not care about the SD card. How can I just add Ethernet card? is there a way for me to avoid adding SD card to The VM linux as you just suggest in your email? Thanks Peng On Thursday,January 12, 2017, <Kent.Mcleod(a)data61.csiro.au<mailto:Kent.Mcleod@data61.csiro.au>> wrote: Hi Peng, Which hardware are you using to run the image? This project has only been tested on the TK1-SOM made by Colorado Engineering. The ethernet port doesn't work as the version of Linux that we use doesn't support it. As for your second question, we configure the IOMMU to only let Linux use the emmc device and USB device on the TK1-SOM. The error is caused because Linux is trying to access a SD card device that it isn't authorized to access. The TK1-SOM doesn't have any SD card hardware so camkes doesn't set up access. If you want to use the Insecure config then you will need to modify apps/vm/vm.camkes and add the right ID to vm.smmu on line 443. To find out which ID to add we take the ID:98 from your Address translation error and look it up in the TK1 technical reference manual. In the memory controller section of the manual there is a "Error Data Capture: Status" section that starts on page 716. Using the table there you can look up ID:98 to see that it belongs to the SWGROUP sdmmc3a. We can now take this and look in seL4 ("kernel/include/plat/tk1/plat/machine/smmu.h?") to find the relevant ASID. From the list of ASIDs we see that SMMU_SDMMC3A_ASID is defined as 23. This is the ID that needs to be added to the vm.smmu array in vm.camkes. Hope this helps, Regards, Kent. ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 9:03 AM To: devel(a)sel4.systems Subject: [seL4] quesitons about TK1 VMM Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

2 1

quesitons about TK1 VMM
by PX 13 Jan '17

13 Jan '17

Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

1 0

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 13 Jan '17

13 Jan '17

Hi, all I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to build "camkes-accelerator" . I don't put any new code yet. I just: 1) repo init the url ; 2) repo sync; 3) make tk1_vm_defconfig; and 4) make. Did I do something wrong here? thanks Peng

2 5

Overly eager xsave size rejection
by Corey Richardson 12 Jan '17

12 Jan '17

in src/arch/x86/machine/fpu.c:140 on 4.0.0, there is > if (x86_cpuid_ebx(0x0d, 0x0) != CONFIG_XSAVE_SIZE) { > printf("XSAVE buffer set set to %d, but should be %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ebx(0x0d, 0x0)); > return false; > } I want to force a large(r than 576) xsave region so that TCBBits is always 11, to help my userspace be vaguely more kernel-config-independent. I don't think it's a problem if the xsave buffer in the TCB is larger than the hardware will actually use? I also think this is buggy. Shouldn't it be querying ecx, since things like AVX aren't enabled in the kernel? To be clear, this is my suggested change: > if (x86_cpuid_ecx(0x0d, 0x0) > CONFIG_XSAVE_SIZE) { > printf("XSAVE buffer set set to %d, but should be at least %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ecx(0x0d, 0x0)); > return false; > } -- cmr http://octayn.net/ +16038524272

2 5

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 12 Jan '17

12 Jan '17

Hi, all I posted this question yesterday, and get no answer. Let me to be more specific this time. I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to parse capDL. The errors are appended as follows: " make: Entering directory '/home/dev/Documents/new_vmm/projects/capd /capDL-tool' stack setup make: stack: Command not found Makefile:37: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/home/dev/Documents/new_vmm/projects/capdl/capDL-tool' Makefile:51: recipe for target '/home/dev/Documents/new_vmm/stage/arm/tk1/parse-capDL/parse-capDL' failed " I checked that there is a file called stack.ymal in the directory: ~/capdl/capDL-tool. My system is also installed latest ghc and ghc-prof. Anybody can help me on this problem? Thanks Peng

3 3

Using the seL4 Benchmark Tool
by Chris Guikema 12 Jan '17

12 Jan '17

Hello, I am currently attempting to use the seL4 Benchmark tool. After going through the menuconfig (kernel -> build options -> Enable Benchmarks -> Track threads and kernel utilization time), I attempt to rebuild, and get a host of errors: In file included from /home/chrisguikema/gdbtest/kernel/include/compound_types.h:16:0, from /home/chrisguikema/gdbtest/kernel/include/types.h:15, from /home/chrisguikema/gdbtest/kernel/src/api/faults.c:14: /home/chrisguikema/gdbtest/kernel/include/object/structures.h:249:5: error: unknown type name 'benchmark_util_t' benchmark_util_t benchmark; And a lot more, but all along the "not a structure or union" line, which makes me think that either the header file isn't being linked properly, or the #ifdefs aren't working for everything. Did I do something improperly in my setup? Thanks, Chris Guikema

2 1

Workshop debrief?
by Jeff Waugh 10 Jan '17

10 Jan '17

Hey there, I might be hoping a little too much for video, but will there be slides and notes from the Workshop? (Particularly interested in the gaps discussion.) Would be handy content on the wiki. :-) Thanks, Jeff

3 4

config-independent object type numbers
by Corey Richardson 10 Jan '17

10 Jan '17

Right now, object type numbers vary based on the kernel config (eg, CONFIG_VTX) etc. This is a huge source of pain for the Rust userspace libraries which don't integrate with seL4's build system. Is it possible for those enums to explicitly label every potential object type for a given architecture with a fixed number? -- cmr http://octayn.net/ +16038524272

2 2

seL4 as Xen guest / AWS
by Tony Arcieri 10 Jan '17

10 Jan '17

Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance. I was curious about the possibility of using seL4 as the host OS for a "unikernel"-like deployment of a Rust application split into a small set of services living in different capability spaces (e.g. network, key storage / crypto) -- Tony Arcieri

3 3

sel4test 4.0.x.xml broken?
by Corey Richardson 09 Jan '17

09 Jan '17

It seems that the line <project name="seL4.git" path="kernel" revision="4.0.x-compatible"/> should be <project name="seL4.git" path="kernel" revision="4.0.0"/> Either that, or a tag is missing from the kernel repo. -- cmr http://octayn.net/ +16038524272

2 1

questions about the vgic maintenance for sel4 TK1 ARM VMM
by PX 09 Jan '17

09 Jan '17

Hi, all I have questions about the vgic maintenance for sel4 tk1 ARM VMM. When the VM acknowledges an IRQ, an exception is raised and is delivered to the VMM. Could someone explain how seL4 intercepts the VM ack? How is this exception is raised ? I am confused because the VM is supposed to totally control the MMIO of the device and can write any thing to the device. How can seL4 be triggered in this case? Which part of source code allows seL4 to intercept the VM ack? Thanks Peng

2 1

Interest in 32-bit x86 Rust userspace?
by Corey Richardson 07 Jan '17

07 Jan '17

Is anyone interested at all in the 32-bit x86 Rust userspace libraries? I'm considering dropping support for them, as I don't personally plan to have any support for them in Robigalia, instead focusing on x86_64. Note that this wouldn't impact any Rust CAmkES components using the support in the sel4 buildsystem, just the sel4-sys, rust-sel4, etc crates. -- cmr http://octayn.net/ +16038524272

1 0

DMA driver in VM
by PX 07 Jan '17

07 Jan '17

Hi, I have a generic question about DMA driver in the VM on sel4. How does the device driver in the vm put physical address in the DMA controller given that there is no emulation in sel4? I worked on TK1 sel4 hypervisor extention version, but cannot find any address translation from vmm. Thanks Peng

1 0

pic/no-pic and some other questions
by Vasily A. Sartakov 06 Jan '17

06 Jan '17

Greetings. I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fact, most of the current problems are related to toolchains: 1. The first problem is a position independent code. Could you please describe me seL4' vision about it? muclibs is building with -fPIC, but everything else doesn't, right? I have a very tricky set of GCC’ flags, related to MIPS’ GOT, small data, abicalls, pic/non-pic, etc, and many of them are not working together. 2. MIPS assembler has several features, one of them is that the -O0 code requires having an addition space above the top of the stack for 4 registers: > 43b610: 27bdffe8 addiu sp,sp,-24 <— start of the function > 43b614: afbf0014 sw ra,20(sp) > 43b618: afbe0010 sw s8,16(sp) > 43b61c: afb0000c sw s0,12(sp) > 43b620: 03a0f021 move s8,sp <— frame stack > 43b624: afc40018 sw a0,24(s8) <— save 1st arg for a subroutine call > 43b628: afc5001c sw a1,28(s8) <— save 2nd arg for the subroutine > 43b62c: afc60020 sw a2,32(s8) <— save 3rd arg for the subroutine So, each time when I am allocating new stack I should return not top of the stack, but top_of_the_stack - 4*sizeof(seL4_Word). As result, sel4utils_configure_thread_config becomes platform specific. Could you please consider a possibility to put it into the «arch» as sel4utils_arch_init_context, or add something like «sel4utils_arch_configure». Also, it is important: this is an issue only for -O0 code, as far I see, -O2 uses different methods for arguments passing. I am trying to build toolchains which do not use frame pointer this style for -O0 code, but I am not sure about the result. 3. I really like how you redesigned declaration syscalls. Now I have a freedom to modify syscalls and do not care about the mainline declarations because now there are syscall wrappers. However, my toolchain generates very poor code for CONFIG_LIB_SEL4_PUBLIC_SYMBOLS and «DEFAULT» — I have proper working code only for CONFIG_LIB_SEL4_INLINE_INVOCATIONS. What is the conceptual difference of these declaration attributes, what they affect? 4. Could you please tell me what was the C equivalent of this asm code: .global __syscall .type __syscall,%function __syscall: sub sp, sp, #4 push {r5,r6} adr r5, 1f ldr r6, 1f ldr r5, [r5,r6] str r5, [sp, #8] pop {r5, r6} pop {pc} .hidden __sysinfo 1: .word __sysinfo-1b something similar to __syscall6 from libmuslc/arch/<arch>_sel4/syscall_arch.h, right? Thank you. P/s Happy new year/merry xmass/happy holidays! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

xsave region size for haswell/broadwell?
by Corey Richardson 06 Jan '17

06 Jan '17

Does anyone have a "maximal" xsave region size big enough for all the xsave-supporting features seL4 enables on Broadwell or Haswell? I don't have access to a machine with these features, so I can't run a program to get them with cpuid. -- cmr http://octayn.net/ +16038524272

2 1

questions about the address translation for a DMA driver in the ARM VM
by PX 05 Jan '17

05 Jan '17

Hi, all Happy new year! I have some urgent questions about address translation for a DMA driver in the ARM seL4-based VM. Your quick response is highly appreciated! 1. In the ARM sel4-based VM, the MMIO of a device is directly exposed to the device driver in the VM. When the DMA device driver allocates a DMA buffer to a device controller, the device driver can directly tell the real controller the IPA of the buffer starting address, instead of the real physical address. In other words, the device controller can only get the IPA of the buffer starting address. How can this device controller perform DMA without knowing the real PA of the buffer? Does seL4 perform some emulation here? How? 2. A closely related question to 1: when we develop a DMA driver in the VMM space, we put the real physical address of the device descriptor and real physical address of the DMA buffer in the controller registers through its MMIO. We found that the controller cannot find the correct place for the descriptor and the buffer. Do the seL4 hypervisor perform the address translation? If so, which source code does that? Thanks Peng

2 3

Build Error
by Daniel Romero 05 Jan '17

05 Jan '17

Hi, I am currently on a BeagleBone running Ubuntu 14.04 using gcc-arm-none-eabi. However I am getting the following error running 'make' after 'make menuconfig'. I am wondering if someone can guide me in the right direction [libs/libsel4] building... [GEN] include/sel4/types_gen.h Traceback (most recent call last): File "/home/ubuntu/seL4test/libs/libsel4/tools/bitfield_gen.py", line 26, in <module> from six.moves import range ImportError: No module named six.moves make[1]: *** [include/sel4/types_gen.h] Error 1 make: *** [libsel4] Error 2 Thank you, Hector Daniel Romero hdromero93(a)gmail.com

2 1

seL4test on Odroid-XU4
by Yevgeny Lavrov 05 Jan '17

05 Jan '17

Hello I ran into the following issue while running seL4test suite on Odroid-XU4: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 there are pending interrupts 0x00000001 reading sel4test-driver-image-arm-exynos5 3149364 bytes read Exynos5422 # bootelf 0x48000000 ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4130441f] ELF-loading image 'kernel' paddr=[60000000..60037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[60038000..60411fff] vaddr=[10000..3e9fff] virt_entry=1e74c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info .... 1 untypeds of size 10 1 untypeds of size 11 126 untypeds of size 12 2 untypeds of size 13 3 untypeds of size 14 3 untypeds of size 15 5 untypeds of size 16 3 untypeds of size 17 3 untypeds of size 18 3 untypeds of size 19 3 untypeds of size 20 2 untypeds of size 21 2 untypeds of size 22 1 untypeds of size 23 2 untypeds of size 24 2 untypeds of size 25 2 untypeds of size 26 2 untypeds of size 27 1 untypeds of size 29 Switching to a safer, bigger stack... seL4 Test ========= _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 31 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 2147483648, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 30 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 1073741824, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 29 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 536870912, error 1 ..... _utspace_split_alloc@split.c:247 Failed to find any untyped capable of creating an object at address 0x12dd0000 vka_alloc_object_at@object.h:64 Failed to allocate object of size 4096 at paddr 0x12dd0000, error 1 init_timer_caps@main.c:348 [Cond failed: error] Failed to get untyped at paddr 0x12dd0000 for timer Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill HYP mode is enabled, and seL4test suite is compiled in Debug Mode. Prior to running seL4test, I ran code from seL4 tutorials and those ran w/o any problems. Any suggestions on what I might have done wrong? Thanks

3 4

Exposing TSD on x86
by Corey Richardson 03 Jan '17

03 Jan '17

How do people feel about exposing the TSD (time-stamp disable) bit as a piece of state on the TCB? Ideally it'd be lazily switched. I vaguely want this in Robigalia for disabling access to real time in non-sufficiently-privileged processes. Best, -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Workshop debrief?
by Corey Richardson 20 Dec '16

20 Dec '16

I really ought to stop using my phone for email. Sent back to list. On Mon, Dec 19, 2016, at 05:25, Jeff Waugh wrote: > On Mon, Dec 19, 2016 at 8:19 PM, Corey Richardson > <corey(a)octayn.net> wrote: > > > I'm writing up my notes and will be publishing them on the > > Robigalia blog. > > Will send a link here when it's up. Ihor said he'd be collecting > > slides, > > not sure what the availability of those will be. > > > > Cool -- maybe let the list know too? -- cmr http://octayn.net/

1 0

RELEASE: Announcing CAmkES 2.3.0
by Stephen.Sherratt＠data61.csiro.au 15 Dec '16

15 Dec '16

Announcing the release of CAmkES 2.3.0 Changes in this release: * support for seL4 4.0.0 * new dependency: Haskell Stack (http://haskellstack.org) + Haskell Stack is a haskell version and package manager. It takes care of installing an appropriate version of ghc and cabal for building the capDL translator - part of CAmkES' build system. Check out an example CAmkES system with: repo init -u https://github.com/seL4/camkes-manifest.git -m default-2.3.x.xml repo sync For more information about CAmkES, see: https://wiki.sel4.systems/CAmkES Cheers, Stephen

1 0

ARM bootloaders that matter
by Jeff Waugh 14 Dec '16

14 Dec '16

Hi all, Out of interest, are there any ARM targets the seL4 development team / community care about that do not boot via u-boot or UEFI (whatever the implementation, be it u-boot, vendor-supplied, etc)? Thanks, Jeff

4 5

RELEASE: Announcing seL4 4.0.0
by Parthasarathi.Susarlaajay＠data61.csiro.au 13 Dec '16

13 Dec '16

We are pleased to announce the release of 4.0.0 of seL4. Listed below are a few of the key changes in this release: * Reorder bootinfo structure. * Add missing seL4_AllRights macro in libsel4. * Disallow kernel from using a device frame as an IPC buffer. * Syscall docs in manual now generated by doxygen. * Changes to make verification easier. * Various documentation fixes. * Benchmarks refactoring. * Coding style fixes. * Support for TLB and Cache management. * Preemptible backwards memzero for Retype. * Support for TCB operations in X86 multicore. * Support for raspberry-pi 3. ARM specific changes: * ARM Hyp refactoring. * Update VCPU fault definitions. * Add userspace invocations for hardware debugging. * Enable PMU export for V8. * Support ARM MPCore registers * Fix config dependency for 'IPC Buffer location'. * Use new cap rights structures in iospace. * Move initial setting of TPIDRURW register. * Add seL4_BenchmarkFlushCaches() for arm and ia32. * Support for prefetcher on Cortex-A9. * Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C. * am335x: Prevent out of bounds array access. * TK1 + Remove temporary SMMU memory mapping support. + Correct SMMU PD and PT indexing. + Split the mux controller from the misc region. * OMAP: + Fix issues with OMAP IRQ Code. X86 specific changes: * Add userspace invocations for hardware debugging. * Avoid writing the fs/gs base unless necessary. * Explicitly declare adress of .phys.bss. * Add BSS regions for BOOT and PHYS code. * Write FS and GS base when restoring user context. * Initialize store area when using XSAVE variant instructions. * Efficiently pack objects for fastpath. * Increase IPI words to 3. * Support for x2APIC. * Support larger XSAVE region sizes. * Change ia32 to use fs register for IPC buffer. * Update the bootinfo for number of cores. * Initial support for SMP vt-x. * Split CPU ID management into mode and general. * Fix cpuid family/model composition. * Add X86_64 support. Please note that this release is not source compatible with earlier releases of seL4, please read https://research.csiro.au/tsblog/introduc ing-device-untyped-memory-sel4/ for more information regarding the changes. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/4.0.0.tar.gz [259d9eadaddef579c2b98b91cf40d13a 4.0.0.tar.gz] The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf Contributors: * Adrian Danis * Alexander Boettcher * Amirreza Zarrabi * Anna Lyons * Christian Helmuth * Corey Richardson * Donny Yang * Hesham Almatary * Jeff Waugh * Joel Beeren * Kent McLeod * Kofi Doku Atuah * Matthew Brecknell * Matthew Fernandez * Matt Rice * Rafal Kolanski * Stephen Sherratt * Thomas Sewell * Xin,Gao Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Partha Susarla Kernel engineer DATA61 | CSIRO E parthasarathi.susarla(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

seL4 on Zinq7000 on QEMU
by Andrew Gacek 09 Dec '16

09 Dec '16

I'm trying to build and emulate a version of seL4 for the zinq7000 platform, but it crashes immediately. I've started by taking the camkes tutorial and building it for zinq7000: repo init -u https://github.com/seL4/camkes-manifest.git repo sync make arm_simple_defconfig make menuconfig # change seL4 platform to zinq7000 make When I try to emulate it, it crashes right away: qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel images/capdl-loader-experimental-image-arm-zynq7000 qemu: fatal: Trying to execute code outside RAM or ROM at 0x10000000 R00=00000000 R01=00000000 R02=00000000 R03=00000000 R04=00000000 R05=00000000 R06=00000000 R07=00000000 R08=00000000 R09=00000000 R10=00000000 R11=00000000 R12=00000000 R13=00000000 R14=00000000 R15=10000000 PSR=400001d3 -Z-- A svc32 s00=00000000 s01=00000000 d00=0000000000000000 s02=00000000 s03=00000000 d01=0000000000000000 s04=00000000 s05=00000000 d02=0000000000000000 s06=00000000 s07=00000000 d03=0000000000000000 s08=00000000 s09=00000000 d04=0000000000000000 s10=00000000 s11=00000000 d05=0000000000000000 s12=00000000 s13=00000000 d06=0000000000000000 s14=00000000 s15=00000000 d07=0000000000000000 s16=00000000 s17=00000000 d08=0000000000000000 s18=00000000 s19=00000000 d09=0000000000000000 s20=00000000 s21=00000000 d10=0000000000000000 s22=00000000 s23=00000000 d11=0000000000000000 s24=00000000 s25=00000000 d12=0000000000000000 s26=00000000 s27=00000000 d13=0000000000000000 s28=00000000 s29=00000000 d14=0000000000000000 s30=00000000 s31=00000000 d15=0000000000000000 s32=00000000 s33=00000000 d16=0000000000000000 s34=00000000 s35=00000000 d17=0000000000000000 s36=00000000 s37=00000000 d18=0000000000000000 s38=00000000 s39=00000000 d19=0000000000000000 s40=00000000 s41=00000000 d20=0000000000000000 s42=00000000 s43=00000000 d21=0000000000000000 s44=00000000 s45=00000000 d22=0000000000000000 s46=00000000 s47=00000000 d23=0000000000000000 s48=00000000 s49=00000000 d24=0000000000000000 s50=00000000 s51=00000000 d25=0000000000000000 s52=00000000 s53=00000000 d26=0000000000000000 s54=00000000 s55=00000000 d27=0000000000000000 s56=00000000 s57=00000000 d28=0000000000000000 s58=00000000 s59=00000000 d29=0000000000000000 s60=00000000 s61=00000000 d30=0000000000000000 s62=00000000 s63=00000000 d31=0000000000000000 FPSCR: 00000000 Aborted Is there something I'm doing wrong? Thanks, Andrew

2 9

Virtio on camkes-vm
by Robert VanVossen 08 Dec '16

08 Dec '16

Hello, We are looking to add another virtio device to camkes-vm for guests to use. I have been looking through the code at how virtio_net works and I have a pretty decent understanding of how it is configured and used. I have a few design/philosophical questions though. 1. Was any of this (libethdriver, libpci, Ethdriver component, virtio_net.c, virtio_emul.c) ported from somewhere else, or was it all written from scratch? 2. Why is components/Init/src/virtio_net.c used in conjunction with vm0_config.init_cons instead of just using the VMNet templates? 3. Looks like pci handling was decoupled from drivers like libethdriver and it is left up to the VM Init component to configure PCI. What is the reason for that? 4. Virtio_emul.c appears to be the layer that actually provides the virtio interface to the VM. Would it make more sense to make this more generic to cover more devices, or should new emulation files be created for each device? Thanks, Robbie VanVossen

2 1

Huge kernel images no more
by Jeff Waugh 06 Dec '16

06 Dec '16

Hurrah, I was curious about the huge kernel images, and had it on my list to poke at. Adrian's changes merged last night sorted it: x86: Explicitly declare adress of .phys.bss x86: Add BSS regions for BOOT and PHYS code Simulation debug x86_64 image is down from 7.1M to 1.1M. That's more like it! Nice! :-) Thanks, Jeff

2 1

Bitcoin on seL4?
by Carl Dong 02 Dec '16

02 Dec '16

Hi all, I recently acquired a BD-SL-I.MX6 and will be tinkering with it to install seL4. A major use case for me is if I could run [bitcoind](https://en.bitcoin.it/wiki/Bitcoind) or at least [vanitygen](https://en.bitcoin.it/wiki/Vanitygen) on seL4. I'm very new to the system, but is there a relatively easy way of cross-compiling said software for seL4? Would love to spend some time learning. Cheers, Carl Dong accounts(a)carldong.me

4 3

seL4 Memory Management
by Mark Reus 01 Dec '16

01 Dec '16

Hi I have been going through some of the research papers about seL4. I wanted to understand the security features in the memory management. I am a little confused, hope someone can I help me. Quote from the paper "Finally, the kernel ensures that each physical frame mapped by the MMU at a useraccessible address is of the Frame object type. These Frame objects contain no kernel data and since they cannot overlap with other typed objects, direct user access to kernel data is not possible" I understand that seL4 promotes isolation between processes and no allocation is done by the kernel itself rather it is done by user level manager. Since we use untyped memory and we retype them, there is no overlap of objects. The user level resource managers can access both the kernel memory and other memory as well because they have capabilities to both. What exactly in the above quote causes the isolation of user level memory with kernel memory. I am of the notion that the kernel allocated objects are still accessible and can be modified to point to some other memory? Am I misunderstanding something? Regards Mark

4 4

Good C, bad C, verifiable C
by Jeff Waugh 30 Nov '16

30 Nov '16

Howdy, Is there a guide to the dos and don'ts of C according to the seL4 verification process? I kinda remember reading a quick summary somewhere, but can't find it on the wiki. Maybe I read it in one of the papers? I certainly remember reading the moral equivalent of "lol no strings". ;-) Thanks, Jeff

2 1

contiguous physical memory allocation for seL4
by PX 30 Nov '16

30 Nov '16

Hi, all I want to allocate a contiguous physical memory block (larger than a physical page) and map it to contiguous virtual addresses in the vspace, what's the best way to do it? Are there existing libraries allowing me to do that? thanks Peng

3 2

First International seL4 Workshop
by Gernot.Heiser＠data61.csiro.au 29 Nov '16

29 Nov '16

Hey seL4 community! We’d like to invite you to participate in the inaugural seL4 Workshop. Given the growth in the community we are starting an annual seL4 workshop where we can come together to share and learn what is being done with seL4. Unlike the previous developers days, the focus is much more on what is happening with seL4 and what interesting things are being done using seL4 rather than a learning or tutorial event. We’d like participants to join and: - present what they are doing with seL4 - demonstrate seL4-based projects - give tutorials on aspects of seL4 or tools, libraries, environments for working with seL4 - show results or progress of verification work involving seL4 - discuss interesting challenges (and possible solutions) they’ve encountered when using seL4 - discuss visions for the future of seL4 and high-assurance systems This workshop will take place on Thursday December 15, 2016 (and may be extended to December 16th if there is enough demand) in Malibu, CA, USA. Note that you are welcome to attend even if you do not present anything. Please register participation at: https://sel4.systems/Community/Devdays/ Participation is free, and we may be able to provide students with financial assistance for travel. This workshop is sponsored by the Center for Secure and Resilient Systems at HRL Laboratories, LLC, and by Data61. Gernot for the Data61 Trustworthy Systems Team

2 1

Re: [seL4] Timer for Performance Measurement
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

?Hey Andrew, Sorry I took so long to get back to you: we have a benchmarking suite, seL4Bench (https://github.com/seL4/sel4bench/blob/master/apps/ipc/src/main.c) which should have userspace timers and precise timestamps available for most platforms. As I understand, you will just have to write a new microbenchmark of your own, and import your library, and then insert calls to the relevant timestamp counter functions (https://wiki.sel4.systems/Benchmarking%20guide)? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Andrew Mine <secondmine(a)gmail.com> Sent: 04 November 2016 16:30 To: devel(a)sel4.systems Subject: [seL4] Timer for Performance Measurement Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

Re: [seL4] how to get timing information on seL4 user space
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

??Hi Peng, Well, an atomic counter would suffice, and if you need to secure the counter, you could wrap it around with a server. You either need a hardware upcounter, or else a periodic event-timer that you can use to emulate a hardware upcounter; from there, you just use your upcounter for your jiffies. Libplatsupport has userspace timer drivers for most platforms we support: https://github.com/seL4/util_libs/tree/master/libplatsupport? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: 29 November 2016 08:27 To: devel(a)sel4.systems Subject: [seL4] how to get timing information on seL4 user space Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

how to get timing information on seL4 user space
by PX 29 Nov '16

29 Nov '16

Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

IPC measurements
by Neelesh Vemula 28 Nov '16

28 Nov '16

Hi I have been measuring the performance of my application and doing some comparisons with other kernels. I had a couple of queries. I am running seL4 on zynq device. I am using the given timer driver in libplatsupport to measure the clock cycles. Queries: 1) I have found the sample benchmark numbers for seL4 IPC from http://l4hq.org/docs/performance.php. Since I am running on Armv7 Cortex A9 , the time for one half way trip is 316 ns. Is this measured from system call to system call or from process to process? 2) I am trying to compare the performance on FreeRTOS and Linux, is there any such comparison on where seL4 stands? 3) Does the IPC time vary with the different api of ReplyRecv, Reply, seL4_NBRecv? I have this question because I am seeing that Reply is taking about twice the amount of clock cycles compared to Recv. In terms of my application, I am majorly looking at measuring one whole cycle which includes: 1) 1st Process sends message to 2nd Process 2) 2nd Process Reads from AXI device space 3) 2nd Process replies with Reply and waits for another command from 1st process 4) 1st process sends another message to 2nd Process 5) 2nd Process writes to the hardware 6) Time from step 1 to step 5 is measured. Results for this on seL4 : 3180 clock cycles FreeRTOS: 2414 clock cycles I am sure there is possibility of unnecessary overheads involved in my measurement, but I expected seL4 to be faster. Can someone help me in this regard. Regards Neelesh Vemula

2 1

Reading executable of the first process in kernel
by Norrathep Rattanavipanon 22 Nov '16

22 Nov '16

Hi, I want to modify the sel4 kernel to compute a checksum over the executable of the first process before executing it. The goal is to ensure that we execute the correct first process. What I'm doing right now is modify try_init_kernel() in kernel/src/archarm/kernel/boot.c by adding the following lines: for(i=ui_p_reg_start, i<ui_p_reg_end; i++) { checksum += *((char*) (i)); } My questions are the following: (1) Is this a right place to perform the checksum (inside try_init_kernel())? I assume in this function, seL4 kernel already takes over and thus this should do the job. (2) Based on my understanding, what I did was computing the checksum over the entire image (which may includes executable of other processes as well). Is there a way to just read the executable of the first process and ignore the rest in seL4 kernel? (3) I'm also curious: where/when does the seL4 kernel start the root process? I see the end of the same file (boot.c) that it just calls try_init_kernel() but does not load the root process. Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

Memory Management
by Mark Reus 22 Nov '16

22 Nov '16

Hi I have a general case about memory allocation in particular with that of the Vspace. I have been reading some documents and trying to compare how it is in Linux Kernel. Any program Virtual memory in a Linux kernel is as shown in picture below where all processes have 1GB of virtual memory which is mapped to kernel space for faster context switches and system calls. _____________________ | Kernel Space (1GB) | |_____________________| | | | User Mode Space | | (3 GB) | | | |_____________________| I have come across this this link http://os.inf.tu-dresden.de/pipermail/l4-hackers/2014/006262.html detailing a little about the sel4 memory management. But I haven't been able to completely comprehend it . I wanted to know if the seL4 kernel also has a similar mapping of kernel space. Regards Mark

2 1

Syscall errors with musl
by Rinat Dobrokhotov 21 Nov '16

21 Nov '16

Hi all, I have written simple programme which gets system time. I get syscall errors when programm is calling gettimeofday function: *main.c:* #include <time.h> #include <sys/time.h> #include <stdlib.h> #include <stdio.h> int main(int argc, char *argv[]) { int iterations = 1000000; struct timeval start, end; gettimeofday(&start, NULL); for (int i = 0; i < iterations; i++) { } gettimeofday(&end, NULL); printf("%ld\n", ((end.tv_sec * 1000000 + end.tv_usec) - (start.tv_sec * 1000000 + start.tv_usec))); return 0; *Errors:* libsel4muslcsys: Error attempting syscall 263 libsel4muslcsys: Error attempting syscall 78 Could you tell me where I mistook? -- Best regards, Rinat Dobrokhotov

2 1

seL4RPC vs seL4RPCCall?
by Andrew Gacek 18 Nov '16

18 Nov '16

What's the difference between seL4RPC and seL4RPCCall in CAmkES? Is there documentation on the various connectors somewhere? Thanks, Andrew

2 1

Send input to seL4 in QEMU
by Andrew Gacek 18 Nov '16

18 Nov '16

Hi, We are developing an seL4 application that will process UDP packets coming in over a network connection. Eventually, we'll be running this on real hardware with real drivers, but for now we are using QEMU. We have a python script that can generate packet payloads. Is there a way to send this information into QEMU so that we can develop our seL4 application without having the drivers and hardware in place? If it matters, we are using CAmkES as well. Thanks, Andrew

2 3

seL4 Kernel Profiler
by Chris Guikema 18 Nov '16

18 Nov '16

Hello, I am working on a Code Profiler for use in seL4 Systems. I see that the Kernel already has some form of profiling/benchmarking functionality built in. However, I do not see anything in the documentation that covers how this is used. Is there a guide that I can follow to get the kernel profile functional? Thanks Chris Guikema

2 1

Will seL4_Word ever be anything but uintptr_t?
by Corey Richardson 17 Nov '16

17 Nov '16

I guess this is a somewhat philosophical question. It's come up a bit in the Rust libs I've been writing. Casting from pointer-sized things to *specifically* u32/u64 is bit tiresome for the places where I can't abstract over that. -- cmr http://octayn.net/ +16038524272

2 1

seL4 on i.MX53
by Yevgeny Lavrov 15 Nov '16

15 Nov '16

Hello. I've multiple ARM devices at my disposal that I want to use to experiment with seL4, one of them is USB Armory (Architecture: ARMv7 Cortex-A8 Processor: i.MX53 800MHz). Before I get into it, I would like to know if seL4 supports this ARM device. Thanks

2 1

Unable To Map Physical Frame
by Mark Reus 13 Nov '16

13 Nov '16

Hi I want to map the arm global timer which is located at memory location 0xF8F00200 . However, when I am trying to get the physical frame using : error = simple_get_frame_cap(&simple, (void*)global_timer_paddr, 12, &ep_cap_path); if (error) { ZF_LOGE("Failed to find frame at paddr %p\n", global_timer_paddr); return error; } I get the Error Statement on stduout as "main@main.c:209 Failed to find frame at paddr 0xf8f00200" If i print the bootinfo during bootup, I can see that I have access to this region 0xf8000000 | 00000012 | [520 <--> 521 ] Can someone help me as why this issue may be caused? I know that this global timer is said to be mapped in the private region. But I do not what exactly that means and if we cannot do it. Regards Mark

2 1

malloc and SCHED0004
by Vasily A. Sartakov 05 Nov '16

05 Nov '16

Greetings. I am keep working, and now I would like to discuss my second memory-related issue. In contrast with first one, the second issue happens only in SCHED004 test, in malloc function: helper_thread_t **threads = (helper_thread_t **) malloc(sizeof(helper_thread_t*) * NUM_PRIOS); malloc dies because there is no record inside TLB. someone tries to write something to an address, for example, 0x54f1c8. This address is important because it is located outside of the virtual memory allocated for the test. Previous, elf_loader allocates a region and the region ends exactly on 0x54efff. I have experimented with different setups, added some debug functions, and each time I saw the same picture: malloc dies because tries to write to next page outside the allocated region. I know what is the function tries to write. It is a pretrim, part of libmuslc: static int pretrim(struct chunk *self, size_t n, int i, int j) { size_t n1; struct chunk *next, *split; /* We cannot pretrim if it would require re-binning. */ if (j < 40) return 0; if (j < i+3) { if (j != 63) return 0; n1 = CHUNK_SIZE(self); if (n1-n <= MMAP_THRESHOLD) return 0; } else { n1 = CHUNK_SIZE(self); } if (bin_index(n1-n) != j) return 0; next = NEXT_CHUNK(self); printf("next - %x, n1 = %x\n", next, n1); split = (void *)((char *)self + n); <————— the split points outside the allocated region split->prev = self->prev; <————— here we die split->next = self->next; split->prev->next = split; split->next->prev = split; split->psize = n | C_INUSE; split->csize = n1-n; next->psize = n1-n; self->csize = n | C_INUSE; return 1; } As a previous, I would like to ask, should I keep in mind something platform specific? maybe you have modified, like a_and asm functions or something else in libmuslc? Also, malloc itself raises questions: void *malloc(size_t n) { struct chunk *c; int i, j; if (adjust_size(&n) < 0) return 0; <….> i = bin_index_up(n); for (;;) { uint64_t mask = mal.binmap & -(1ULL<<i); mal.binmap is used uninitialised. also, when we set up bits inside it? Moreover, I have different values on ARM (0x80000000000) and MIPS (0x8000000000000000), I am not sure that it is ok Thank you! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 6

Timer for Performance Measurement
by Andrew Mine 04 Nov '16

04 Nov '16

Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

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

timers in seL4
by Horace Blanc 24 Oct '16

24 Oct '16

Hi, I am trying to understand the timer design of both seL4 as a kernel and as a hypervisor on ARM architecture. I understand that in both cases, seL4 uses a timer in order to preempt its threads. This means that seL4 must keep the control over that timer and cannot let threads use it directly. I also understand that seL4 does not provide any timer API to its threads. It seems then that the intended use is to implement a timer driver in userland in order for other application to access timing functions. But this timer driver cannot access the same timer as seL4. Does this mean that at least two physical timers (or at least two physical timer interfaces) are necessary? ARM virtualization extensions offers a virtual timer to be used by VMs and which is implemented with an offset register. They also offer different timers (one for an hypervisor, one for kernel/application and one for the virtual timer). It seems that the current seL4 as a hypervisor project does not use these extenstions. Do they? If not why? Thank you for your answers

1 0

Freelance
by Marco Reus 22 Oct '16

22 Oct '16

Hi I apologize if this is not the right platform to reach people. But I am looking for a freelancer who has some expereince in working with seL4 kernel. I need some aid in implementation of a project. Regards Vicky

1 0

Larger badges on 64-bit?
by Corey Richardson 21 Oct '16

21 Oct '16

Is there a future in which we recover the extra 32+ bits of padding on 64-bit systems for use in badges? In Robigalia, 28 bit badges are extremely limiting for what we want to use them for. -- cmr http://octayn.net/

2 1

CAmkES Groups
by Robert VanVossen 19 Oct '16

19 Oct '16

Hello, I have been trying to get groups with CAmkES 2.2 working, but it doesn't look like it will build correctly. At first, when I place components in a group, I get that there is an unresolved reference to one of the components during compilation. I was able to get past this by moving the function assign_address_spaces in camkes/camkes/runner/Transforms.py from POST_RESOLUTION to PRE_RESOLUTION, but after that I still ran into some issues: [LD] MyGroup_group_bin if [ 2 -eq 1 ]; then cp "comp1.instance-copy.bin" " MyGroup_group_bin"; else /usr/bin/ccache arm-xilinx-eabi-gcc comp1.instance-copy.bin comp2.instance-copy.bin -Wl,--build-id=none -L<stage_dir>/lib -Wall -nostdinc -std=gnu11 -O2 -D_XOPEN_SOURCE=700 -marm -Wtrampolines -mcpu=cortex-a9 -g -Wno-main -fno-stack-protector -Wl,--start-group -lsel4 -lsel4debug -lc -lsel4muslccamkes -lsel4camkes -lsel4sync -lutils -lsel4vka -lsel4utils -lsel4platsupport -lplatsupport -lsel4vspace -lgcc -Wl,--end-group -static -nostdlib -u _camkes_start -e _camkes_start -o MyGroup_group_bin; fi <stage_dir>/lib/libsel4camkes.a(crt0.o): In function `_camkes_start': (.text+0x6c): undefined reference to `_start' Any insight on this? Are groups supported yet? Thanks, Robbie VanVossen

2 1

SDHC driver in Sabre Lite
by Norrathep Rattanavipanon 19 Oct '16

19 Oct '16

Is there any example on how to use sdhc driver in ( https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)? Currently, I'm struggling to read a block of data from micro-sd in seL4. I use the following code (assertions are omitted here for readability) to instantiate the driver : ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); ps_dma_man_t dma_man = {0}; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); ps_io_ops_t io_ops = { .io_mapper = io_mapper, .dma_manager = dma_man }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev,0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); error = sdio_init(id, &io_ops, dev); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); void* vaddr = (void*) 0x1980000; uintptr_t paddr = (uintptr_t) 0x119a7000; long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL, NULL); And the code's stuck in mmc_block_read function where interrupt status (BRR and BWR) are never on. Thanks in advance, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 5

Missing untypeds on x86?
by Jeff Waugh 19 Oct '16

19 Oct '16

Hi all, Using x86 master on qemu with 2G memory, the kernel's map looks good: Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fee0000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from 7ffe0000 size 20000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 But the largest physical address of non-device untyped I get from bootinfo is 0x1faf9000. Same at 1G to 3G, though it does the right thing at 128M. On the other hand, x86_64 looks fine with 0x7ffc0000, and adapts to more. btw, very exciting to see x86_64 code land! Working well so far. Thanks, Jeff

2 1

question about adding device to ARM VM linux
by PX 18 Oct '16

18 Oct '16

Hi, all I have a question about adding a device to ARM VM linux. When a device is added to the vmlinux, two functions, map_device () and map_ram () are invoked. I don't understand the purpose of map_ram(). In map_device(), the capacity to the device is used to set up the mapping between a virtual address and the MMIO (of the device). Then, in the map_ram (), a capacity to the virtual address is allocated. I am confused because the virtual address is already mapped to the mmio of the device. why do we need to allocate a capacity for the virtual address? Should the capacity be the same as the one for the device? Thanks Peng

1 0

Benchmark results?
by Corey Richardson 18 Oct '16

18 Oct '16

Hello, Are there any public results from sel4bench, or should I get my own numbers for some hardware? -- cmr http://octayn.net/

2 1

adding code to the main.c for ARM VMM
by PX 18 Oct '16

18 Oct '16

Hi, I have posted this question before and my problem is not totally solved because I am not familiar with Makefile. I try to make my question more specific as follows. I want to add new code, which is already organized under a directory, say, test. I want to add the directory test to main.c file for ARM VMM, located at ~/projects/vm/apps/vm/components/VM/src/main.c. In the program, we want to refer to the sub-directories by relative path to the directory test. what is the easy to do that? How can we add the directory test to the search path so that we can include the header files by the relative path to the directory test, say include "test1/test1.h"? We tried to modify the makefile at ~projects/vm/apps/vm, but we have to add all the sub-directories, and there are problems for the files with the same name under different directories. thanks Peng

2 1

Re: [seL4] endpoint.c
by Vasily A. Sartakov 18 Oct '16

18 Oct '16

> we take address that causes syscall from the ksCurThread and set them back. Thus, FaultInstruction should point to something different, right? > I have add FaultInstruction in the same manner as it made in ARM platform: sub lr, lr, #4 /* Store FaultInstruction */ str lr, [sp, #(PT_FaultInstruction - PT_LR_svc)] I am tacking address of an instruction causes exception, subtract 4 from the value, and save it into the FauiltInstruction. Now get* and set* functions are: word_t PURE getRestartPC(tcb_t *thread) { return getRegister(thread, FaultInstruction); } void setNextPC(tcb_t *thread, word_t v) { setRegister(thread, CP0_EPC, v); } Also, Faultinstruction is part of frameRegisters and «linked» with cp0_epc of seL4_UserContext (sel4arch.xml) Now both tests are passed: Starting test 27: TEST_RECYCLE0001 TEST_RECYCLE0001 Running test RECYCLE0001 (Basic endpoint recycle testing.) <<seL4 [decodeInvocation/609 T0x8fee3f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #101.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #163.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #230.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #303.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #364.>> <<seL4 [decodeInvocation/609 T0x809db100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #428.>> <<seL4 [decodeInvocation/609 T0x809db300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #491.>> <<seL4 [decodeInvocation/609 T0x809db500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #564.>> <<seL4 [decodeInvocation/609 T0x809db700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #619.>> <<seL4 [decodeInvocation/609 T0x809db900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #694.>> <<seL4 [decodeInvocation/609 T0x809dbb00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #761.>> <<seL4 [decodeInvocation/609 T0x809dbd00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #828.>> <<seL4 [decodeInvocation/609 T0x809dbf00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #831.>> <<seL4 [decodeInvocation/609 T0x8fe29100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #898.>> <<seL4 [decodeInvocation/609 T0x8fe29300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #965.>> <<seL4 [decodeInvocation/609 T0x8fe29500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1032.>> <<seL4 [decodeInvocation/609 T0x8fe29700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1099.>> <<seL4 [decodeInvocation/609 T0x8fe29900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1170.>> <<seL4 [decodeInvocation/609 T0x8fe29b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1221.>> <<seL4 [decodeInvocation/609 T0x80a13100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1295.>> <<seL4 [decodeInvocation/609 T0x80a13300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1354.>> <<seL4 [decodeInvocation/609 T0x80a13500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1427.>> <<seL4 [decodeInvocation/609 T0x80a13700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1490.>> <<seL4 [decodeInvocation/609 T0x80a13900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1563.>> <<seL4 [decodeInvocation/609 T0x80a13b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1628.>> <<seL4 [decodeInvocation/609 T0x80a13d00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1635.>> <<seL4 [decodeInvocation/609 T0x80a13f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1698.>> <<seL4 [decodeInvocation/609 T0x80aa1100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1765.>> <<seL4 [decodeInvocation/609 T0x80aa1300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1828.>> <<seL4 [decodeInvocation/609 T0x80aa1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1897.>> <<seL4 [decodeInvocation/609 T0x80aa1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1966.>> <<seL4 [decodeInvocation/609 T0x80aa1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #2033.>> Test RECYCLE0001 passed Starting test 28: TEST_RECYCLE0002 TEST_RECYCLE0002 Running test RECYCLE0002 (Recycle deletes caps) <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #361.>> <<..> <<seL4 [decodeInvocation/609 T0x80a90700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2003.>> <<seL4 [decodeInvocation/609 T0x80a90900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2073.>> <<seL4 [decodeInvocation/609 T0x80a90b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2131.>> <<seL4 [decodeInvocation/609 T0x80a90f00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2203.>> Test RECYCLE0002 passed Can you please tell me something about the Faultinstruction context field, and, in general, what the assumptions about the behaviour of CPU you put into the design. For example, in MIPS, in a case of a trap, EPC points on instruction causes a trap, but in a case of an interrupt, PC and further EPC points on next instruction. Should I take this into the account somewhere in the kernel? > >> Hope that helps. >> >> Regards, >> Hesham >> ________________________________________ >> From: Devel <devel-bounces(a)sel4.systems> on behalf of Vasily A.Sartakov <sartakov(a)ksyslabs.org> >> Sent: Friday, October 14, 2016 12:33 AM >> To: devel(a)sel4.systems >> Subject: [seL4] endpoint.c >> >> Hello. >> >> I have a problem with endpoint.c test (RECYCLE0001): >> >> Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c >> >> I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look?

2 2

Fwd: Microkernels / Component-based OSes devroom - Call for Participation
by Vasily A. Sartakov 18 Oct '16

18 Oct '16

Just want to invite you to FOSDEM’17 > The developers of several free and open-source microkernel-based > operating systems will meet at FOSDEM 2017 [1] in Brussels, Belgium > and will share a developer room on Saturday of February 04, 2017 [2]. > The devroom is currently looking for content in the form of talks and > activities related to the area of microkernel-based operating systems. > Possible topics include, but are not limited to: > > * Introduction of a specific OS or framework > * Design of subsystems and the general architecture of an OS > * Enabling support for hardware (architectures, device drivers) > * Used languages and tools > * Maintainance and testing > * Security and robustness > * Trends and challenges > * Use cases, experiences, lessons learned and demos > > Please use the Pentabarf [3] system to submit your proposals and file it > under the track “Microkernels and Component-based OS”. You do not need > to create a new account if you already have one. When in doubt, please > use the devroom mailing list [4]. If you do not want to give a talk > yourself, you may still send suggestions for what else you would like to > see, or do in the devroom. Please send your suggestions to the mailing > list. The deadline for your proposal is on December the 4th. > > Make sure to include the following in your proposal: > > * Title of your talk (will be printed in the FOSDEM booklet) > * Your full name (will be printed in the FOSDEM booklet) > * A short abstract (one or two paragraphs) > * Duration of your talk (please, at least 25 and no longer than 45 min) > > The official devroom schedule (along with the accepted talks) will be > announced on December the 11th on the devroom's mailing list and the > speakers will be notified via e-mail. The schedule will also be published > on the FOSDEM website. > > > About FOSDEM > > FOSDEM is a two-day event organised by volunteers to promote the > widespread use of free and open source software. Taking place in the > beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the > best such conference in Europe. FOSDEM covers a wide spectrum of free > and open source software projects, and offers a platform for people to > collaborate. To this end, FOSDEM has set up developer rooms (devrooms) > with network/internet connectivity and projectors where teams can meet > and showcase their projects. Devrooms are a place for teams to discuss, > hack and publicly present latest directions, lightning talks, news and > discussions. Besides developer rooms, FOSDEM also offers main tracks, > lightning talks, certification exams and project stands. Every year, > FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. > Participation and attendance is totally free, though the organisers > gratefully accept donations and sponsorship. No registration necessary. > > > About the devroom > > Since the first Microkernel devroom in 2012 this devroom has been part of > each following FOSDEM. By now it has become a somewhat institutionalized > tradition for the micro kernel community to meet there; to this date over > a dozen projects have participated in one way or another. Each of the > projects face similar challenges but come up with partially differend > solutions. Therefore, the goal of the Microkernel devroom is to bring the > various projects together, let them exchange ideas, cross-pollinate and > socialize. > > > Social events > > It also has become a habit that the microkernel projects dine together > somewhere in downtown Brussels after the devroom closes. The year 2017 > will not be any different, so there is going to be a microkernel family > dinner on Saturday night. The exact location and time will be specified > later. Consult the FOSDEM web and other projects for additional social > events such as the famous FOSDEM-organized Friday Beer Event and the > FOSDEM-arranged free sightseeing tours for spouses. > > > Important dates recap > > * 04.12.2016: Deadline for submissions > * 11.12.2016: Schedule published and speakers notified of acceptance > * 04.02.2017: The devroom takes places > > > Links > > [1] http://fosdem.org/ > [2] https://fosdem.org/2017/practical/transportation/ > [3] https://fosdem.org/submit > [4] https://lists.fosdem.org/listinfo/microkernel-devroom -- Vasily A. Sartakov sartakov(a)ksyslabs.org

1 0

General Questions
by Mark Reus 17 Oct '16

17 Oct '16

Hi I have recently started with working on sel4 and I have a couple of questions. i) Can a process be spawned or configured only from the root task? (using sel4_configure_process) ii) How to enable or locate prints of ZF_LOGE in kernel? I have enabled kernel prints and debug in make menuconfig. iii) I have followed the tutorial for IPC between a spawned process and root task. The setup is done as follows from the root task: /* create an endpoint */ vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); assert(error == 0); /* * make a badged endpoint in the new process's cspace. This copy * will be used to send an IPC to the original cap */ /* make a cspacepath for the new endpoint cap */ cspacepath_t ep_cap_path; seL4_CPtr new_ep_cap; vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /* copy the endpont cap and add a badge to the new cap */ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path, seL4_AllRights, seL4_CapData_Badge_new(EP_BADGE)); assert(new_ep_cap != 0); However, I want to establish communication between two spawned processes. In that case I need to copy the badged endpoint capability of one process into another process. But in the spawned process I wouldn't have access to the pointer (sel4utils_process_t of new process), so how can i use mint_cap_to_process. Can someone help me with these. Thanks in advance. Regards Mark

3 2

endpoint.c
by Vasily A. Sartakov 14 Oct '16

14 Oct '16

Hello. I have a problem with endpoint.c test (RECYCLE0001): Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

sel4 hypervisor communication
by Horace Blanc 13 Oct '16

13 Oct '16

Hi, 1) Is there a mechanism for inter VM communication with seL4 as a hypervisor? 2) If the VMMs run in kernel mode (PL1), as I was told, does it mean they use hvc commands instead of swi/svc commands when sending messages to seL4 as hypervisor? Thank you in advance,

2 1

syscall.c
by Vasily A. Sartakov 11 Oct '16

11 Oct '16

Greetings. I have moved forward to tests in my our MIPS port. Some of them work fine, but not all. Now I have a question about syscall.c test. What exactly we test here? In ARM-based part I see initialisation of 12 registers, performing syscall with further checking that our initialised registers have original values. So, as far I understand, these registers should be modified in a syscall’s inline, thus, they should be allocated on the stack and reloaded after the end of syscall. Right? My issue here is that I have much many than 12 registers and my compiler chooses them randomly (for me). For example, sometimes it uses only S0-S7 with some T0-T9 registers, sometimes all T0-T9 with some S0-S7 registers. Moreover, I cannot put more than 30 asm instructions in one inline (gcc error), thus, maybe I should specify proper register name here. But for that, I should be sure that I understand this test correct. Can we help me? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

Spawn new process
by Andrew Mine 11 Oct '16

11 Oct '16

Hi I am working with sel4-tutorials and wanted to spawn a new process using int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *target_vka, vspace_t *spawner_vspace, sel4utils_process_config_t config); However, I am not able to understand some of the details required to initialize the parameter config used in the function. Can someone give me link to an example of sorts where this is used. Regards Andrew Mine

1 0

adding new code to VMM on TK1
by PX 11 Oct '16

11 Oct '16

Hi, Please forgive my ignorance. I want to add new code to the seL4-based VM for TK1. However, I find it is hard to add new directories. The newly added directories are always ignored or can not be found by compiler. What's the correct way to add new directories? which scripts we should look into? thanks Peng

3 4

questions about the device driver in virtual machine on ARM seL4 (TK1 board)
by PX 06 Oct '16

06 Oct '16

Hi, I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000. 1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio. 2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping. Do I miss something? Thanks Peng

2 4

Post-mutikernel approach to multiprocessor support?
by Jeff Waugh 04 Oct '16

04 Oct '16

Hi all, Is there anything that can be shared so far about seL4's post-multikernel approach to multiprocessor support? (I couldn't see anything new or upcoming on the publications pages, and figured a paper or two might land before code aimed for Q4'16.) Thanks, Jeff

2 5

Possible seL4 developer day Dec 15–16 in Malibu
by Gernot.Heiser＠data61.csiro.au 04 Oct '16

04 Oct '16

Dear seL4 Community, Part of the Data61 seL4 Team will be in Malibu in mid December and we are considering running another Developer Day. As in the past, this would actually run over 1.5 days, from the morning of the 15th to about mid-day on the 16th and be a combination of lectures and hands-on sessions. As usually we’ll try to make this a free event, provided that our friends at HRL Labs can host us. We have been discussing the possibility of providing an advanced stream besides the “newbie” version we had been running in the past. Right now, we are gauging interest in this. So, if you are interested in participating on those two days, would you please let Ihor know 1) how many participants you expect from your organisation 2) whether you are interested in the newbie or an advanced version, 3) if advanced, what topics you would like covered Examples of advanced materials - advanced driver writing/porting, eg how to port a real Linux driver - advanced real-time topics: eg building stuff from scratch rather than filling in templates - locking and synchronisation - architecting seL4-based systems - process for building real systems: throw everything into a VM, and then extract bits into native components - anything specific you are interested in We’d imagine the advanced stream to be less structured, emphasising largely independent work on a specific problem, with people around to help. It could even be solving a particular problem you have (but we’d need to understand what you’re trying to build beforehand). Gernot & Ihor

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Gernot.Heiser＠data61.csiro.au 29 Sep '16

29 Sep '16

We have just received this comment on github, which I think merits some explanation: > There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. Summary: I accept that this is a valid use case, but the suggested solution is not the right one. There are two reasons why I’m saying this: 1) the current behaviour of send-only IPC is correct and cannot be changed, 2) send-only IPC is the wrong way to address this use case. Re (1): Anyone who tried to use seL4_Send() or seL4_NBSend() will likely have noticed that they are of very little use, because you don’t know whether the message was transferred. So, why can't we return at least a boolean value, indicating whether a message has been delivered or it was dropped on the floor? It’s simple: this would violate the dataflow guarantees provided by seL4. Send-only IPC is there to enable one-way information flow, and consequently can be invoked using a send-only cap. But a send-only cap must not allow any information flow from the receiver to the sender (or else all our isolation proofs would break down). Basically, a return status that can be influenced by the receiver constitutes a back channel that is not authorised by a cap, and as such is verboten. This means that send-only IPC is of very little practical use, except where you really want one-way information transfer, or you have a higher-level protocol that lets you get away with not knowing whether the message was lost. (Eg if the receiver being not ready is a protocol violation by the receiver, and it has only itself to blame for losing the message.) So, could we make send-only IPC a bit more useful by changing the semantics slightly? For example, we could have a return value that indicates successful message delivery if the send was invoked with a send+receive cap, but will always return false if the invocation used a send-only cap? In principle that would be doable without violating security requirements. The cost would be extra checking. It would also be somewhat unsystematic if the semantics of a send-only operation would depend on whether your cap has receive rights as well. It’d be arguably misleading, as you’re doing more than sending. This gets me to (2): send-only IPC is the wrong way to solve the problem. The above use case is clearly one where info flow is inherently two-way: you send something and need an acknowledgment of receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. The problem, of course, is that seL4_Call() is always blocking, there is no polling variant of this syscall. Should there be an seL4_NBCall()? Arguably yes, just as the RT branch already provides a seL4 SignalRecv() syscall, which is the non-blocking equivalent of seL4_ReplyRecv(). Will it happen? Possibly, but not in mainline the near future. The reason is that to add this (fairly simple) feature to the mainline kernel will require verifying it, and our verification engineers are presently very busy delivering on contracted milestones. We’ll discuss this internally. In the meantime I’ve added some explanation of the semantics of seL4_Send()/seL4NBSend() to the FAQ on the seL4 wiki. Gernot

4 6

quesion about TK1 Linux irq
by PX 27 Sep '16

27 Sep '16

Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng

2 1

Fwd: [Fwd: quesion about TK1 Linux irq]
by Jason.Butler＠data61.csiro.au 27 Sep '16

27 Sep '16

The irq numbers are remapped in: kernel/include/plat/tk1/plat/machine.h Jason ? -------- Forwarded Message -------- From: PX <seawolf.peng(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] quesion about TK1 Linux irq Date: Mon, 26 Sep 2016 17:38:47 -0400 Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Matt Rice 26 Sep '16

26 Sep '16

Gernot.Heiser wrote: > We have just received this comment on github, which I think merits some explanation: >> There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. ... >This gets me to (2): send-only IPC is the wrong way to solve the problem. > >The above use case is clearly one where info flow is inherently two-way: you send >something and need an acknowledgment of > receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than > separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. New to sel4 and the list (so sorry for stuffing up the threading) Couldn't at the expense of an extra notification send, use a notification where the receiver of the notification then should call the then do a non-blocking reply. I didn't see reply being non-blocking described in the manual so please correct me if i am wrong. This only works one party is willing to block correct, and there is no way to short circuit the call if an incoming message could be delivered to the call'ing process before the call can be completed? Although it would seem to take some amount of gymnastics to balance sending and receiving... so if really neither are willing to wait there is always notifications+shared memory?

3 4

Questions about Capability model
by Daniel Wang 21 Sep '16

21 Sep '16

Hi all, I’m new to the capability concept of seL4. Please correct me if I’m wrong. My understand of the capability is that it is a reference to a chunk of memory that allocated for specific purpose. Say if I want to do IPC between two threads A and B, I will need to apply an chunk of memory as endpoint, which give me a capability that I can pass from thread A to thread B is that correct? Also it is ok to assume the message passing mechanism in IPC is a producer-consumer model? The reason I ask it because I’m thinking is it possible for three (or more) threads that need to communicate with each other using the same endpoint, or it has to be paired for each two of those threads to use an endpoint? Thanks -Dan

3 4

developing a Ethernet card server for seL4
by PX 20 Sep '16

20 Sep '16

Hi, all, We want to develop a networking service on top of seL4, which works as a hypervisor, on Jetson TK1. We know that there is source code for lwip under /projects/util_libs/libethdrivers, but there is no support for TK1. We want to know how much effort needed to port the code to TK1 platform? Is it straightforward? Is there any TK1 ethernet driver source code available? Peng

3 3

How to run seL4 as a hypervisor?
by Daniel Wang 19 Sep '16

19 Sep '16

Hi all, Is there any document/tutorial about using seL4 as a hypervisor to running Linux on top? Appreciate for your help. Thanks -Dan

2 1

General Questions
by sixpackgurkenwasser＠use.startmail.com 15 Sep '16

15 Sep '16

Hello, I've got several questions. 1. Is there a simple way to relate a virtual address in the initial threads address space to the corresponding frame cap in the BootInfo? 2. In 8.2.2 of the manual it is stated in that "seL4 provides no way to obtain the physical address of a page from its capability". Isn't that exactly what the GetAddress method of a Page object does(10.4.14)? Cheers, Steve

3 2

Re: [seL4] General seL4 Kernel Questions
by Kofidoku.Atuah＠data61.csiro.au 13 Sep '16

13 Sep '16

Hey, welcome: ? > 1) Once the kernel boots, the control is given to a root task which we define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities? The root task is given capabilities to all kernel objects , and it has full permissions (Read-write-grant) on all of them -- you needn't do any work to cause the root task to have permissions/control over the initial objects. Just need to read and parse the BootInfo struct that describes how they are laid out in your CSpace. >2) Who is in-charge of scheduling or thread suspend (We can start new threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc? The kernel handles scheduling in the main, but threads can be suspended as needed by any other thread that has a capability to the TCB of the thread that you want to manage. Mainline seL4 currently doesn't support multicore, so there is no thread migration, and I do not know what form the multicore extensions will take, with regards to CPU affinity configuration as yet. It's not easy to speculate either, since the entire scheduler is going to undergo intrusive changes when the Real Time extensions are released. >3) While spawning a new thread? Who allocates virtual memory to it? And is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings? A new thread is initially a blank TCB -- to associate a virtual address space (VSpace) with it, you'd need to create a VSpace (seL4_Untyped_Retype), and then pass that to the kernel while configuring the TCB (seL4_TCB_Configure). The VSpace is also just a blank page directory, so you have to then create the page tables for the address space, and then create frames to map into the page tables, etc. The VSpace object is a light wrapper around hardware page tables, so yes, they cover a 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for itself. >4) What are the default things loaded into Virtual Memory of a thread? Only the Cspace maybe made available via CNode_mutates? or something else? Nothing -- the day that comes after the darkest night has the greatest number of possibilities -- or something like that: what I'm trying to say is that because no policy is enforced by the kernel (not even executable format) you have the greatest range of flexibility to do what you want with the new thread's VSpace. When you create a new VSpace there is nothing in it at all. The only exception is that when the kernel creates the root task's VSpace, it also then goes on to put the bootinfo struct into it, and in addition it allocates a stack and IPC buffer, and expands the root task's ELF image -- this is a special case because the root task is special. Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________

3 2

Re: [seL4] General seL4 Kernel Questions
by Andrew Mine 13 Sep '16

13 Sep '16

Hi Thanks a lot for the responses. It is much clearer now. I will delve a little bit more into this. Regards Andrew Mine On Mon, Sep 12, 2016 at 2:07 AM, <Kofidoku.Atuah(a)data61.csiro.au> wrote: > Hey, welcome: > > > 1) Once the kernel boots, the control is given to a root task which we > define. Does this root task have all permissions and capabilities or do we > still need to assign it capabilities? > > The root task is given capabilities to all kernel objects , and it has > full permissions (Read-write-grant) on all of them -- you needn't do any > work to cause the root task to have permissions/control over the initial > objects. Just need to read and parse the BootInfo struct that describes how > they are laid out in your CSpace. > > >2) Who is in-charge of scheduling or thread suspend (We can start new > threads from root task), is it also responsibility in root task to manage > and schedule it? Who is in charge of migrating the tasks, flushing CPUs > loading new stack etc? > > The kernel handles scheduling in the main, but threads can be suspended as > needed by any other thread that has a capability to the TCB of the thread > that you want to manage. Mainline seL4 currently doesn't support multicore, > so there is no thread migration, and I do not know what form the multicore > extensions will take, with regards to CPU affinity configuration as yet. > It's not easy to speculate either, since the entire scheduler is going to > undergo intrusive changes when the Real Time extensions are released. > > >3) While spawning a new thread? Who allocates virtual memory to it? And > is the virtual memory allocated equal to 4 GB like in linux kernel where > all applications get same Virtual Memory size but different mappings? > > A new thread is initially a blank TCB -- to associate a virtual address > space (VSpace) with it, you'd need to create a VSpace > (seL4_Untyped_Retype), and then pass that to the kernel while configuring > the TCB (seL4_TCB_Configure). The VSpace is also just a blank page > directory, so you have to then create the page tables for the address > space, and then create frames to map into the page tables, etc. The VSpace > object is a light wrapper around hardware page tables, so yes, they cover a > 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for > itself. > > >4) What are the default things loaded into Virtual Memory of a thread? > Only the Cspace maybe made available via CNode_mutates? or something else? > > Nothing -- the day that comes after the darkest night has the greatest > number of possibilities -- or something like that: what I'm trying > to say is that because no policy is enforced by the kernel (not even > executable format) you have the greatest range of flexibility to do what > you want with the new thread's VSpace. When you create a new VSpace there > is nothing in it at all. > > The only exception is that when the kernel creates the root task's VSpace, > it also then goes on to put the bootinfo struct into it, and in addition it > allocates a stack and IPC buffer, and expands the root task's ELF image -- > this is a special case because the root task is special. > > Kofi Doku Atuah > Kernel engineer > DATA61 | CSIRO > E kofidoku.atuah(a)data61.csiro.au > www.data61.csiro.au > > CSIRO's Digital Productivity business unit and NICTA have joined forces to > create digital powerhouse Data61 > ------------------------------ > > >

1 0

General seL4 Kernel Questions
by Andrew Mine 12 Sep '16

12 Sep '16

Hi I need help with some basic questions which I am getting confused of how seL4 is working. I am currently using the tutorials-seL4 branch. 1) Once the kernel boots, the control is given to a root task which we define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities? 2) Who is in-charge of scheduling or thread suspend (We can start new threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc? 3) While spawning a new thread? Who allocates virtual memory to it? And is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings? 4) What are the default things loaded into Virtual Memory of a thread? Only the Cspace maybe made available via CNode_mutates? or something else? I am sorry if the questions are silly, but I am getting confused. Thanks and Regards Andrew Mine

1 0

seL4 GDB
by Chris Guikema 09 Sep '16

09 Sep '16

Hello everyone, DornerWorks has developed a GDB-stub system for the ARMv7 platform (specifically Zynq 7000) that can be found at the following repos: https://github.com/dornerworks/gdbstub-app https://github.com/dornerworks/gdbstub-app-manifest If you have any questions, feel free to ask.

1 0

CAmkES Question
by Chris Guikema 02 Sep '16

02 Sep '16

Hello Ihor, My name is Chris Guikema, and I am an embedded systems engineer at DornerWorks, located in Grand Rapids Michigan. I am currently working on a project that requires the use of the CAmkES system, and I would like some help, if you are willing to. The project is to allow for debugging using CAmkES. The debugging process was successfully implemented in a simple seL4 program by using the init thread to set up an exception thread and setting up the exception endpoint, which was mapped to the init thread. The init thread was then used to implement a bad assembly code, which fired an exception. The exception handler thread was waiting on something to appear at the endpoint, and then grabbed the program counter and the stack of the init thread and sent it to a GDB function, which allowed debugging. My job is to replicate the debugging using CAmkES. However, CAmkES doesn't seem to want the application to utilize any of the seL4 system calls, and I don't believe the application knows its root cspace and vspace, so any attempt to initialize a debug thread and setup an exception endpoint just don't work. What steps do I need to take to 1, set up an endpoint that I could map to the exception endpoint (the simple libraries cause a vm fault), and 2, set up a thread that waits on the application to throw an exception and allow the debugging to occur. Any help you could send me would be appreciated. I look forward to hearing from you. Thanks Chris Guikema

2 1

sel4 as hypervisor
by Horace Blanc 01 Sep '16

01 Sep '16

Hi, I would like to have more information concerning the design of the hypervisor functionality in the sel4 project on ARMv7 architectures. >From what I read (FAQ/announcement from Adrian Danis in this mailing list), sel4 can run an application called VMM which adds that functionality. Here are my questions: 1) Did the design of this functionality require any change in the sel4 microkernel or is it just the VMM in userland that permits it? (what was in the arm_hyp branch that is now in master?) 2) Does this mean that it is a type-2 hypervisor? Do the guest OS run on top of the VMM? 3) How are the virtualization extentions of ARM used? More precisely what runs on the different protection levels (PL0, PL1 and PL2)? 4) To what extent is this hypervisor design pure? Do the guest OS know that it is running on top of seL4? Best, Horace BLANC

2 1

Genode 16.08 supports dynamic workloads on seL4
by Alexander Boettcher 31 Aug '16

31 Aug '16

Hello, we are proud to announce that the just released version 16.08 of the Genode OS Framework brings vastly extended seL4 support, which allows interactive and dynamic system scenarios to run directly on the x86 version of the seL4 kernel. With the new version, users of seL4 can compose dynamic operating systems from a plethora of ready-to-use Genode components. First, there are our time-tested device drivers and protocol stacks: - VESA driver (based on x86emu of XOrg) - Intel graphics driver (based on Linux 4.4.3), e.g., to drive external connectors - Intel wireless stack (based on Linux 4.4.3) including WPA supplicant - Network driver (based on iPXE) - AHCI, PS/2, PIT, ACPI driver - Audio driver (ported from OpenBSD 5.9) - USB driver (based on Linux 4.4.3) with hot-plug support - lwIP - light weight TCP/IP stack - Linux TCP/IP Stack (ported from Linux 4.4.3) - File-system support, e.g., ext2 based on Rump kernels Also, Genode includes a range of low-complexity resource multiplexers: - Secure GUI multiplexer - Nitpicker - Highly configurable and dynamical window manager - Audio mixer - Virtual networking components - Virtual file-system support For application development, there are several runtime environments and high-level libraries: - Noux - UNIX-like subsystem to run command-line-based GNU software like bash, vim, coreutils, gcc/g++, ... - Environments for the Rust, Python, and Lua programming languages - Base libraries like libc, standard C++ library, pthreads, OpenSSL, Readline etc. - Qt5 libraries and applications, including Webkit There's a lot more to explore and - in the pure microkernel way - each of these components are executed in user mode as separate protection domains on seL4. More details about version 16.08 can be found in the extensive release documentation: https://genode.org/documentation/release-notes/16.08 and, for the impatient, a life demo scenario of Genode on seL4 can be downloaded: https://www.genode.org/documentation/release-notes/16.08#Try_Genode_seL4_at… Best regards, -- Alexander Boettcher Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

1 0

Kernel extensions and userspace options
by Jonathan C Day 30 Aug '16

30 Aug '16

Hi, I am very interested in SEL4, partly because I was assured it was impossible to use Formal Methods in kernel development, partly because it's a fascinating project in its own right, but right now because there are some embedded applications that could do with the high level of reliability and security that provable correctness implies. Unfortunately, said applications need a comprehensive network stack and a powerful packet filtering/mangling engine. The latter could imaginably be done in the kernel, as it's deterministic, but I don't see any obvious value. Nonetheless, if someone has coded such a system as a third-party add-on, I would be very interested. There are good arguments for why the former can't be done, in a way that can be proven, and I really want the correctness. In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it? To be honest, I'm not sure I need a multitasking userspace, but I do absolutely need the network stack and packet filter. Everything else can be ported, albeit with difficulty. However, network operating systems are thin on the ground and tend to be proprietary, exactly what I don't want. For those curious, I'm looking to end up with a system with strong bounds on robustness and security, and that can handle things like multipath TCP, network failover, QoS and OpenFlow. However, all of these requirements boil down to a sequential process. Unnecessary complexity is where you end up with problems. If current wisdom says that there's nothing suitable in userspace, then does anyone know if there are there any existing Coloured Petri Nets that I could use to build what I need into the kernel? Even if I can't get better than a quasi-guarantee, it would be something.

3 6

Re: [seL4] Devel Digest, Vol 27, Issue 16 - High Assurance Hardware
by Tyga 30 Aug '16

30 Aug '16

> > Re: > > ------------------------------ > Date: Mon, 29 Aug 2016 23:01:45 +0000 > From: <Gernot.Heiser(a)data61.csiro.au> > <snip> > You may *think* that the manufacturers don?t make changes to the more > conventional bits of the hardware, and thus they are ?correct", but that > isn?t true, of course. And on top of that we know that there are > intentional backdoors in commercial hardware. > The only way around this is high-assurance hardware, and this doesn?t come > at an affordable cost. > > I think it?s an illusion to think one can partition hardware into trusted > and untrusted bits. In the end, the OS is at the mercy of the hardware, if > it?s faulty then you lose, there?s no way around it. A key attraction of seL4 is the trustworthiness of the microkernel. Running it on hardware with known bugs or features (e.g. recent Intel CPUs) that compromise the kernel's trustworthiness counteracts the perceived advantages. Perhaps, it would be possible to list CPUs (and possibly boards) that are recognised for being free of known potential attack vectors. I would certainly not want to invest time and effort into making seL4 run on hardware that could have be reasonably known to be of low assurance.

2 1

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

Dear seL4 developers, first, I'd like to thank you for publishing seL4 under GPL. I am very happy that I can finally get my hands dirty with working with the kernel of your group. :-) Currently, I am taking the first baby steps to bring the Genode OS framework (http://genode.org) to seL4. For reference, I am using the experimental branch. The first smallish issue I stumbled upon stems from the fact that Genode is written in C++. By compiling the seL4 syscall bindings with a C++ compiler, I got the following error: error: inconsistent operand constraints in an ‘asm’ It can be reproduced by putting the following code snippet into a cc file and compiling it with 'g++ -m32 -c' (tested with the Genode tool chain as well as with GCC 4.8.1): typedef enum { seL4_SysDebugPutChar = -9, _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1)) } seL4_Syscall_ID; void seL4_DebugPutChar(char c) { asm volatile ( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a" (seL4_SysDebugPutChar), "b" (c) : "%ecx", "%edx", "%esi", "%edi", "memory" ); } When compiling the same code snippet with 'gcc' instead of 'g++', everything is fine. It turns out that the C++ compiler does not like the enum value to be specified as input argument. I found the following ways to circumvent this problem: * Changing the enum value 'SysDebugPutChar' to a positive value, * Removing the definition of '_enum_pad_seL4_Syscall_ID', * Casting 'seL4_SysDebugPutChar' to an integer: : "a" ((int)seL4_SysDebugPutChar), In any case, I seem to have to change the bindings. Do you see a way around it? If not, would you consider one of the solutions above for the seL4 headers? On another note, I noticed that the bindings use the EBX register. Unfortunately, this makes it impossible to compile seL4 userland software as position-independent code (PIC). E.g., when compiling the above code snippet via 'g++ -m32 -fPIC -c', the following error occurs: error: inconsistent operand constraints in an ‘asm’ However, PIC is required in order to use shared libraries. The solution would be to not use EBX to pass arguments to the 'asm' statements, save EBX on the stack prior moving the respective kernel argument to the register, and, of course, restoring it after sysenter returns. Before I start changing the bindings, I'd like to know: is there anyone else working on the same problem? Would you be open to accept a change of the bindings to become PIC compliant on the costs of a few added instructions? Or do you have another suggestion how I should go about it? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

syscalls and tlb
by Vasily A. Sartakov 26 Aug '16

26 Aug '16

Greetings. I am working on MIPS port of seL4. Now I can run very simple hello world application which reads and dumps bootinfo page. In other words, I modified elfloader, added platform and architecture support to the kernel, add _sel4_start for mips in libsel4platsupport, adopted mips support of libmuslc to work with __sysinfo in mips and more. Now I have some questions. I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why? The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB? thank you. -- Vasily A. Sartakov sartakov(a)ksyslabs.org

4 5

Does anyone pay attention to Google's new operating system fuchsia
by XilongPei 24 Aug '16

24 Aug '16

Hi, Google has announced a new operating system fuchsia, https://github.com/fuchsia-mirror Its kernel is called Magenta, Magenta has a capability-based security model, this is very similar to seL4. Does anyone pay attention to Google's new operating system fuchsia? Xilong Pei Tongji University Shanghai, China 2016/8/24

3 3

x86: loosing edge triggered interrupts when using I/O APIC
by Alexander Boettcher 24 Aug '16

24 Aug '16

Hi, we are using as user level timer driver the PIT on Genode/seL4 and experience situations that the driver does not get IRQs after a while. It happens on Qemu as also on native x86 hardware. We tracked down the problem to the masking of edge-triggered IRQs on the I/O APIC in the seL4 kernel. According to Intel, [0] chapter 3.2.4 "Interrupt Mask R/W", edge interrupts on a masked interrupt pin gets ignored and are not held pending. On [2] there are also some discussion about this topic too. We solved/workaround the issue by this patch [1]. I looked additionally into two other microkernels using the I/O APIC and they don't mask edge level triggered I/O APIC interrupts. I wonder if anybody already stumbled about the issue on seL4/x86? If not, please take the patch or give advices to adapt the patch so that it may get upstream. Thanks, Alexander Boettcher. [0] http://www.intel.com/design/chipsets/datashts/29056601.pdf [1] https://github.com/genodelabs/genode/blob/master/repos/base-sel4/patches/io… [2] http://yarchive.net/comp/linux/edge_triggered_interrupts.html

2 1

New to seL4
by Andrew Mine 22 Aug '16

22 Aug '16

Hi I have just started looking at seL4 and I was wondering where can I find some documentation explaining the features and difference between seL4 and other kernels. I have gone through the manual and tutorial documents but nothing majorly explains how seL4 is different and its features. Any guidance towards any documentation will be helpful. Thanks Andrew

2 1