- Devel - lists.sel4.systems

Adding a library to the executable
by Chris Koziarz 22 Oct '20

22 Oct '20

Hi all, This might be a CMake rather than seL4 question, but bear with me because I'm new to CMake so still I don't understand how seL4 is being built. I don't know how to add and link a piece of new code (a static library) to the executable. I add the statements to the CMakeList.txt: add_library(chrises_lib STATIC ${sources}) target_link_libraries(chrises_lib ...) and I can see libchrises_lib.a being built. By examining build.ninja, I can see the whole bunch of libraries (.a files) being pulled in by the linker, but there is no chrises_lib.a in the long list of .a files. And the result is obviously 'undefined reference to' all symbols that are im[lemented in chrises_lib.a. What am I missing? What do I have to add to the series of CMakeList.txt and where I need to add (besides add_library and target_link_libraries that I'm already using per above), in order for my chrises_lib.a be included in the list at static libs below? ############################################# # Link the executable apps/sel4test-driver/sel4test-driver build apps/sel4test-driver/sel4test-driver: C_EXECUTABLE_LINKER__sel4test-driver apps/sel4test-driver/archive.o apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/arch/arm/arch.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/main.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/interrupt.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/syscall.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/tests/timer.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/testtypes.c.obj apps/sel4test-driver/CMakeFiles/sel4test-driver.dir/src/timer.c.obj | libsel4/libsel4.a apps/sel4test-driver/sel4runtime/libsel4runtime.a apps/sel4test-driver/seL4_libs/libsel4allocman/libsel4allocman.a apps/sel4test-driver/seL4_libs/libsel4vka/libsel4vka.a apps/sel4test-driver/seL4_libs/libsel4utils/libsel4utils.a apps/sel4test-driver/sel4_projects_libs/libsel4rpc/libsel4rpc.a apps/sel4test-driver/seL4_libs/libsel4test/libsel4test.a apps/sel4test-driver/seL4_libs/libsel4platsupport/libsel4platsupport.a apps/sel4test-driver/seL4_libs/libsel4muslcsys/libsel4muslcsys.a apps/sel4test-driver/libsel4testsupport/libsel4testsupport.a apps/sel4test-driver/seL4_libs/libsel4test/libsel4test.a apps/sel4test-driver/sel4_projects_libs/libsel4rpc/libsel4rpc.a apps/sel4test-driver/sel4_projects_libs/libsel4nanopb/libsel4nanopb.a apps/sel4test-driver/sel4_projects_libs/libsel4nanopb/libnanopb.a apps/sel4test-driver/seL4_libs/libsel4sync/libsel4sync.a apps/sel4test-driver/seL4_libs/libsel4serialserver/libsel4serialserver.a apps/sel4test-driver/seL4_libs/libsel4utils/libsel4utils.a apps/sel4test-driver/util_libs/libelf/libelf.a apps/sel4test-driver/util_libs/libcpio/libcpio.a apps/sel4test-driver/seL4_libs/libsel4platsupport/libsel4platsupport.a apps/sel4test-driver/sel4runtime/libsel4runtime.a apps/sel4test-driver/util_libs/libplatsupport/libplatsupport.a apps/sel4test-driver/util_libs/libfdt/libfdt.a apps/sel4test-driver/seL4_libs/libsel4simple-default/libsel4simple-default.a apps/sel4test-driver/seL4_libs/libsel4debug/libsel4debug.a apps/sel4test-driver/seL4_libs/libsel4vspace/libsel4vspace.a apps/sel4test-driver/seL4_libs/libsel4simple/libsel4simple.a apps/sel4test-driver/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a apps/sel4test-driver/util_libs/libutils/libutils.a apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a || apps/sel4test-driver/libsel4testsupport/libsel4testsupport.a apps/sel4test-driver/musllibc/muslc_gen apps/sel4test-driver/seL4_libs/libsel4allocman/libsel4allocman.a apps/sel4test-driver/seL4_libs/libsel4debug/libsel4debug.a apps/sel4test-driver/seL4_libs/libsel4debug/sel4debug_Gen apps/sel4test-driver/seL4_libs/libsel4muslcsys/libsel4muslcsys.a apps/sel4test-driver/seL4_libs/libsel4muslcsys/sel4muslcsys_Gen apps/sel4test-driver/seL4_libs/libsel4platsupport/libsel4platsupport.a apps/sel4test-driver/seL4_libs/libsel4platsupport/sel4platsupport_Gen apps/sel4test-driver/seL4_libs/libsel4serialserver/libsel4serialserver.a apps/sel4test-driver/seL4_libs/libsel4serialserver/sel4serialserver_Gen apps/sel4test-driver/seL4_libs/libsel4simple-default/libsel4simple-default.a apps/sel4test-driver/seL4_libs/libsel4simple/libsel4simple.a apps/sel4test-driver/seL4_libs/libsel4sync/libsel4sync.a apps/sel4test-driver/seL4_libs/libsel4test/libsel4test.a apps/sel4test-driver/seL4_libs/libsel4test/sel4test_Gen apps/sel4test-driver/seL4_libs/libsel4utils/libsel4utils.a apps/sel4test-driver/seL4_libs/libsel4utils/sel4utils_Gen apps/sel4test-driver/seL4_libs/libsel4vka/libsel4vka.a apps/sel4test-driver/seL4_libs/libsel4vka/sel4vka_Gen apps/sel4test-driver/seL4_libs/libsel4vspace/libsel4vspace.a apps/sel4test-driver/sel4_projects_libs/libsel4nanopb/libnanopb.a apps/sel4test-driver/sel4_projects_libs/libsel4nanopb/libsel4nanopb.a apps/sel4test-driver/sel4_projects_libs/libsel4rpc/libsel4rpc.a apps/sel4test-driver/sel4runtime/libsel4runtime.a apps/sel4test-driver/sel4runtime/sel4runtime_Gen apps/sel4test-driver/sel4test-driver_Gen apps/sel4test-driver/sel4test-tests/sel4test-tests apps/sel4test-driver/util_libs/libcpio/libcpio.a apps/sel4test-driver/util_libs/libelf/libelf.a apps/sel4test-driver/util_libs/libfdt/libfdt.a apps/sel4test-driver/util_libs/libplatsupport/libplatsupport.a apps/sel4test-driver/util_libs/libplatsupport/platsupport_Gen apps/sel4test-driver/util_libs/libutils/libutils.a apps/sel4test-driver/util_libs/libutils/utils_Gen kernel/kernel_Gen libsel4/libsel4.a libsel4/sel4_Gen libsel4/sel4_autoconf_Gen

