July 2018 - Devel - lists.sel4.systems

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

ARM Vchan Error
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong). Here is what I did so far: 1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev); --------------------------------------------------- vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){ //uint32_t data = fault_get_data(fault); uint32_t data = fault_get_ctx(fault)->r1; vchan_entry_point(vm, data); // fflush(stdout); advance_fault(fault); return 0; } struct device vchan_dev = { .devid = DEV_CUSTOM, .name = "vchan-driver", .pstart = 0x2040000, .size = 0x1000, .handle_page_fault = &vchan_device_fault_handler, .priv = NULL, }; --------------------------------------------------- 2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following: --------------------------------------------------- int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) { int res = 0; int err; unsigned phys_ptr = virt_to_phys(vmcall); vmcall->data = data; vmcall->cmd = cmd; vmcall->phys_data = virt_to_phys(data); vmcall->size = sz; down(&hyp_sem); /* Set up arguments for the ARM hyp call */ asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1"); asm volatile (".arch_extension virt\n\t” "hvc #0"); asm volatile ("mov %0, r0" : "=r" (res) : : ); err = vargs->err; up(&hyp_sem); return err; } --------------------------------------------------- The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information. --------------------------------------------------- # modprobe driver.ko [81.826621] driver: loading out-of-tree module taints kernel Bad sys call from [Linux]: scone 0 at PC: 0xbf000214 Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407) ————————————————————————— I’m not sure if this error is triggered by the modified call_into_hypervisor() or by event_thread_run()->eventfd_signal(). Any help would be appreciated! Thanks in advance. Best Regards -Daniel Wang

2 1

reading thread registers
by Michael Neises 10 Jul '18

10 Jul '18

Hello, I know there exists a function seL4_TCB_ReadRegisters, which can read the registers of a certain thread, given a/the capability to the thread. Ultimately, I'm interested in reading memory at runtime to determine whether the data I expect is present. So I'm wondering, is there in seL4 an init process, whose registers contain all the working memory of the system? And furthermore, how can I access a capability to a given thread in order to pass it into the ReadRegisters function mentioned above? Cheers, Michael

2 1

Memory Region overlap error
by Jeremy Fields 09 Jul '18

09 Jul '18

Hello- I'm trying to boot Genode/seL4 on hardware. I've tried a few different combinations of versions, and GRUB configurations, without success. I keep getting the same error despite these different combinations There was a thread that touched on this, but I couldn't find any resolution http://sel4.systems/pipermail/devel/2017-December/001776.html @##################################### Bender: Hello World. framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type Boot config: parsing cmdline 'sel4 disable_iommu' Boot config: console_port = 0x3f8 ▒Boot config: debug_port = 0x3f8 Boot config: disable_iommu = true module #0: start=0xf8f0000 end=0xffff228 size=0x70f228 name='image.elf' Physical Memory Region from 0 size 9ac00 type 1 Physical Memory Region from 9ac00 size 5400 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 18dbb000 type 1 Adding physical memory region 0x100000-0x18ebb000 Physical Memory Region from 18ebb000 size 12d000 type 4 Physical Memory Region from 18fe8000 size 1000 type 1 Adding physical memory region 0x18fe8000-0x18fe9000 Physical Memory Region from 18fe9000 size 17000 type 4 Physical Memory Region from 19000000 size 4ffd000 type 1 Adding physical memory region 0x19000000-0x1dffd000 Physical Memory Region from 1dffd000 size 3000 type 3 Physical Memory Region from 1e000000 size 8e784000 type 1 Adding physical memory region 0x1e000000-0x1f800000 Physical Memory Region from ac784000 size 94000 type 2 Physical Memory Region from ac818000 size fe8000 type 1 Physical Memory Region from b0000000 size 4000000 type 2 Physical Memory Region from fed20000 size 20000 type 2 Physical Memory Region from fed50000 size 40000 type 2 Physical Memory Region from ffa00000 size 40000 type 2 Physical Memory Region from 1000000000 size 350000000 type 1 Physical memory region not addressable Adding physical memory region 0x0-0x1f800000 seL4 failed assertion '!p_region_overlaps(reg)' at /home/critical/Downloads/genode-18.05/contrib/sel4-c59276cc6e3aa138a1e56af8c8a56ce64cf327b8/src/kernel/sel4/src/ arch/x86/kernel/boot.c:123 in function add_allocated_p_region halting... Kernel entry via Interrupt, irq 0 @##################################### Any thoughts? Anything I can try? Any information I can provide to help diagnose? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

3 3

We're hiring OS engineers
by Gernot.Heiser＠data61.csiro.au 06 Jul '18

06 Jul '18

Would you like to work on seL4 inside the TS team? Here’s your chance: https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-System-Engineer/488529400/ https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-Systems-Senior-Engineer/4… Gernot

1 0