- Devel - lists.sel4.systems

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 29 May '17

29 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