- Devel - lists.sel4.systems

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 13 Jul '18

13 Jul '18

?Hey Thad, Thanks for catching that: it turns out that we weren't passing -nostdlib to the linker when linking the ELFLoader, so the cross-toolchain's linker was trying to link the ELFLoader against the cross toolchain's libc, but it shouldn't be doing that and it should instead be using our libmuslc. A fix has been pushed out and you should be seeing it shortly. Thanks for your patience, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

seL4 vm examples with Qemu
by Mike Clark 12 Jul '18

12 Jul '18

Is it currently possible to boot the camkes-vm-example applications using qemu? I followed the directions here (https://github.com/seL4/camkes-vm-examples) to get a build of the minimal application. I then tried to follow the directions here ( https://docs.sel4.systems/Hardware/Qemu/#running-qemu) to boot using qemu. Unfortunately I get an error when trying to boot. The error says: *"seL4 caled fail at /host/camkes_vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :("* *halting...* *Kernel entry via Interrupt, irq 0* I'm running this on a ubuntu 16.04 machine with an Intel i5-4200U ( https://ark.intel.com/products/75459/Intel-Core-i5-4200U-Processor-3M-Cache… ). Thanks!

2 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 11 Jul '18

11 Jul '18

> > > On 11.07.2018 01:45, Jeremy Fields wrote: > > Here's my results from these permutations, using Genode 18.05 / sel4 > 9.0.1 > > (hopefully the formatting works). I know some permutations probably don't > > make sense, but I did them anyways. Any thoughts? I have the serial > output > > from these tests as well, but didn't want to overload this message with > > that. Additionally, can you folks share specific machine make/models that > > you know work with Genode/seL4? Hopefully some 'consumer off the shelf' > > stuff. > > We have no specific Genode/seL4 x86 hardware list, but there exists an > unofficial list at [0] which may serve your question. > > > PermuationResult > > Legacy / Multiboot 2 + Bender Memory region overlap > > Legacy / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > Legacy / Multiboot 1 crashes/reboots > > Legacy / Multiboot 2 Memory region overlap > > UEFI / Multiboot 2 + Bender Memory region overlap > > UEFI / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > UEFI / Multiboot 1 freezes? > > UEFI / Multiboot 2 Memory region overlap > > Thanks for testing. > > May you please apply the seL4 kernel patch and test, whether this solves > your issue ? > > > [0] http://usr.sysret.de/jws/genode/hcl.html > > -- > 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

Re: [seL4] Memory Region overlap error
by Jeremy Fields 11 Jul '18

11 Jul '18

> > Hello, > > On 05.07.2018 14:34, Jeremy Fields wrote: > > Sure - I've tried a few different combinations, but the latest Genode 18.5 > > used seL4 9.0.1. I'm attempting to use this on an x86 machine that has a > > Xeon 1607 and a dedicated GPU. The thread I referenced in my initial post > > implied that UEFI might be an issue, but I've tried both UEFI and legacy > > boots without success. I tried using/building Genode 17.5 with whatever > > version of seL4 it acquires, but get the same error. Let me know if there's > > anything else I can provide > > some suggestions from my side. > > Try to remove the chain bootloader "bender", just to exclude it as > potential reason of trouble. In genode/tool/run/boot_dir/sel4 remove the > "multiboot2 /boot/bender ..." line and adjust the line below from > "module2 /boot/sel4 ..." -> "multiboot2 /boot/sel4 ...". Use some simple > scenario for testing, like log.run > > If the issue persists, you may try to boot Genode/seL4 the Multiboot 1 > way instead of Multiboot 2, which however will solely work for BIOS > legacy boots (no UEFI). Replace the "multiboot2" and "module2" in > genode/tool/run/boot_dir/sel4 with "multiboot" and "module". > > > Cheers, > > Alex B. > > -- > 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 > Here's my results from these permutations, using Genode 18.05 / sel4 9.0.1 (hopefully the formatting works). I know some permutations probably don't make sense, but I did them anyways. Any thoughts? I have the serial output from these tests as well, but didn't want to overload this message with that. Additionally, can you folks share specific machine make/models that you know work with Genode/seL4? Hopefully some 'consumer off the shelf' stuff. PermuationResult Legacy / Multiboot 2 + Bender Memory region overlap Legacy / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) Legacy / Multiboot 1 crashes/reboots Legacy / Multiboot 2 Memory region overlap UEFI / Multiboot 2 + Bender Memory region overlap UEFI / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) UEFI / Multiboot 1 freezes? UEFI / Multiboot 2 Memory region overlap -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 11 Jul '18

11 Jul '18

Sorry Thad, I want to correct something I said: I recommended that you try the arm-linux-gnueabihf toolchain, but that should have been the arm-linux-gnueabi toolchain. Aside from that, I went and double checked, and this toolchain works just fine -- one thing to note though, is that you don't have to specify the -DCROSS_COMPILER_PREFIX=foo option, and you should be able to just use -DAARCH32=1 and our build system should automatically select the right toolchain to invoke for you (see: https://github.com/seL4/seL4/blob/master/gcc.cmake#L24?) Feel free to ask more questions about the new build system since we expect adaptation to take some time. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

ninja build tool error
by 송대영 11 Jul '18

11 Jul '18

Hello, I have question about sel4's new ninja build tool. *1. From now on, sel4-tutorials use ninja build tool, so I repo new sel4-tutorials.Last step, I executue this command "../init-build.sh --plat pc99 --tut hello-1" but It prints with this error messages.What's the problem?---------------------------------------------------------------------------------------------CMake Warning at tools/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does notCall Stack (most recent call first): tools/cmake-tool/base.cmake:58 (include) tools/cmake-tool/all.cmake:16 (include) CMakeLists.txt:23 (include)CMake Error at projects/sel4-tutorials/CMakeLists.txt:34 (message): You must select a tutorial for compilation. Select using -DTUTORIAL=<PREFERENCE>. Choose one of hello-1;hello-2;hello-2-nolibs;hello-3;hello-3-nolibs;hello-4;hello-4-app;hello-timer;hello-timer-client.-- Configuring incomplete, errors occurred!See also "/home/scribnote5/sel4-tutorials-manifest/build_hello_1/CMakeFiles/CMakeOutput.log".2. How can I build sel4 ia32 images in sel4bench?This command "../init-build.sh -DPLATFORM=ia32 -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE" doesn't make sel4bench image file.*

2 1

sel4test cross compiling for arm
by Thad Seeberger 11 Jul '18

11 Jul '18

Good day. Trying to build first test and run on qemu. Cmake failing to compile the test program. Does this with different versions of cross compile. Can someone point me in the right direction of where to start looking. thx Thad localhost build-arm]# ../init-build.sh -DCROSS_COMPILER_PREFIX=arm-none-eabi- -DPLATFORM=kzm -- The C compiler identification is GNU 7.3.1 -- The CXX compiler identification is GNU 7.3.1 -- Check for working C compiler: /opt/arm/bin/arm-none-eabi-gcc -- Check for working C compiler: /opt/arm/bin/arm-none-eabi-gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /opt/arm/bin/arm-none-eabi-g++ -- Check for working CXX compiler: /opt/arm/bin/arm-none-eabi-g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /opt/arm/bin/arm-none-eabi-gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FAILED -- Performing test SOFTFP_FLOAT with flags -mfloat-abi=softfp -- Test SOFTFP_FLOAT FAILED CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring done -- Generating done -- Build files have been written to: /home/maddthad/seL4test/build-arm -- Performing test SOFT_FLOAT with flags -mfloat-abi=soft -- Test SOFT_FLOAT FAILED CMake Error at tools/seL4/cmake-tool/flags.cmake:135 (message): Kernel does not support hardware floating point but toolchain cannot build software floating point Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring incomplete, errors occurred! See also "/home/maddthad/seL4test/build-arm/CMakeFiles/CMakeOutput.log". See also "/home/maddthad/seL4test/build-arm/CMakeFiles/CMakeError.log". CMakeError.log: compiling the C compiler identification source file "CMakeCCompilerId.c" failed. Compiler: /opt/arm/bin/arm-none-eabi-gcc Build flags: Id flags: The output was: 1 /opt/gcc-arm-none-eabi-7-2018-q2-update/bin/../lib/gcc/arm-none-eabi/7.3.1/../../../../arm-none-eabi/lib/libc.a(lib_a-exit.o): In function `exit': exit.c:(.text.exit+0x2c): undefined reference to `_exit' collect2: error: ld returned 1 exit status Compiling the CXX compiler identification source file "CMakeCXXCompilerId.cpp" failed. Compiler: /opt/arm/bin/arm-none-eabi-g++ Build flags: Id flags: The output was: 1 /opt/gcc-arm-none-eabi-7-2018-q2-update/bin/../lib/gcc/arm-none-eabi/7.3.1/../../../../arm-none-eabi/lib/libc.a(lib_a-exit.o): In function `exit': exit.c:(.text.exit+0x2c): undefined reference to `_exit' collect2: error: ld returned 1 exit status

