- Devel - lists.sel4.systems

Compile errors for Beaglebone Black
by Todd_Peterson＠mgtsciences.com 31 Aug '17

31 Aug '17

Hi, I am trying to compile seL4 for the BBB. I am getting the following errors when it gets to timer_service. I am following the instructions at https://github.com/seL4/refos-manifest. I got past another compile error by adding a typedef to device_timer.h for pstimer_t. Any help is appreciated. // tfp, added to avoid compiler error typedef uint32_t pstimer_t; [apps/timer_server] building... [HEADERS] [STAGE] autoconf.h [CC] src/state.o In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:22:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h: In function 'data_open_map': /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h:95:69: warning: passing argument 6 o f 'data_open' from incompatible pointer type [-Wincompatible-pointer-types] d.dataspace = data_open(session, name, flags, mode, dspaceSize, &errnoRetVal); ^ In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:21:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client.h:72:11: note: expected 'int ** (*)()' but ar gument is of type 'int *' seL4_CPtr data_open(seL4_CPtr session, char* name, int flags, int mode, int size, int* errno); ^ [CC] src/device_timer.o /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_handle_irq': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:146:5: warning: implicit declaration of function 'timer _handle_irq' [-Wimplicit-function-declaration] timer_handle_irq(s->timerDev, irq); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_init': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:239:5: error: unknown type name 'timer_config_t' timer_config_t config; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: error: 'dm_timer_paddrs' undeclared (first use in this function) config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: note: each undeclared identifier is reported on ly once for each function it appears in /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:18: error: 'dm_timer_irqs' undeclared (first use in this function) config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:243:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:19: warning: implicit declaration of function 'ps_g et_timer' [-Wimplicit-function-declaration] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:17: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:250:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TICK_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:252:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TICK_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:253:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:258:16: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->tickDev = ps_get_timer(TICK_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:273:41: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->timerDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:274:19: warning: implicit declaration of function 'time r_get_nth_irq' [-Wimplicit-function-declaration] int irq = timer_get_nth_irq(s->timerDev, i); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:282:44: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->tickDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:289:21: warning: implicit declaration of function 'time r_start' [-Wimplicit-function-declaration] int error = timer_start(s->tickDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:310:13: warning: implicit declaration of function 'time r_periodic' [-Wimplicit-function-declaration] error = timer_periodic(s->timerDev, TIMER_PERIODIC_MAX); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_get_time': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:344:21: warning: implicit declaration of function 'time r_get_time' [-Wimplicit-function-declaration] uint64_t time = timer_get_time(s->timerDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:345:21: error: request for member 'properties' in somet hing not a structure or union if (!s->timerDev->properties.upcounter) { ^ make[1]: *** [/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/common/common.mk:265: src/device_timer.o] Error 1 make: *** [tools/common/project.mk:331: timer_server] Error 2 Todd Peterson Chief Embedded Systems Engineer Management Sciences, Inc. 6022 Constitution Ave NE Albuquerque, NM 87144 505-255-8611 (office) 505-205-7057 (cell) This email message and any attachments are for the sole use of the intended recipient(s) and may contain proprietary and/or confidential information which may be privileged or otherwise protected from disclosure. Any unauthorized review, use, disclosure or distribution is prohibited. If you are not the intended recipient(s), please contact the sender by reply email and destroy the original message and any copies of the message as well as any attachments to the original message.

1 0

Genode OS Framework 17.08 with extended seL4 support
by Alexander Boettcher 30 Aug '17

30 Aug '17

Hello, we're happy to announce the version 17.08 of the Genode OS Framework. Within the last release cycle (3-months) we upgraded our Genode/seL4 support from kernel version 3.2.0 to 6.0.0, enabled x86_64 and ARM support, added UEFI support to the seL4 kernel and enabled SMP for x86. A summary of changes and features are: - Hardware-accelerated graphics for Intel Gen-8 GPUs - The seL4 6.0 kernel on ARM and 64-bit x86 hardware - Genode as Xen DomU - Preliminary UEFI support for NOVA, base-hw, and seL4 - New server for capturing reports to files - New runtime for the sequential execution of components - Support for boot-time initialized frame buffer - FatFS-based VFS plugin - Extended non-blocking operation of the VFS - Refined time handling - Updated Muen separation kernel The long version of the official release documentation: https://genode.org/documentation/release-notes/17.08 All the best, -- 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 1

