- Devel - lists.sel4.systems

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

seL4 IPC fastpath question
by 송대영 08 Oct '18

08 Oct '18

Hello, I have question about seL4 IPC fastpath. I ran sel4bench on sabre lite(arm v7). 1. IPC fastpath can apply in seL4_Call and seL4_Reply_Recv, is it right? seL4_Send, seL4_Recv can't apply IPC fastpath. 2. IPC_fastpath can only send message that message's length is 0, is it right? I found these comments. /* Call slowpath, long IPC (10), same prio client to server, different address space */ /* ReplyRecv slowpath, long IPC (10), same prio server to client, on the slowpath, different address space */ 3. In seL4 IPC mechanism, IPC only use registers not memory?

3 2

Questions on CAMKES-ARM-VM Build and Components
by Daniel Wang 05 Oct '18

05 Oct '18

Hi all, It seems CAmkES-arm-vmm has been immigrated to cmake, How can I build it? I tried to build it by invoking: # ../init-build.sh -DCAMKES_VM_APP=tk1_vm -DPLATFORM=tk1 # ninja But it does not work. Also, thank for the detailed CAmkES X86 documents. I’m wondering does the VM Connector and kernel modules work for ARM architecture, TK1 or TK1-SOM specifically? Best Regards -Daniel Wang

3 6