2 1

Future plans w.r.t. Cortex-R
by piotr＠skrzypek.eu 10 Jul '18

10 Jul '18

Dear seL4 Maintainers, Could you please share what are your future support plans w.r.t. ARM Cortex-R family - the 'reliable' and 'real-time' side of ARM portfolio? Cortex-R implementations include interesting safety features i.a. lockstep processing. It feels like a good match for seL4 safety-oriented philosophy. However, Cortex-R processors have MPU instead of MMU, which seems to be ruling them out for now. Are there any plans to have an seL4 'MPU' branch in order to support these kind of processors? Thank you in advance, Piotr Skrzypek

3 4

Questions on U-boot Verified Boot with CAmkES-ARM-VM
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to test secure boot with the CAmkES-arm-vm. I found that U-boot has its implementation of secure boot called verified boot, but it seems only support FIT image format. I’m wondering is there a way to convert the final ELF image to an FIT image? I’m studying the details of different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much! Best Regards -Daniel Wang

2 1

sel4 qemu x86 runtime error
by Thad Seeberger 10 Jul '18

10 Jul '18

Compile now no problem however I'm getting error when running. I believe its an invalid opcode exception. I think my build not matching the qemu but I've tried diff machines and they do the same. I also get this warning during build, not sure if this relevant: Warning: Installation path /home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool not found on the PATH environment variable. make: Leaving directory `/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool' Qemu commanr, lines with ????? suspect: qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 (process:98550): GLib-WARNING **: gmem.c:483: custom memory allocation vtable not supported Boot config: parsing cmdline 'images/kernel-ia32-pc99 ' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false ???? Warning: Your kernel was not compiled for the current microarchitecture. Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fefe000 type 1 Adding physical memory region 0x100000-0x1f800000 Physical Memory Region from 1fffe000 size 2000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information Kernel loaded to: start=0x100000 end=0x160000 size=0x60000 entry=0x10005e ACPI: RSDP paddr=0xf7180 ACPI: RSDP vaddr=0xdfcf7180 ACPI: RSDT paddr=0x1ffffbc1 ACPI: RSDT vaddr=0xdffffbc1 ACPI: FADT paddr=0x1ffff1c0 ACPI: FADT vaddr=0xdffff1c0 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffffb11 ACPI: MADT vaddr=0xdffffb11 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected Detected 1 IOAPICs, but configured to use PIC instead Detected 1 boot module(s): module #0: start=0x161000 end=0x25aed0 size=0xf9ed0 name='images/capdl-loader-experimental-image-ia32-pc99' ELF-loading userland images from boot modules: size=0x189000 v_entry=0x804f544 v_start=0x8048000 v_end=0x81d1000 p_start=0x25b000 p_end=0x3e4000 Moving loaded userland images to final location: from=0x25b000 to=0x160000 size=0x189000 Starting node #0 with APIC ID 0 Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: ?????? user exception 0x6 code 0x0 in thread 0xff3f5d00 "rootserver" at address 0x805130e With stack: 0x80cfda0: 0x0 0x80cfda4: 0x0 0x80cfda8: 0x0 0x80cfdac: 0x0 0x80cfdb0: 0x0 0x80cfdb4: 0x0 0x80cfdb8: 0x0 0x80cfdbc: 0x0 0x80cfdc0: 0x0 0x80cfdc4: 0x0 0x80cfdc8: 0x0 0x80cfdcc: 0x0 0x80cfdd0: 0x0 0x80cfdd4: 0x0 0x80cfdd8: 0x0 0x80cfddc: 0x0 QEMU: Terminated Have a great day.

2 1