x86_64 kernel crash
by Alexander Boettcher 30 Aug '17

30 Aug '17

Hello, we're are in progress of extending our Genode/seL4 support, namely adding x86_64 and ARM support. During this work I encountered on x86_64 some sporadically crashes of the seL4 kernel. It happened during the debugging of our roottask on seL4 in form of a page fault in the kernel ("KERNEL EXCEPTION") or a static assertion in the kernel (see below). >From my understanding, this shouldn't be possible based on your verification work. Nevertheless, it happens reliable. (To be fair, the roottask was in this scenario already a bit confused and did things wrong - which however should never be enough to force the kernel in an exception or assertion - I presume.) I saved and stripped down the scenario which causes the kernel exception with high reliably and hope you can re-produce it and find the root cause. I stripped down the scenario to just the Genode image binary and the steps we did to create the seL4 kernel from the vanilla sources. Steps to reproduce: qemu-system-x86_64 -no-kvm -serial stdio -m 512 -kernel sel4 -initrd bomb_image.elf The binaries of "bomb_image.elf" can be found at [1] and the kernel "sel4" at [2]. The kernel is based on seL4 6.0 and a patch to pc99/autoconf.h (see [0]). Beside that it is the vanilla 6.0 kernel: https://github.com/seL4/seL4.git git commit 8564ace4dfb622ec69e0f7d762ebfbc8552ec918 "update VERSION file to 6.0.0" patch -p1 <~autoconfig.patch BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 make objcopy -O elf32-i386 kernel.elf.strip sel4 (Qemu complains otherwise about 64bit elf for boot) The final "sel4" binary can be used with the "bomb_image.elf" and qemu as pointed out above. I tried Qemu 2.5.0 as shipped with Ubuntu 16.04 LTS and Qemu 2.8.0 (self-compiled). On real hardware the scenario typically leads after a while (kernel booted, roottask booted, scenario starts to run) to a reboot (without the messages or assertion as in the Qemu case, see below). The tool-chain for Genode is based on GNU GCC 6.3.0 (see [3] and [4]). The kernel was either compiled with Genode's toolchain (6.3.0) or with the standard GCC as provided by Ubuntu 16.04 LTS (GCC 5.4.0). On x86_32 I could not reproduce the issue. (On ARM I did not try.) I hope the information are helpful - if you need more just ask. Cheers, Alex. ========== KERNEL EXCEPTION ========== Vector: 0xe ErrCode: 0x0 IP: 0xffffffff80720e60 SP: 0xffffffff80740e08 FLAGS: 0x6 CR0: 0x8000003b CR2: 0x3007065 (page-fault address) CR3: 0x1ffb000 (page-directory physical address) CR4: 0x220 Stack Dump: *0xffffffff80740e08 == 0xffffff8001a99b00 *0xffffffff80740e10 == 0xffffffff80729b1f *0xffffffff80740e18 == 0x1 *0xffffffff80740e20 == 0xffffffff80721c59 *0xffffffff80740e28 == 0xffffffff *0xffffffff80740e30 == 0x0 *0xffffffff80740e38 == 0xffffff801f02b740 *0xffffffff80740e40 == 0xffffff801f02b740 *0xffffffff80740e48 == 0x1 *0xffffffff80740e50 == 0xffffff8001a99000 *0xffffffff80740e58 == 0x7 *0xffffffff80740e60 == 0x59 *0xffffffff80740e68 == 0xffffff8001a99b00 *0xffffffff80740e70 == 0xffffffff80729cf3 *0xffffffff80740e78 == 0x9000000000000007 *0xffffffff80740e80 == 0xffffff8001a99059 *0xffffffff80740e88 == 0xffffff80ffffffff *0xffffffff80740e90 == 0xffffffff80740f18 *0xffffffff80740e98 == 0xffffff800013c200 *0xffffffff80740ea0 == 0x10000 Halting... halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 16 or seL4 failed assertion '(cte_t*)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && (cte_t*)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at src/object/cnode.c:457 in function cteInsert halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 18 or a fault by the roottask (and not in the kernel). So - this is no issue for the kernel: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x18 with status 0x4 in thread 0xffffff800013c200 "child of: 'rootserver'" at address 0x20419cf [0] https://github.com/alex-ab/genode/blob/crash_sel4_kernel_vanilla/autoconfig… [1] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/image_bomb.… [2] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/sel4 [3] https://genode.org/download/tool-chain [4] https://sourceforge.net/projects/genode/files/genode-toolchain/17.05/ -- 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 3

