- Devel - lists.sel4.systems

seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)
by Blam Kiwi 07 Nov '18

07 Nov '18

I am investigating the use of seL4 on heterogeneous architectures such as the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm investigating that involves utilising both the Cortex-R5 cores and Core-A53 cores for different applications. I'm rather new to seL4 development so I'm a bit stuck and need some advice. It's easiest if I just list my requirements and assumptions for my architecture design: a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS Kernel to manage system resources and run virtual machines. b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. c) I require the use of the Cortex A53 cores for running unsafe Linux VMs. d) It's my understanding that seL4 lacks 64-bit multicore support for its own scheduler, but VMs running on seL4 could be provided with access to all the cores? (Eg: Linux) e) It's my understanding that seL4 lacks heterogeneous task scheduling, and cannot manage both the Cortex R5 and Cortex A53 cores. This leads me to make the following architectural conclusions: [1] It's not possible to boot an seL4 kernel on one processor and have it manage the other. [2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an seL4 kernel on each. [3] Some domain specific protocol is required for the CPU modules to communicate and share resources. Any help or advice would be appreciated. Regards, Robbie

4 4

Passing Network Resource to Linux VM in TK1-SOM
by Daniel Wang 07 Nov '18

07 Nov '18

Hi all, I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang

2 2

run docker on sel4
by Jia He 06 Nov '18

06 Nov '18

Hi all I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker. I am investigating the proper implemenatation for running docker on sel4 on arm64. There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated. Is there any other ways or anything else to make the implatation more feasible? --- Cheers, Justin

3 2

seL4 IPC and SMP question.
by 송대영 06 Nov '18

06 Nov '18

HI, I have a question about IPC and SMP. I ran sel4bench on sabre lite(i.mx6, arm v7). 1. I want to confirm performance difference between Lazy Scheduling and Beno Scheduling. Can I configure scheduler? 2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"? 3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means. What "Cycles" means in this benchmark? smp : This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput. 4. I try to measure IPC performance with SMP is on. I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles. Are these results are available?

3 2

Booting seL4test on x86 hardware
by Alex Pavey 31 Oct '18

31 Oct '18

Hello, We are having issues being able to get the seL4test userland image to boot on x86 hardware. We have attempted to boot with syslinux off a USB, with PXELINUX, and with grub and see the same userland image loading issue across boot methods. Build steps: - Following https://docs.sel4.systems/Hardware/IA32 - Using "-DPLATFORM=x86_64" o Does not appear to boot (no serial output) - Using "-DPLATFORM=ia32" o Kernel boots but is unable to load userland image The manifest commit hash is: 01c11cfcd881c1da5b7520162fae40f6eae1c16b Hardware: - DELL Optiplex 980 with an Intel Core i7 860 processor We are seeing the following serial output: SYSLINUX 6.03 20171017 Copyright (C) 1994-2014 H. Peter Anvin et al Loading sel4kernel... ok Loading rootserver... ok Boot config: parsing cmdline 'sel4kernel' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0x1d6000 end=0x4abdf4 size=0x2d5df4 name='rootserver' Parsing GRUB physical memory map Physical Memory Region from 0 size 9e400 type 1 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size df5cfc00 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from df6cfc00 size 54000 type 4 Physical Memory Region from df723c00 size 2000 type 3 Physical Memory Region from df725c00 size 8da400 type 2 Physical Memory Region from f8000000 size 4000000 type 2 Physical Memory Region from fed00000 size 400 type 2 Physical Memory Region from fed20000 size 80000 type 2 Physical Memory Region from fec00000 size 100000 type 2 Physical Memory Region from fee00000 size 100000 type 2 Physical Memory Region from ffb00000 size 500000 type 2 Physical memory region not addressable Physical memory region not addressable Multiboot gave us no video information ACPI: RSDP paddr=0xfec00 ACPI: RSDP vaddr=0xdfcfec00 ACPI: RSDT paddr=0xfc790 ACPI: RSDT vaddr=0xdfcfc790 ***WARNING*** SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com) consider enabling Kernel loaded to: start=0x100000 end=0x13a000 size=0x3a000 entry=0x100076 ACPI: RSDT paddr=0xfc790 ACPI: RSDT vaddr=0xdfcfc790 ACPI: FADT paddr=0xfc85c ACPI: FADT vaddr=0xdfcfc85c ACPI: FADT flags=0xa5 ACPI: DMAR paddr=0xfcdde ACPI: DMAR vaddr=0xdfcfcdde ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0xfc9c4 ACPI: MADT vaddr=0xdfcfc9c4 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x2 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x4 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x6 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x1 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x3 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x5 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x7 ACPI: Not recording this APIC, only support 1 ACPI: MADT_IOAPIC ioapic_id=8 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: BOOT MODULE: 0x1d6000: 0x0 0x1d6010: 0x0 0x1d6020: 0x0 0x1d6030: 0x0 0x1d6040: 0x0 0x1d6050: 0x0 0x1d6060: 0x0 0x1d6070: 0x0 0x1d6080: 0x0 0x1d6090: 0x0 0x1d60a0: 0x0 Boot module does not contain a valid ELF image seL4 called fail at /host/sel4test/kernel/src/arch/x86/kernel/boot_sys.c:813 in function boot_sys, saying "boot_sys failed for some reason :(" halting... Kernel entry via Interrupt, irq 0 Thanks, Alex

3 4

Camkes x86 VM Build Error
by Amit Goyal 30 Oct '18

30 Oct '18

Hi, I am using Ubuntu 16.04 on 64 Bit, i7 machine and running the CAmkES x86 VM instructions available at: https://docs.sel4.systems/CAmkESVM After running: ../init-build.sh -DCAMKES_VM_APP=minimal I am getting the following error: -------------------------------------------------------------------------------------------------------------------------------- camkes-gen.cmake is out of date. Regenerating... CMake Error at tools/camkes/camkes.cmake:593 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 678, in <module> sys.exit(main(sys.argv, sys.stdout, sys.stderr)) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 515, in main instantiate_misc_templates(renderoptions) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 509, in instantiate_misc_templates outfile_name=outfile.name, imported=read, options=renderoptions) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Renderer.py", line 109, in render self.templates, **kwargs) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Context.py", line 261, in new_context }.items()) + list(kwargs.items())) AttributeError: type object 'ObjectType' has no attribute '__members__' Call Stack (most recent call first): CMakeLists.txt:35 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/home/goyal/sel4/camkes_vm/build_vm/CMakeFiles/CMakeOutput.log". ------------------------------------------------------------------------------------------------------------------------------- I also tried to run the same instructions on a different machine (Ubuntu 16.04, 64 Bit, i5 machine) on which ../init-build.sh -DCAMKES_VM_APP=minimal is run successfully. It gets stuck on running ninja. I am getting the following error: -------------------------------------------------------------------------------------------------------------------------------- ghc-8.0.2: 106.97 MiB / 107.55 MiB ( 99.47%) downloaded... ghc-8.0.2: 107.24 MiB / 107.55 MiB ( 99.71%) downloaded... ghc-8.0.2: 107.50 MiB / 107.55 MiB ( 99.96%) downloaded... ghc-8.0.2: 107.55 MiB / 107.55 MiB (100.00%) downloaded... /home/akshat/.stack/programs/x86_64-linux/ghc-8.0.2.tar.xz.tmp: renameFile:renamePath:rename: does not exist (No such file or directory) Makefile:45: recipe for target 'parse-capDL' failed make: *** [parse-capDL] Error 1 ninja: build stopped: subcommand failed. -------------------------------------------------------------------------------------------------------------------------------- Can someone suggest a way out for both the problems. -- Thanks and Regards, Amit Goyal

2 3

can not build tutorials anymore
by Thad Seeberger 30 Oct '18

30 Oct '18

good day. I can no longer build tutorials. These used to build a month ago. My system hasn't changed and I can still build the older ones with no issues. I get lost trying to debug this cmake/python stuff. ./init --verbose --plat pc99 --tut hello-camkes-1 INFO:sh.command:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>: starting process DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: started process INFO:sh.command:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..', pid 17525>: process started DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: acquiring wait lock to wait for completion DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: got wait lock DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: exit code not set, waiting on pid -- The C compiler identification is GNU 7.3.1 -- The CXX compiler identification is GNU 7.3.1 -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/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/rh/devtoolset-7/root/usr/bin/g++ -- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/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/rh/devtoolset-7/root/usr/bin/gcc CMake Error at projects/sel4-tutorials/cmake/helpers.cmake:141 (message): Failed to render: PYTHONPATH=/home/john/sel4/projects/camkes/capdl/python-capdl-tool;python;/home/john/sel4/projects/sel4-tutorials/template.py;--tut-file;/home/john/sel4/projects/sel4-tutorials/tutorials/hello-camkes-1/hello-camkes-1;--out-dir;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/gen;--input-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/input_files;--output-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/output_files;--arch;x86_64;;;, Traceback (most recent call last): File "/home/john/sel4/projects/sel4-tutorials/template.py", line 154, in <module> sys.exit(main()) File "/home/john/sel4/projects/sel4-tutorials/template.py", line 142, in main render_file(args, env, state, file) File "/home/john/sel4/projects/sel4-tutorials/template.py", line 90, in render_file out_stream.write(template.render(context.get_context(args, state))) File "/home/john/sel4/projects/sel4-tutorials/tools/context.py", line 435, in get_context context.update(ObjectType.__members__.items()) AttributeError: type object 'ObjectType' has no attribute '__members__' Call Stack (most recent call first): projects/sel4-tutorials/cmake/helpers.cmake:164 (ExecuteGenerationProcess) projects/sel4-tutorials/CMakeLists.txt:29 (GenerateTutorial) -- Configuring incomplete, errors occurred! See also "/home/john/sel4/hello-camkes-1_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 91, in <module> File "./init", line 81, in main File "/home/john/sel4/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/john/sel4/projects/sel4-tutorials/common.py", line 69, in _init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output, _err=output) File "/sandbox/lib/python2.7/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/sandbox/lib/python2.7/site-packages/sh.py", line 774, in __init__ self.wait() File "/sandbox/lib/python2.7/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/sandbox/lib/python2.7/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 .. STDOUT: STDERR:

2 2

camkes-arm-vmm run multiple VMs at once
by Daniel Wang 26 Oct '18

26 Oct '18

Hi all, I’m wondering can the camkes-arm-vmm run multiple VMs at once? I know it is possible for X86 but I’m not sure about the ARM version. Thanks Best Regards -Daniel Wang

3 2

Kernel Exception in seL4 Tutorial
by Jeremiah Peschka 25 Oct '18

25 Oct '18

I’m attempting to build the seL4 tutorials on a local VM (Ubuntu 18.04 "Linux ubuntu 4.15.0-36-generic #39-Ubuntu SMP Mon Sep 24 16:19:09 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux”). I have confirmed that the VM has the pre-reqs present and the repository was synced using repo this afternoon. The builds succeed, but running the VM produces a kernel exception. Here is sample output from attempting to build the dynamic-1 tutorial: https://pastebin.com/NnShcREU A similar error occurs when I build the completed solution, as well. Using GDB, it appears that main is never reached. Thanks for any assistance, Jeremiah Peschka

2 6

seL4 IPC SMP
by 송대영 24 Oct '18

24 Oct '18

HI, I have question about IPC on SMP. I ran sel4bench on sabre lite(i.mx6, arm v7) which SMP is on. Sabre lite has 4 cores. I supposed that SMP improved IPC performances. But results were not. seL4_CALL SMP on 504 SMP off 336 Would you give me reason why these results are happened?

2 2