2 2

Connectivity of 2 sel4 powered systems
by ogosinkem＠gmail.com 21 Oct '20

21 Oct '20

Hi all, I wanted to ask what the best way to connect to Odroid-C2 boards that run the sel4 microkernel to each other using picotcp or the preferred library for network connectivity. Is there a way to connect them wirelessly or is an ethernet connection a must?. I'm very new to the sel4 kernel so I apologise if these questions seem basic and generic. Sincerely, Nkem Ogosi

2 1

Camkes-arm-vm + MCS?
by Jim McColl 20 Oct '20

20 Oct '20

So I have been messing with seL4 for about a month now and I have been having a wonderful time! But I would like to do something kind of wacky. I’d like to run a couple of virtual machines like in the vm_multi example…but with MCS. I remember reading on the website a while back that virtualization + MCS was not supported, but then all the seL4 Foundation changes happened and I can no longer find that reference. So I was wondering if there is virtualization support with MCS on the public seL4 side yet? (Or maybe the private side github? If so I’d be more than happy to write a toy to test it out on some of the hardware (TK1SOM, TX2) I have here at the house [image: :smile:]) I decided to take a day and play with trying to get the vm_cross_connector and MCS (using the mcs-examples) to play nice together using platform qemu-arm-virt…but I’m currently stuck on a seL4_recv in vm_run_arch after getting a handle_async_event@main.c:909 Not IRQ Message: Unknown label (8) which I suspect is a seL4_Fault_VCPUFault from the MCS telling the thread its budget is up, but honestly I don’t have enough experience yet to really know…so its kind of a guess. I put a bunch of prints in there and I know the Linux Kernel is loaded its almost like its getting right up to the entry point and then faulting. Anyways any help anyone can provide would be awesome and thanks in advance for any help!

1 0

Invitation to Attend the 3rd seL4 Summit
by Heiser, Gernot (Data61, Kensington NSW) 15 Oct '20

15 Oct '20

Dear seL4 Community, The 3rd seL4 Summit will take place (virtually) on 15–18 November (US East Coast time). The program features a tutorial and 3 days packed with great talks and panels, see https://na.eventscloud.com/file_uploads/a236a51b4b76609e82fcc316992b73f4_20… Presentations will be streamed according to the schedule and available for download right after, and there will be an on-line discussion forum. Registration is only $80US: https://na.eventscloud.com/ereg/index.php?eventid=579066& Gernot

1 0

Mailing list delivery problems ...
by Chubb, Peter (Data61, Kensington NSW) 14 Oct '20

14 Oct '20