Arm VMM Vchan
by Enrique Leon 26 Aug '17

26 Aug '17

Hello to All, I am trying to do some message passing between a vm component and a camkes component. I have tried by enabling the Vchan option on the build system and compiling the helloworld linux user level program on a tk1. I received an error about the /dev/vmm_manager not being able to open. What is the proper method of setting up the Vchan communication for camkes-arm-vmm on a tk1? Thank You

1 0

Re: [seL4] Devel Digest, Vol 39, Issue 26
by talos 25 Aug '17

25 Aug '17

Dear, I used "qemu-system-i386 -m 1024 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99" It showed "Booting from ROM" Thanks, Sincerely ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Thu, Aug 24, 2017 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 39, Issue 26 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: about camkesvm (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 24 Aug 2017 00:00:19 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] about camkesvm Message-ID: <1503532819201.94096(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hey Talos, Sorry we didn't make this clearer on that page: those defconfigs build an x86-pc image; not an ARM image. Could you try running Qemu again, but with something similar to, qemu-system-i386 -m <WHATEVER_RAM_SIZE_YOU_WANT> -kernel <SEL4_KERNEL_IMAGE> -initrd <CAPDL_INITRD_IMAGE> And tell me what happens? Sorry for the inconvenience. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: 22 August 2017 15:39 To: devel Subject: [seL4] about camkesvm Hi I started the tutorial following the link: https://wiki.sel4.systems/CAmkESVM I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99 but the error is Segmentation fault (core dumped) what's wrong? Thanks Sincerely -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170824/cd4992b3/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 39, Issue 26 *************************************

2 1

camkes-arm-vm Platform Support
by Robert VanVossen 25 Aug '17

25 Aug '17

Hello, Is Data61 or anyone else working on porting camkes-arm-vm to platforms other than the TK1? Thank you, Robbie VanVossen DornerWorks, Ltd.

2 1

about camkesvm
by talos 24 Aug '17

24 Aug '17

Hi I started the tutorial following the link: https://wiki.sel4.systems/CAmkESVM I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99 but the error is Segmentation fault (core dumped) what's wrong? Thanks Sincerely

2 1

Raspberry Pi3 + seL4
by Steven Johnston 23 Aug '17

23 Aug '17

Has anyone had issues with serial when running the test suite on a Raspberry Pi 3b? Currently I am following the blog post: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ In the seL4test project I have successfully compiled sel4test-driver-image-arm-bcm2837 from rpi3_debug_xml_defconfig. Along with this I have the following files: bootcode.bin, start.elf, u-boot.bin, and config.txt. Bootcode.bin and start.elf are from the current Raspian firmware. Config.txt just contains a line to enable UART ("enable_uart=1") and one to point and u-boot.bin ("kernel=u-boot.bin"). And per the comment section of the seL4 post I downgraded the version of u-boot to before March 2017 (currently using Jan 2017). I am not deviating from the blog posting but I am experiencing an issue not mentioned. I have no serial output (I do have a u-boot terminal prompt through HDMI, so I can load/boot the binary). When I boot seL4 I receive the misaligned cache messages (through HDMI) and then it hangs. Without serial I have no eyes to see if the seL4 tests are running. Other than wiring into the RPI3 UART (GND/TX/RX on pins 6/8/10) and enabling UART in config.txt is there another step I'm missing? Thanks for any direction you can point me in, Steve

2 2

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

22 Aug '17

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

1 0

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

21 Aug '17

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

1 0

mpu vs mmu
by Thomas Dundon 21 Aug '17

21 Aug '17

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

3 2

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

19 Aug '17

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

1 0

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

18 Aug '17

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

2 6

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

05 Aug '17

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

2 11

rumprum and camkes
by Michal Podhradsky 05 Aug '17

05 Aug '17

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

2 1

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

05 Aug '17

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

2 2

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

03 Aug '17

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

4 4

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

31 Jul '17

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

2 1

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