Devel October 2018

devel@sel4.systems

20 participants
24 discussions

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

Camkes VM Linux tutorial
by hedi delpazir 23 Oct '18

23 Oct '18

Hi, After running ./init --plat pc99 --tut camkes-vm-linux(following https://docs.sel4.systems/Tutorials/camkes-vm-linux.html) following error will occurred: -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc CMake Error at projects/camkes/vm/camkes_vm_helpers.cmake:21 (ApplyCommonReleaseVerificationSettings): ApplyCommonReleaseVerificationSettings Function invoked with incorrect arguments for function named: ApplyCommonReleaseVerificationSettings Call Stack (most recent call first): camkes-vm-linux/CMakeLists.txt:10 (include) -- camkes-gen.cmake is out of date. Regenerating... -- Configuring incomplete, errors occurred! See also "/home/hedi/sel4-tutorials-manifest/camkes-vm-linux_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 91, in File "./init", line 81, in main File "/home/hedi/sel4-tutorials-manifest/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/hedi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 69, in _init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output, _err=output) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 1427, in *call* return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 774, in *init* self.wait() File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=camkes-vm-linux .. STDOUT: STDERR: Any Idea?

2 1

CAmkES-VM Stalling
by Chris Guikema 23 Oct '18

23 Oct '18

Hello, I am seeing a weird issue with the CAmkES-VM. Just last week, I was able to run the VM successfully using the "minimal" version. I followed these steps: $ repo init -u https://github.com/seL4/camkes-vm-examples-manifest.git $ repo sync $ mkdir test && cd test $ ../init-build.sh -DCAMKES_VM_APP=minimal $ ninja Everything compiles correctly. I then had to use ccmake .. to switch the FPU save method to FXSAVE before recompiling. My QEMU command is: $ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 1 -cpu Nehalem,+vmx -nographic My QEMU version is: $ qemu-system-x86_64 --version QEMU emulator version 2.5.0 (Debian 1:2.5+dfsg-5ubuntu10.32), Copyright (c) 2003-2008 Fabrice Bellard And I'm running on Ubuntu 16.04. I get as far as: [ 1.930000] clocksource: Switched to clocksource pit [ 2.274669] VFS: Disk quotas dquot_6.6.0 [ 2.324891] VFS: Dquot-cache hash table entries: 1024 (order 0, 4096 bytes) [ 2.463451] hugetlbfs: disabling because there are no supported hugepage sizes [ 2.562973] random: fast init done After that, everything just runs extraordinarily slowly, or ends up stalling out completely. This is a change from a couple weeks previously, were I could get to the login prompt within ~10s using the minimal VM configuration. Has anything changed in the past few weeks that would have caused this? Thanks, Chris

2 1

MCS tutorial
by hedi delpazir 23 Oct '18

23 Oct '18

Hi, After running ninja in build directory(following https://docs.sel4.systems/Tutorials/mcs.html) following error will occurred: [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/parse-capDL Copied executables to /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build: - parse-capDL Warning: Installation path /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build not found on the PATH environment variable. ninja: build stopped: subcommand failed. Any idea?

2 1

FOSDEM 2019 - Microkernels developer room - CfP
by Alexander Boettcher 12 Oct '18

12 Oct '18

FYI -------- Forwarded Message -------- Subject: FOSDEM 2019 - Microkernels developer room - CfP Date: Thu, 11 Oct 2018 11:48:24 +0200 From: Sebastian Sumpf <Sebastian.Sumpf(a)genode-labs.com> Reply-To: Genode users mailing list <users(a)lists.genode.org> To: users(a)lists.genode.org FOSDEM 2019 - Microkernels and Component-based OSes devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2019 [1] in Brussels, Belgium and will share a developer room on Sunday February 03, 2019 [2]. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and componenent-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * enabling support for hardware (architectures, device drivers) * used languages and tools * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos Please use the Pentabarf [3] system to submit your proposals. You do not need to create a new account if you already have one. When in doubt, please use the devroom mailing list [4]. If you do not want to give a talk yourself, you may still send suggestions for what else you would like to see, or do in the devroom. Please send your suggestions to the mailing list. The deadline for your proposal is on December the 1st 2018. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (please, at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December the 15th on the devroom's mailing list and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. About the devroom Since the first Microkernel devroom in 2012 this devroom has been part of each following FOSDEM. By now it has become a somewhat institutionalized tradition for the micro kernel community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the Microkernel devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2019 will not be any different, so there is going to be a microkernel family dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. Important dates recap * 01.12.2018: Deadline for submissions * 15.12.2018: Schedule published and speakers notified of acceptance * 03.02.2019: The devroom takes places Links [1] http://fosdem.org [2] https://fosdem.org/2019/practical/transportation [3] https://penta.fosdem.org/submission/FOSDEM19 [4] https://lists.fosdem.org/listinfo/microkernel-devroom See you all at FOSDEM! _______________________________________________ Genode users mailing list users(a)lists.genode.org https://lists.genode.org/listinfo/users

1 0

Reverse back to Original TK1-SOM U-boot
by Daniel Wang 12 Oct '18

12 Oct '18

Hi all, I’m using a TK1-SOM board. Following the document (https://docs.sel4.systems/Hardware/CEI_TK1_SOM/#u-boot <https://docs.sel4.systems/Hardware/CEI_TK1_SOM/#u-boot>) I flashed the U-boot to enable booting HYP mode. How do I reverse back to the original U-boot so that I can boot the original on board Linux? Thank you! Best Regards -Daniel Wang

2 5

US Army SBIR calls for open HW/SW stack
by Gernot.Heiser＠data61.csiro.au 09 Oct '18

09 Oct '18

… and mentions seL4 prominently: https://www.sbir.gov/sbirsearch/detail/1508741

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel October 2018