Hi Folks, Some time over the last few weeks, the DNS config on our mail server changed such that we ended with a mail loop. The result is that email sent to the list between September 25 and October 11 may have been lost. So if you sent email to devel(a)sel4.systems during that time, we're not ignoring you -- we never saw the email. Peter C -- Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group CSIRO's Data61

1 0

Userland components in Ring 1/2 (where kernel is in ring 0) to provide protection from less trusted components
by Isaac Beckett 19 Sep '20

19 Sep '20

Hey all, I was wondering if it makes sense for someone building a system on seL4 to run certain drivers or other critical components in a more privileged environment, but still outside the kernel. Does using a different CPU mode in this context make sense? My hunch is that the case is no, because x86 has those extra rings, but ARM only has two modes, Supervisor/System and User mode, which would make it hard to provide any mechanism for the kernel to manage privileged components, because of the differences between platforms.

6 6

capability name change
by Sachin More 17 Sep '20

17 Sep '20

Hi: Between version 9.0.1 and 10.0.0, the capability name seL4_CapIOPort changed to seL4_CapIOPortControl in the file seL4/libsel4/include/sel4/bootinfo_types.h. I have some legacy code written for 9.0.1 that I want to port to 10.0.0. When I changed the occurrences of seL4_CapIOPort to seL4_CapIOPortControl, I am getting the following: Warning: copy: seL4_CNode_Copy (0x7) returned 3 followed some time later by: Warn<<seL4(CPU 0) [decodeInvocation/530 T0xffffff80002de400 "child of: 'child of: 'rootserver''" @20f27a4]: Attempted to invoke a null cap #7.>> What am I doing wrong? thanks in advance, Sachin

2 2

Re: [seL4] Devel Digest, Vol 76, Issue 8
by Chris Koziarz 16 Sep '20

16 Sep '20

Thanks Damon for your help. I've reinstalled Haskell stack this morning> This time I tried fault-handlers tutorial. It appears the reinstall had made the difference as ninja indeed spawned the process: $ stack build --fast and after just a minute or two (yesterday the whole thing was hanging for a good 20-30min before I lost patience), a long log was produced. Among tons of messages, I found this warning: Copied executables to /home/chris/sel4_tutorials/fault-handlers_build/capDL-tool: - parse-capDL Warning: Installation path /home/chris/sel4_tutorials/fault-handlers_build/capDL-tool not found on the PATH environment variable. I hope the warning won't stop me, although I'm curious why capDL wants to live in (and have a path to) a tutorial build directory rather than some common bin dirs like /usr/bin:/snap/bin or such... Thanks again, Chris On Tue, Sep 15, 2020 at 10:53 PM <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: CAmkES Linux VM Tutorial/Minimal Build Issue > (Lee, Damon (Data61, Kensington NSW)) > 2. Re: ADL tool hangs (Lee, Damon (Data61, Kensington NSW)) > 3. capability name change (Sachin More) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 15 Sep 2020 02:16:43 +0000 > From: "Lee, Damon (Data61, Kensington NSW)" > <Damon.Lee(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] CAmkES Linux VM Tutorial/Minimal Build Issue > Message-ID: <tfbr1r3vl6e.fsf(a)coopers.keg.data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi Jim, > > > So there I was having a lovely time doing the seL4 > > Tutorials...and I got > > hit with debug output #1 below, so I confirmed that I indeed had > > nested > > virtualization working by making an running an Ubuntu VM in side > > of an > > Ubuntu VM on an Ubuntu box in using kvm and qemu, so I do not > > think it is > > that. I tried passing the host processor through just to see if > > there > > something was getting in the way to no avail. > > I took a look at the debug output and it looks like there's > something funny > going on with the kernel and the VMM. I was able to replicate your > issue using > the manifest available on GitHub, but it was working fine using > our internal > manifests. So I suspect there were probably fixes that haven't > been propagated > to GitHub yet via our internal CI processes. > > I'll take a look at why our CI haven't propagated changes to > GitHub and in the > meantime, I've created a fork[1] on GitHub of our internal > tutorial manifest so > you can use that instead. > > [1] https://github.com/nomadeel/sel4-tutorials-manifest > > Hope this helps, > Damon > > > ------------------------------ > > Message: 2 > Date: Tue, 15 Sep 2020 02:25:57 +0000 > From: "Lee, Damon (Data61, Kensington NSW)" > <Damon.Lee(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] ADL tool hangs > Message-ID: <tfbo8m7vkr0.fsf(a)coopers.keg.data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi Chris, > > > I have recently messed up my ubuntu host seL4 building machine > > and I had to > > recreate it from scratch. But I have missed something on the > > way. So I have > > a problem building anything that involves Camkes components. It > > appears > > that a tool generating ADL or linking capDL or something along > > is missing > > and results in a hang during building. For example when building > > ipc > > tutorial (for x85 platform): > > > > root@ubuntu:/home/chris/sel4_tutorials/ipc_build# ninja > > [0/8] Generating capDL-tool/parse-capDL^C > > ninja: build stopped: interrupted by user. > > > > Or mcs tutorial: > > > > root@ubuntu:/home/chris/sel4_tutorials/mcs_build# ninja > > [0/8] Generating capDL-tool/parse-capDL^C > > ninja: build stopped: interrupted by user. > > This build step builds the capDL-tools which is written in > Haskell. 'stack' is > the toolchain used to build the capDL-tools and we've seen > examples of it taking > a *very* long time on specific distributions like Ubuntu. To > verify this, > perhaps try `ps aux | grep stack` or similar to see if 'stack' is > being run. > > We do cache the build after the first time it's being run, so > subsequent builds > shouldn't take too long. If this build step doesn't finish even > after waiting > for a long time (30 minutes or so), let us know and we'll be happy > to help. > > Regards, > Damon > > > ------------------------------ > > Message: 3 > Date: Tue, 15 Sep 2020 08:51:15 -0400 > From: Sachin More <sachinsureshmore(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] capability name change > Message-ID: > <CAH36oswCDPRDFeNbgFPVnKvgapFyo= > BbsiNRuf+FjqrBaquegg(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hi: > > Between version 9.0.1 and 10.0.0, the capability name seL4_CapIOPort > changed to seL4_CapIOPortControl in the file > seL4/libsel4/include/sel4/bootinfo_types.h. > I have some legacy code written for 9.0.1 that I want to port to 10.0.0. > When I changed the occurrences of seL4_CapIOPort to seL4_CapIOPortControl, > I am getting the following: > > Warning: copy: seL4_CNode_Copy (0x7) returned 3 > > followed some time later by: > > Warn<<seL4(CPU 0) [decodeInvocation/530 T0xffffff80002de400 "child of: > 'child of: 'rootserver''" @20f27a4]: Attempted to invoke a null cap #7.>> > > What am I doing wrong? > > thanks in advance, > Sachin > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 76, Issue 8 > ************************************ >

2 1

Subject=Re: CAmkES Linux VM Tutorial/Minimal Build Issue
by Jim McColl 16 Sep '20

16 Sep '20

Damon, Too easy, worked on the first go! Thank you for the help! -Jim Evidence: Welcome to Buildroot buildroot login: [ 2.627354] random: fast init done Welcome to Buildroot buildroot login: root Password: # ls -ali total 4 108 drwx------ 2 root root 0 Sep 15 15:20 . 1 drwxrwxr-x 17 root root 0 Jan 8 2020 .. 1114 -rw------- 1 root root 11 Sep 15 15:20 .ash_history #

1 0

ADL tool hangs
by Chris Koziarz 15 Sep '20

15 Sep '20

Hi all, I have recently messed up my ubuntu host seL4 building machine and I had to recreate it from scratch. But I have missed something on the way. So I have a problem building anything that involves Camkes components. It appears that a tool generating ADL or linking capDL or something along is missing and results in a hang during building. For example when building ipc tutorial (for x85 platform): root@ubuntu:/home/chris/sel4_tutorials/ipc_build# ninja [0/8] Generating capDL-tool/parse-capDL^C ninja: build stopped: interrupted by user. Or mcs tutorial: root@ubuntu:/home/chris/sel4_tutorials/mcs_build# ninja [0/8] Generating capDL-tool/parse-capDL^C ninja: build stopped: interrupted by user. Looking into build.ninja script, I think the problem command be this one: build capDL-tool/parse-capDL: CUSTOM_COMMAND COMMAND = cd /home/chris/sel4_tutorials/mcs_build/capDL-tool && printf capDL-tool/parse-capDL:\ > /home/chris/sel4_tutorials/mcs_build/capDL-tool/parse-capDL.d && find -L /home/chris/sel4_tutorials/projects/capdl/capDL-tool/ -type f -printf %p\ >> /home/chris/sel4_tutorials/mcs_build/capDL-tool/parse-capDL.d && cp -a /home/chris/sel4_tutorials/projects/capdl/capDL-tool/* . && /usr/bin/cmake -E env make DESC = Generating capDL-tool/parse-capDL depfile = /home/chris/sel4_tutorials/mcs_build/capDL-tool/parse-capDL.d restat = 1 but I don't know why it would be hanging my build and how I should fix it. Any help greatly appreciated. Chris.

2 1