- Devel - lists.sel4.systems

raspberry pi 4
by Sachin More 31 Oct '20

31 Oct '20

Hi: Has anyone tried to use seL4 on a raspberry pi 4? thanks, Sachin

4 7

Re: [seL4] Devel Digest, Vol 77, Issue 11
by Chris Koziarz 30 Oct '20

30 Oct '20

Thanks Damon for your help! I've added the required "simple" attribute to the assembly configuration: assembly { composition { [...] component Client client; } configuration { [....] client.simple = true; } } But the usage generates: implicit declaration of function ‘camkes_make_simple’ and I don't know what header(s) I should include and/or any library I should link to get ‘camkes_make_simple’ decl/def. camkes_make_simple() function does not exist in any of simple camkes tutorials to figure out the required headers, while your example has too many headers to figure out what headers are really needed. Further help with it is greatly appreciated. Thanks. Chris On Thu, Oct 29, 2020 at 4:36 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. seL4_BootInfo in Camkes environment (Chris Koziarz) > 2. Re: seL4_BootInfo in Camkes environment > (Lee, Damon (Data61, Kensington NSW)) > 3. Re: raspberry pi 4 (Jose A. Pascual) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Thu, 29 Oct 2020 13:39:12 +1100 > From: Chris Koziarz <chris(a)breakawayconsulting.com.au> > To: devel(a)sel4.systems > Subject: [seL4] seL4_BootInfo in Camkes environment > Message-ID: > <CAMuEnL6VH8xYxK9SR64Sc65onK7By= > 66XkiPHhgMzu4rjDgnRg(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > In a regular seL4 PD, I always have seL4_BootInfo available > via platsupport_get_bootinfo(), and all goodies that I can learn from > therein are available. > > But it appears that the camkes components (probably we should talk about > "client components", i.e. the ones with "control;" attribute and an entry > point: int run(void)), > are started as a typical root task, with a call: > void __sel4_start_root(seL4_BootInfo *boot_info) > however boot_info is passed herein as NULL. > At least boot_info appears NULL for me on ARM64. > So, is the access to seL4_BootInfo disallowed in camkes env? Or how can I > access seL4_BootInfo in camkes? > > Chris > > > ------------------------------ > > Message: 2 > Date: Thu, 29 Oct 2020 04:28:56 +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] seL4_BootInfo in Camkes environment > Message-ID: <tfbft5x4pve.fsf(a)coopers.keg.data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi Chris, > > > In a regular seL4 PD, I always have seL4_BootInfo available > > via platsupport_get_bootinfo(), and all goodies that I can learn > > from > > therein are available. > > > > But it appears that the camkes components (probably we should > > talk about > > "client components", i.e. the ones with "control;" attribute and > > an entry > > point: int run(void)), > > are started as a typical root task, with a call: > > void __sel4_start_root(seL4_BootInfo *boot_info) > > however boot_info is passed herein as NULL. > > At least boot_info appears NULL for me on ARM64. > > So, is the access to seL4_BootInfo disallowed in camkes env? Or > > how can I > > access seL4_BootInfo in camkes? > > The bootinfo isn't disallowed in a CAmkES environment but parts of > it > is gutted out (untyped information, IRQ control cap etc.) > depending on > the configuration of the CAmkES application. To access the > bootinfo, > you could append this configuration option for a specific > component in > the "configuration" block in the ".camkes" file of your > application: > > <component_name>.simple = true; > > The simple_t interface which abstracts the bootinfo can then be > grabbed via the 'camkes_make_simple()' function. > > There are examples of the bootinfo usage in our CAmkES VM > repositories > that you can checkout here: > > https://github.com/seL4/camkes-vm/blob/master/components/VM_Arm/src/main.c#… > > Regards, > Damon > > > ------------------------------ > > Message: 3 > Date: Thu, 29 Oct 2020 06:45:16 +0100 > From: "Jose A. Pascual" <joseantonio.pascual(a)ehu.eus> > To: Nick Spinale <Nick.Spinale(a)arm.com> > Cc: Sachin More <sachinsureshmore(a)gmail.com>, "devel(a)sel4.systems" > <devel(a)sel4.systems> > Subject: Re: [seL4] raspberry pi 4 > Message-ID: > <CAK8ti4+QiFTDnBKRfZYWQ-XXAT_= > MnTr_+jHJRfmwZQ-w6W6NA(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hi, > We are also running seL4 on the RPI4 and we managed to run "sel4test" > passing all the tests. > Basically, you can build the sel4test project and execute all the tests > without errors as in the Rpi3. > We are using it in an OS course to build a very simple OS on top of seL4. > I'll try to open a PR in the following days. > Nick, if you don't mind, I'll compare our patch with yours to check if we > are doing everything the same way. > I'll keep you informed. > > Jose (& Mikel) > > > On Thu, Oct 29, 2020 at 1:29 AM Nick Spinale <Nick.Spinale(a)arm.com> wrote: > > > > Can I prepare, say seL4 11.0 and then apply your patches and then > > compile using seL4's build system (or your build system if it is in > public > > domain)? > > > > At the moment, I?m unable to share the rest of the code for this > > particular project. I have, however, published our Raspberry Pi 4-related > > patches to public branches of 'seL4' [1] and ?seL4_tools' [2]. These > > patches, which are the extent of our Raspberry Pi 4-related patches for > > upstream seL4 repositories, only encompasses the bootloader (?elfloader?) > > and the seL4 kernel itself. The projects that you might use for getting > > started, such as ?sel4test? [3], depend on platform support for userland > > libraries such as those found in ?seL4_libs? [4]. > > > > If you decide to add Raspberry Pi 4 support to those userland libraries, > > I?d be happy to help out with that. > > > > > > [1] https://github.com/nspin/seL4/tree/rpi4 > > [2] https://github.com/nspin/seL4_tools/tree/rpi4 > > [3] https://github.com/seL4/sel4test-manifest > > [4] https://github.com/seL4/seL4_libs > > > > > > - - - - > > Nick Spinale (nickspinale.com) > > Arm Research, Cambridge UK > > - - - - > > > > IMPORTANT NOTICE: The contents of this email and any attachments are > > confidential and may also be privileged. If you are not the intended > > recipient, please notify the sender immediately and do not disclose the > > contents to any other person, use it for any purpose, or store or copy > the > > information in any medium. Thank you. > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 77, Issue 11 > ************************************* >

2 2

seL4_BootInfo in Camkes environment
by Chris Koziarz 29 Oct '20

29 Oct '20

In a regular seL4 PD, I always have seL4_BootInfo available via platsupport_get_bootinfo(), and all goodies that I can learn from therein are available. But it appears that the camkes components (probably we should talk about "client components", i.e. the ones with "control;" attribute and an entry point: int run(void)), are started as a typical root task, with a call: void __sel4_start_root(seL4_BootInfo *boot_info) however boot_info is passed herein as NULL. At least boot_info appears NULL for me on ARM64. So, is the access to seL4_BootInfo disallowed in camkes env? Or how can I access seL4_BootInfo in camkes? Chris

2 1

seL4 on gem5
by Bodun Hu 28 Oct '20

28 Oct '20

Hello, I'm currently trying to set up seL4 inside the gem5 simulator to get some benchmark results. Are there any tutorials or instructions regarding how to set it up? Any tip will be appreciated! *Edward Hu* The University of Texas at Austin | Computer Science | Homepage: https:// <http://goog_1605193962>bodunhu.com

2 1

Adding a library to the camkes project
by Chris Koziarz 28 Oct '20

28 Oct '20

Camkes CMakefiles are quite different to the non-camkes ones that I've learned recently. For starters, I cannot figure out a simple step of adding an include path & a static library to a camkes project. For example, I want to expand projects/camkes/apps to include an extra file that calls functions from libsel4vka. Adding a source file is easy: just expand SOURCES list, e.g.: DeclareCAmkESComponent(Driver SOURCES components/Driver/src/driver.c components/Driver/src/sel4vka-caller.c) But sel4vka-caller.c needs the include paths to seL4_libs/libsel4vka/include. And the libsel4vka.a needs to be built and linked to the executable. I don't know how I can achieve it. The CMakefile original (trivial) content is: project(uart C) DeclareCAmkESComponent(Client SOURCES components/Client/src/client.c) DeclareCAmkESComponent(Driver SOURCES components/Driver/src/driver.c) DeclareCAmkESRootserver(uart.camkes) I try to add the libsel4vka.a to the linker via appending to it: target_link_libraries( uart PUBLIC sel4vka ) But I get: /usr/bin/cmake -S/home/chris/camkes_brkwy/projects/camkes -B/home/chris/camkes_brkwy/uart_tqma8xqp-build ninja: error: rebuilding 'build.ninja': subcommand failed chris@ubuntu:~/camkes_brkwy/uart_tqma8xqp-build$ ninja CMake Error at apps/uart/CMakeLists.txt:35 (target_link_libraries): Cannot specify link libraries for target "uart" which is not built by this project. I don't understand why "uart" is not a target, given the statement: project(uart C) So given target_link_libraries() fails me here, what am I doing wrong? what's the proper way of including -I paths and *.a files in Camkes-type CMakefile? Thanks for your help! Chris

2 1

3rd seL4 Summit - Tutorial
by Cedric MAIRE 24 Oct '20

24 Oct '20

Dear seL4 developers, I would be happy to get more information about the presented tutorial during the 3rd seL4 summit. What will it be about? Is this tutorial already available on the website or exclusive to the summit attendees? I looked through the given PDF (https://na.eventscloud.com/file_uploads/a236a51b4b76609e82fcc316992b73f4_20…) but didn't find any information regarding the tutorial. Best regards, Cedric Maire <html xmlns="http://www.w3.org/1999/xhtml"> <head> <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> <STYLE type="text/css">  </STYLE> </head> <body> <hr style="color: #000000;background-color: #000000;height: 1px;"/> <p>The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: <a href="http://www.icrc.org">www.icrc.org</a><p> <p>This e-mail is intended for the named recipient(s) only.<br> Its contents are confidential and may only be retained by the named recipient(s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. </p> <hr style="color: #000000;background-color: #000000;height: 1px;"/> </body> </html>

1 0

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

CAmkES Linux VM Tutorial/Minimal Build Issue
by Jim McColl 15 Sep '20

15 Sep '20

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. That was when I decided to go through the devel archives and the closest similar post I could find was 07 Aug 2020 ( https://sel4.systems/pipermail/devel/2020-August/002845.html) unfortunately there's no debug output so I cannot confirm is it is the same issue. There was also an issue in April ( https://sel4.systems/pipermail/devel/2020-April/002781.html) that also looked similar but I grep'd through the source and could not find the line referenced line from the commit. Finally I natively built minimal from https://github.com/seL4/camkes-vm-examples in the hopes that it was an issue with the tutorial docker container which led to output #2 below. Which brings me to now humbly request for help so I can finish up the tutorials. Thank you advance for any help anyone can provide, hopefully it is a simple mistake on my part. -Jim ====== VERY LONG DEBUG STUFF BELOW ====== - Debug Output #1: ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa1d000 end=0x1e366e0 size=0x14196e0 name='images/capdl-loader-image-x86_64-pc99' 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 7fedf000 type 1 Adding physical memory region 0x100000-0x7ffdf000 Physical Memory Region from 7ffdf000 size 21000 type 2 Physical Memory Region from b0000000 size 10000000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information ACPI: RSDP paddr=0xf68d0 ACPI: RSDP vaddr=0xf68d0 ACPI: RSDT paddr=0x7ffe210d ACPI: RSDT vaddr=0x7ffe210d Kernel loaded to: start=0x100000 end=0xa1c000 size=0x91c000 entry=0x10125e ACPI: RSDT paddr=0x7ffe210d ACPI: RSDT vaddr=0x7ffe210d ACPI: FADT paddr=0x7ffe1ee5 ACPI: FADT vaddr=0x7ffe1ee5 ACPI: FADT flags=0x84a5 ACPI: DMAR paddr=0x7ffe20c5 ACPI: DMAR vaddr=0x7ffe20c5 ACPI: IOMMU host address width: 39 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0x7ffe1fd9 ACPI: MADT vaddr=0x7ffe1fd9 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 ELF-loading userland images from boot modules: size=0x289a000 v_entry=0x4083af v_start=0x400000 v_end=0x2c9a000 p_start=0x1e37000 p_end=0x46d1000 Moving loaded userland images to final location: from=0x1e37000 to=0xa1c000 size=0x289a000 Starting node #0 with APIC ID 0 Mapping kernel window is done vt-x: Load IA32_PERF_GLOBAL_CONTROL not supported. Hardware debugging may not work IOMMU 0x0: 16-bit domain IDs supported IOMMU: Using 3 page-table levels (max. supported:3) IOMMU: Create VTD context table for PCI bus 0x0 (pptr=0xffffff807e01d000) ===== SNIP ====== IOMMU: Create VTD context table for PCI bus 0xfe (pptr=0xffffff807e11b000) IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xffffff807e11c000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] ========== KERNEL EXCEPTION ========== Vector: 0xd ErrCode: 0x0 IP: 0xffffffff8080d2e9 SP: 0xffffffff80a0bd88 FLAGS: 0x10002 CR0: 0x8001003b CR2: 0x0 (page-fault address) CR3: 0xa17000 (page-directory physical address) CR4: 0x2220 Stack Dump: *0xffffffff80a0bd88 == 0xffffff807c052880 *0xffffffff80a0bd90 == 0xffffff80318c1400 *0xffffffff80a0bd98 == 0x1 *0xffffffff80a0bda0 == 0xffffffff80812415 *0xffffffff80a0bda8 == 0xffffff8020001580 *0xffffffff80a0bdb0 == 0x1000ff8029831000 *0xffffffff80a0bdb8 == 0xc *0xffffffff80a0bdc0 == 0xffffffff8081eeb8 *0xffffffff80a0bdc8 == 0xc *0xffffffff80a0bdd0 == 0xffffff8020002560 *0xffffffff80a0bdd8 == 0xffffff8029831000 *0xffffffff80a0bde0 == 0x0 *0xffffffff80a0bde8 == 0x1ffed6 *0xffffffff80a0bdf0 == 0xffffff8029831000 *0xffffffff80a0bdf8 == 0xffffff80318c1c00 *0xffffffff80a0be00 == 0xffffff8020002540 *0xffffffff80a0be08 == 0xffffffff80a0be60 *0xffffffff80a0be10 == 0xffffff8020002540 *0xffffffff80a0be18 == 0xffffff80318c18a0 *0xffffffff80a0be20 == 0xffffff8029831000 Halting... halting... Kernel entry via Syscall, number: 1, Call Cap type: 12, Invocation tag: 54 - Debug Output #2: ===== SNIP: Same as above ===== IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xff10d000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/208 T0xff10e400 "rootserver" @8048495]: Untyped Retype: Insufficient memory (1 * 8388608 bytes needed, 0 bytes available).>> Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] seL4 failed assertion '(cte_t *)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && (cte_t *)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at /home/user/Documents/labs/rr/os/seL4-AUS/camkes_vm_examples/kernel/src/object/cnode.c:428 in function cteInsert halting... Kernel entry via Syscall, number: 1, Call Cap type: 12, Invocation tag: 53

2 1

Unable to setup Camkes VM tutorial
by Chris Koziarz 11 Sep '20

11 Sep '20

There is something wrong with Camkes VM repo or with my Linux machine. I am able to setup repo of other tutorials, i.e. repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest works. However when I continue into Camkes VM: root@ubuntu:~/lv4_repo# mkdir camkes_VM root@ubuntu:~/lv4_repo# cd camkes_VM root@ubuntu:~/lv4_repo/camkes_VM# repo init -u https://github.com/sel4/camkes-vm-examples-manifest.git -b tipc-stage I get the following error: Downloading Repo source from https://gerrit.googlesource.com/git-repo fatal: Cannot get https://gerrit.googlesource.com/git-repo/clone.bundle fatal: error [Errno -3] Temporary failure in name resolution fatal: cloning the git-repo repository failed, will remove '.repo/repo' What might be going wrong? As can be seen, I'm running on ubuntu v20.04 Any help appreciated. Chris

2 1

seL4 Summit 2020 - Call for Presentations *extended* to Sep 15.
by Kuz, Ihor (Data61, Kensington NSW) 10 Sep '20

10 Sep '20

Hi, For people not on the seL4 announce list: the 3rd annual seL4 Summit will be held online on November 15-18, 2020. A call for presentations is out, and the deadline for submissions has been extended to September 15, 2020. Please consider submitting something about seL4-based work that you are doing or other seL4/microkernel/trustworthy systems topics. Submission only requires a title and abstract, so it’s pretty low overhead. Submit by email to Summit2020(a)sel4-us.org. See more detail on the announce list[1]. Ihor. [1] https://sel4.systems/pipermail/announce/2020/000036.html

1 0

CAmkES Linux VM - Networking
by Cedric MAIRE 03 Sep '20

03 Sep '20

Dear seL4 developers, I am running the CAmkES VM examples from `https://github.com/seL4/camkes-vm-examples` and am able to boot the `minimal` example with: ``` $ ../init-build.sh -DSIMULATION=TRUE -DCAMKES_VM_APP=minimal $ ninja $ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic ``` However this example does not provide networking capabilities due to missing drivers (is that correct?). Is there a simple way I may add networking? Simply put I would like the Linux guest to be able to connect to the internet. I tried passing the QEMU parameters to setup a tap interface, which didn't help. I also tried to use the example `cma34cr_centos` which should already provide networking but when I try to boot this example using `qemu-system-x86_64 -m 2048 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic` I get the following error: `create_objects@main.c:794 Ran out of untyped memory while creating objects.`. Full log output in the `.log` file. Thanks in advance, Best regards, Cedric Maire =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

1 0

Running RISC-V sel4 in QEMU/Spike
by Porter, Jeremy 02 Sep '20

02 Sep '20

I'm following the steps to build sel4 for QEMU and Spike here: https://docs.sel4.systems/Hardware/spike.html Spike - seL4 Docs | seL4 docs<https://docs.sel4.systems/Hardware/spike.html> If you plan to use the ./simulate script, please be sure to add the -DSIMULATION=1 argument when running cmake. Generated binaries can be found in the images/ directory.. You can also use run the tests on the 32-bit spike platform by replacing the -DRISCV64=TRUE option with -DRISCV32=TRUE. docs.sel4.systems Since my system doesn't have QEMU 4.2 or better I built the latest version of QEMU and use that instead. I get the following error from QEMU: /mnt/data/qemu/build/riscv64-softmmu/qemu-system-riscv64 -machine spike -nographic -serial mon:stdio -m size=4095M -kernel images/sel4test-driver-image-riscv-spikeqemu-system-riscv64: Unable to load the RISC-V firmware "opensbi-riscv64-spike-fw_jump.elf" In Spike this happens: /mnt/data/rocket-tools/bin/spike images/sel4test-driver-image-riscv-spike bbl loader ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..8064d4d7] Looking for DTB in CPIO archive...found at 802cb1a0. Loaded DTB from 802cb1a0. paddr=[8402a000..8402afff] ELF-loading image 'kernel' paddr=[84000000..84029fff] vaddr=[ffffffff84000000..ffffffff84029fff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' paddr=[8402b000..84401fff] vaddr=[10000..3e6fff] virt_entry=1b540 Jumping to kernel-image entry point... Init local IRQ Initialing PLIC... The tutorials lead me to believe this should go to user space. i.e. 327 printf("Booting all finished, dropped to user space\n"); in kernel/src/arch/riscv/kernel/boot.c Can anyone point out what's going wrong here in these two cases? Thank you! Jeremy

2 1

CAmkES Linux VM - Networking
by Cedric MAIRE 28 Aug '20

28 Aug '20

Dear seL4 developers, I am running the CAmkES VM examples from `https://github.com/seL4/camkes-vm-examples` and am able to boot the `minimal` example with: ``` $ ../init-build.sh -DSIMULATION=TRUE -DCAMKES_VM_APP=minimal $ ninja $ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic ``` However this example does not provide networking capabilities due to missing drivers (is that correct?). Is there a simple way I may add networking? Simply put I would like the Linux guest to be able to connect to the internet. I tried passing the QEMU parameters to setup a tap interface, which didn't help. I also tried to use the example `cma34cr_centos` which should already provide networking but when I try to boot this example using `qemu-system-x86_64 -m 2048 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic` I get the following error: `create_objects@main.c:794 Ran out of untyped memory while creating objects.`. Full log output in the `.log` file. Thanks in advance, Best regards, Cedric Maire =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

1 0

some question about sched_ctrl of mcs答复: some question about mcs
by yadong.li 26 Aug '20

26 Aug '20

Hi Kent： Firstly，thank you for your information. I found the test code call "simple_get_sched_ctrl(&env->simple, 0)" function to get sched_ctrl cap, but I feel confused about env->simple. I have two question about sched_ctrl when I want to add mcs call function for camkes-arm-vm project Background: I try to add get sched_ctrl cap before seL4_TCB_Configure of vm_create_vcpu_arch(projects/seL4_projects_libs/libsel4vm/src/arch/arm/boot.c) 1. I try use "simple_get_sched_ctrl(vm->simple, affinity);" or " simple_default_init_bootinfo(&simple, platsupport_get_bootinfo()) simple_get_sched_ctrl(simple, affinity);" But they all failed What "simple" should I used to get sched_ctl in this project. 2. I found camkes_simple_sched_ctrl in component.simple.c generate C code, have below code: /*- if 'sched_ctrl' in configuration[me.name].keys() -*/ But I did not found camkes configurations have "sched_ctrl" field in project or your examples in CAmkES Thank you very much -----邮件原件----- 发件人: Kent Mcleod [mailto:kent.mcleod72@gmail.com] 发送时间: 2020年8月25日 10:37 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] some question about mcs > > Hi, > 1.Did seL4-11.0.0<https://docs.sel4.systems/releases/sel4/11.0.0> support mcs, I found some CONFIG_KERNEL_MCS in this release version ? or must use seL4 10.1.1-mcs <https://docs.sel4.systems/releases/sel4/10.1.1-mcs.html> branch? > 2'Where I can find some example about mcs in project? The introduction of Wiki is too simple , I can 't make the param of seL4_SchedControl_Configure is correct? > > Thank you very much 11.0.0 does introduce a config option CONFIG_KERNEL_MCS (KernelIsMCS in CMake). You could start with the MCS tutorial: https://docs.sel4.systems/Tutorials/mcs.html. Alternatively, there are MCS tests in seL4test: https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… or examples in CAmkES: - https://github.com/seL4/camkes/tree/master/apps/cms-donate - https://github.com/seL4/camkes/tree/master/apps/cs-donate - https://github.com/seL4/camkes/tree/master/apps/cs-nodonate - https://github.com/seL4/camkes/tree/master/apps/periodic - https://github.com/seL4/camkes/tree/master/apps/event-driven - https://github.com/seL4/camkes/tree/master/apps/mcs-donate - https://github.com/seL4/camkes/tree/master/apps/mcs-nodonate I'm not aware if there is any documentation about the CAmkES app examples, but I believe they are supposed to demonstrate different scheduling scenarios using MCS. > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

"Ran out of untyped memory"
by Michael Neises 26 Aug '20

26 Aug '20

Hello, I'm trying to build a camkes app, but when I attempt to run it on an Odroid-xu4, I get the following error just before the boot halts: "Ran out of untyped memory while creating objects" I've narrowed the error down to two calls to a this function: https://github.com/SEL4PROJ/camkes-vm-linux/blob/dc354df3222766b9d366725751… When I use only one call, the image boots nicely. If I use both calls, I get the above error. My understanding is that this function simply adds an executable to the filesystem, so I'm not sure how to begin debugging this. Is it possible that the filesystem is actually "too big" for sel4 to boot successfully? Please advise! Best, Michael Neises

3 4

some question about mcs
by yadong.li 25 Aug '20

25 Aug '20

Hi, 1.Did seL4-11.0.0<https://docs.sel4.systems/releases/sel4/11.0.0> support mcs, I found some CONFIG_KERNEL_MCS in this release version ? or must use seL4 10.1.1-mcs <https://docs.sel4.systems/releases/sel4/10.1.1-mcs.html> branch? 2'Where I can find some example about mcs in project? The introduction of Wiki is too simple , I can 't make the param of seL4_SchedControl_Configure is correct? Thank you very much

2 1

Trouble getting a custom kernel to boot under sel4 on a tk1 board
by Travis Wheatley 25 Aug '20

25 Aug '20

I am having difficulty getting a custom kernel to boot under sel4 on a tk1 board. I have no problems building and booting an image that uses the pre-built linux-tk1-initrd file found in the projects/vm/linux folder. Howoever, when I build a “custom” kernel using buildroot-2016.08.1 as specified in this<https://docs.sel4.systems/projects/camkes-arm-vm/> the boot process hangs shortly after it loads the dtb. <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffc2d400 "rootserver" @106f0]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:605 module name: map_frame_hack install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:605 module name: plat I am using the buildroot_tk1_initrd_defconfig file, also located in the projects/vm/linux folder. I am simply replacing the linux-tk1-initrd file in projects/vm/linux with the image file that gets created in the buildroot-2016.08.1/output/build/linux-custom/arch/arm/boot folder. I then clean my build directory and do the requisite “../init-build.sh -DPLATFORM=tk1 -DCAMKES_VM_APP=vm_minimal” followed by “ninja”. I then put the capdl-loader-image-arm-tk1 file on an SD card, put it in the Tk1 and do: “fatload mmc 1 0x82000000 <filename>” followed by “bootefi 0x82000000” Assuming the guidance on buildroot and the defconfig supplied match what was used to create the working pre-built linux-tk1-initrd kernel the “custom” kernel I built should be very similar. So, what am I missing? Why would a custom kernel hang at the above mentioned point in the boot process?

1 0

Porting Sel4 with RPi 3B+
by 萧琒 21 Aug '20

21 Aug '20

Hi, Professional Devel Support of Sel4, We are porting Sel4 with RPi 3B+, but we fail to boot RPi 3B+ with Sel4 successfully. We cann't find the problem, please help us. we follow the Steps: 1. Use Raspberry Pi Imager v1.4 to burn the operation system (Raspberry Pi OS Lite 32bit) on SD card, and it works well with hardware of RPi 3B+. 2. Build Sel4test-manifest: 2.1 clone the repo of https://github.com/seL4/sel4test-manifest.git 2.2 build image with ../init-build.sh -DPLATFORM=rpi3 -DAARCH32=1 2.3 the image file (sel4test-driver-image-arm-bcm2837) is produced successfully. 3. Following the SD card setup, Copy the following files to root direcctory of SD. 3.1 sel4test-driver-image-arm-bcm2837 3.2 bootcode.bin and start.elf from https://github.com/raspberrypi/firmware/tree/master/boot 3.3 u-boot.bin downloaded from https://sel4.systems/Info/Docs/u-boot-working-rpi3-32bit-v2017.11.bin 3.4 Add enable_uart=1 and kernel=u-boot.bin to the bottom of config.txt 3.5 uboot.env, we fail to find the file, so we don't use the file. if you know the step to produce uboot.env, please lead us. 4. Re-insert SD into the RPi3B+, and power the RPi3B+ on, the RPi3B+ shows the U-Boot successfully. 4.1 sel4test-driver-image-arm-bcm2837 image file’s name printed out with the command of "fatls mmc 0" 4.2 fatload the image with command of "fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2837", the result: reading sel4test-driver-image-arm-bcm2837 4791000 bytes read in 406 ms (11.3 MiB/s) 4.3 bootelf 0x10000000, the result: CACHE: Misaligned operation at range [0082a000, 0082a034] CACHE: Misaligned operation at range [0082b000, 00834fcc] CACHE: Misaligned operation at range [00834fcc, 00835b07] CACHE: Misaligned operation at range [00c9be40, 00c9be9c] CACHE: Misaligned operation at range [00c9be9c, 00c9bec8] ## Starting application at 0x0082a000 ... Then, RPi3B+ is blocked and without anything else to display ! ---- Thanks, Alen 肖月振（萧琒）阿里云事业群-IOT事业部-飞天六十四部电话：13391191786 邮箱：yuezhen.xyz(a)alibaba-inc.com

2 1

Re: [seL4] Devel Digest, Vol 75, Issue 8
by Cedric MAIRE 19 Aug '20

19 Aug '20

Hi Luke, Thanks for your help! I just tried out your solution and get back the following error: `groupmod: GID '1000' already exists`. Here is the workflow that I follow: ``` $ git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git $ cd ~/sel4/seL4-CAmkES-L4v-dockerfiles/ $ git pull # Make sure to be up-to-date. $ git checkout fix_rust $ git pull # Make sure to be up-to-date. `fix_rust` is ahead of `master` so no missing commits. $ ./build.sh -p -b camkes -s rust $ make user CAMKES_IMG=camkes-rust HOST_DIR="~/sel4/" ``` I attached a more detailed log of the error I get. The command throwing this is (full command in log file): `/bin/sh -c groupadd -fg ${GID} ${GROUP} [...] && chmod -R ug+rw /home/${UNAME}` Does this look familiar to you? Best, Cedric -----Original Message----- From: Devel <devel-bounces(a)sel4.systems> On Behalf Of devel-request(a)sel4.systems Sent: samedi, 15 août 2020 04:00 To: devel(a)sel4.systems Subject: Devel Digest, Vol 75, Issue 8 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?mc_phishing_protection_id=28047-b… 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: Dockerfiles - "camkes-rust" Image (Mondy, Luke (Data61, Kensington NSW)) ---------------------------------------------------------------------- Message: 1 Date: Fri, 14 Aug 2020 06:29:32 +0000 From: "Mondy, Luke (Data61, Kensington NSW)" <Luke.Mondy(a)data61.csiro.au> To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] Dockerfiles - "camkes-rust" Image Message-ID: <SYAPR01MB25284E1D39674828FDC11EBED5400(a)SYAPR01MB2528.ausprd01.prod.outlook.com> Content-Type: text/plain; charset="us-ascii" Hello Cedric, Thanks for the report. I believe the best way to use the camkes-rust image is to run this: make user CAMKES_IMG=camkes-rust However, in saying that, it unfortunately does not perform quite as hoped. Because of the way the code is built, it ends up putting the Cargo/Rust content into /root/.cargo, which is inaccessible to you as a non-root user. This is an oversight on my part, as unfortunately these interactive bits of the Dockerfile system don't get tested automatically. I've made a PR on GitHub, which shows the fixes needed: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles/pull/24 Note that the master branch has also been recently updated, so you may need to pick further commits from there (or simply pull them all down first) for things to work. Let me know if that helps. Cheers, Luke -- Dr Luke Mondy, Systems Administrator, P +61 2 9490 5773 | https://ts.data61.csiro.au/?mc_phishing_protection_id=28047-bsrk3aadu815grd… Trustworthy Systems | DATA61 | CSIRO CSIRO Staff Association Delegate Hours at CSIRO Monday: 9:00am to 5pm Tues, Wed, Fri: 1:30pm to 5pm ________________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Cedric MAIRE <cmaire(a)icrc.org> Sent: Friday, 14 August 2020 2:42 AM To: devel(a)sel4.systems Subject: [seL4] Dockerfiles - "camkes-rust" Image Dear seL4 developers, I am using the provided dockerfiles repository to build the docker images in order to compile seL4. I would like to add a rust compiler to my docker image, which I do with "./build.sh -p -b camkes -s rust". This builds an image tagged "trustworthysystems/camkes-rust". I would like to launch this image in a container using the "Makefile" as I would do for the "trustworthysystems/camkes" image (using "make user"). I tried adding targets to the "Makefile" file changing the "USER_BASE_IMG" variable to use "trustworthysystems/camkes-rust" instead of "trustworthysystems/camkes", without success. I also tried to force the image by renaming/retagging "trustworthysystems/camkes " to "trustworthysystems/camkes-old" and "trustworthysystems/camkes-rust" to "trustworthysystems/camkes ". I also forced every base image to be the one containing the Rust compiler (in "Makefile"). All without success. For some reason "trustworthysystems/camkes-rust" image is never used. If I start it manually using docker commands I am able to launch and attach to it, getting the expected Rust compiler. Through the "Makefile" it ever only uses "trustworthysystems/camkes" without the Rust compiler. Is there an easy way to get this to work? What am I missing? Best regards, Cedric =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. =============================================================================== _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… ------------------------------ End of Devel Digest, Vol 75, Issue 8 ************************************ =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 1

Dockerfiles - "camkes-rust" Image
by Cedric MAIRE 14 Aug '20

14 Aug '20

Dear seL4 developers, I am using the provided dockerfiles repository to build the docker images in order to compile seL4. I would like to add a rust compiler to my docker image, which I do with "./build.sh -p -b camkes -s rust". This builds an image tagged "trustworthysystems/camkes-rust". I would like to launch this image in a container using the "Makefile" as I would do for the "trustworthysystems/camkes" image (using "make user"). I tried adding targets to the "Makefile" file changing the "USER_BASE_IMG" variable to use "trustworthysystems/camkes-rust" instead of "trustworthysystems/camkes", without success. I also tried to force the image by renaming/retagging "trustworthysystems/camkes " to "trustworthysystems/camkes-old" and "trustworthysystems/camkes-rust" to "trustworthysystems/camkes ". I also forced every base image to be the one containing the Rust compiler (in "Makefile"). All without success. For some reason "trustworthysystems/camkes-rust" image is never used. If I start it manually using docker commands I am able to launch and attach to it, getting the expected Rust compiler. Through the "Makefile" it ever only uses "trustworthysystems/camkes" without the Rust compiler. Is there an easy way to get this to work? What am I missing? Best regards, Cedric =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 1

QEMU, seL4, CAmkES and Linux VM - Insufficient Memory
by Cedric MAIRE 14 Aug '20

14 Aug '20

Dear seL4 developers, I am trying to setup a stack of QEMU, seL4, CAmkES and a Linux VM. I am following the tutorial on "https://docs.sel4.systems/Tutorials/camkes-vm-linux.html" and also the example on "https://github.com/seL4/camkes-vm-examples". I am running in different errors depending on which path I follow. The machine is an old MacBook Pro (running Linux, exact specs are in the main log file). - Main log file: "intel.log", contains steps and workflows - Tests: All tests seem to pass. - CAmkES VM - Tutorial Version: doesn't start QEMU because of unsupported host flags (warnings) or some failing script - CAmkES VM - Example Version: seems to boot into seL4 or even the Linux VM, but fails because of some memory error Does this look familiar to you? Best regards, Cedric Maire =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 2

Hins for an seL4 virtio pci driver?
by Radev, Martin 10 Aug '20

10 Aug '20

Hello seL4 community, I am currently examining the possibility of using seL4 in a VM and writing a virtio driver to communicate with a virtio pci device in the HV. I looked around the available seL4 projects, and I noticed that there is the `libvirtqueue` and `libpci` projects which should come handy. However, I haven't been able to to find any other project which uses either of the libraries and I haven't found any tests for the two projects. Can you point me to projects which use these two libraries? Kind regards, Martin

2 1

SeL4 Raspberry Pi -- QEMU support
by Brendan Morgenstern 08 Aug '20

08 Aug '20

Hello, I hope all is well. I am interested in running seL4 on the Raspberry Pi, and have been following this guide<https://research.csiro.au/tsblog/sel4-raspberry-pi-3/>. I have followed the instructions and am able to generate an seL4 image correctly, however the guide is geared towards running on hardware and in fact when I run the resulting 'simulate' script I get the following. "Unsupported platform or architecture for simulation". I can run it manually under qemu to an extent with raspi2 as a machine type (): qemu-system-arm -serial null -serial mon:stdio -nographic -M raspi2 -kernel sel4test-driver-image-arm-bcm2837 And it produces this output<https://pastebin.com/LLuum55T>. It seems the image can be *run*, but it doesn't seem to work; it gets stuck on the TIMER0001 test and the previous tests produce errors. It seems that qemu can't quite emulate the raspberry pi hardware. Is there a way to run the seL4 image on the Raspberry Pi in QEMU, or can you provide an alternative for emulation, or any help whatsoever on this matter? Thank you for your time, Brendan Morgenstern ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 2

Re: [seL4] [seL4 Announce] UNSW seL4 teaching videos available
by Heiser, Gernot (Data61, Kensington NSW) 02 Aug '20

02 Aug '20

I’ve (almost) finished teaching and all seL4-related videos from my Advanced OS course are now up on YouTube, details below. Gernot > On 2 Jun 2020, at 10:50, Announcements about seL4 -- low volume list <announce(a)sel4.systems> wrote: > > Dear seL4 community, > > I’m pleased to announce yet another contribution of UNSW Sydney to the seL4 community: This year I’m making the seL4-related videos from my UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel: https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV > > At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. > > The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site: https://www.cse.unsw.edu.au/~cs9242/current/ > > Enjoy, > Gernot

1 0

help with tutorial
by Sachin More 03 Jul '20

03 Jul '20

Hi: I am new to L4 and have been working through the tutorials. However, I am having a problem doing the hello-camkes-0 tutorial. When I try to install the tutorial, I get the output below. Looks like a file hello-camkes-0_build/camkes_gen/deps_1 is not there. Any help would be greatly appreciated! thanks, Sachin $ ./init --tut hello-camkes-0 loading initial cache file ../projects/sel4-tutorials/settings.cmake -- Found capdl: /compile/sel4-tutorials-manifest/projects/capdl CMake Warning (dev) at /usr/share/cmake3/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (camkes-tool) does not match the name of the calling package (sel4-tutorials). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:67 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/settings.cmake:96 (find_package) This warning is for project developers. Use -Wno-dev to suppress it. -- Found camkes-tool: /compile/sel4-tutorials-manifest/projects/sel4-tutorials CMake Warning (dev) at /usr/share/cmake3/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (camkes-tool) does not match the name of the calling package (sel4-tutorials). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:67 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/settings.cmake:96 (find_package) CMakeLists.txt:3 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- The C compiler identification is GNU 7.3.1 -- The ASM compiler identification is GNU -- Found assembler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- 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 -- Found camkes-tool: /compile/sel4-tutorials-manifest/projects/camkes-tool -- Found seL4: /compile/sel4-tutorials-manifest/kernel -- Found elfloader-tool: /compile/sel4-tutorials-manifest/tools/seL4/elfloader-tool -- Found musllibc: /compile/sel4-tutorials-manifest/projects/musllibc -- Found util_libs: /compile/sel4-tutorials-manifest/projects/util_libs -- Found seL4_libs: /compile/sel4-tutorials-manifest/projects/seL4_libs -- Found projects_libs: /compile/sel4-tutorials-manifest/projects/projects_libs -- Detecting cached version of: capDL-tool -- No cache path given. Set SEL4_CACHE_DIR to a path to enable caching binary artifacts. -- Found sel4runtime: /compile/sel4-tutorials-manifest/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Detecting cached version of: musllibc -- No cache path given. Set SEL4_CACHE_DIR to a path to enable caching binary artifacts. -- /compile/sel4-tutorials-manifest/hello-camkes-0_build/ast.pickle is out of date. Regenerating... -- /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes-gen.cmake is out of date. Regenerating... CAmkES uses UTF-8 encoding, but your locale's preferred encoding is ansi_x3.4-1968. You can override your locale with the LANG environment variable. CMake Error at /compile/sel4-tutorials-manifest/tools/seL4/cmake-tool/helpers/make.cmake:13 (file): file failed to open for reading (No such file or directory): /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes_gen/deps_1 Call Stack (most recent call first): /compile/sel4-tutorials-manifest/tools/seL4/cmake-tool/helpers/make.cmake:71 (MakefileDepsToList) /compile/sel4-tutorials-manifest/projects/camkes-tool/camkes.cmake:503 (execute_process_with_stale_check) CMakeLists.txt:17 (GenerateCAmkESRootserver) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:29 (include) CMakeLists.txt:4 (sel4_tutorials_regenerate_tutorial) CMake Error at /compile/sel4-tutorials-manifest/projects/camkes-tool/camkes.cmake:523 (message): Failed to generate /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes-gen.cmake Call Stack (most recent call first): CMakeLists.txt:17 (GenerateCAmkESRootserver) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:29 (include) CMakeLists.txt:4 (sel4_tutorials_regenerate_tutorial) -- Configuring incomplete, errors occurred! See also "/compile/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/compile/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 106, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/compile/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 74, in _init_build_directory return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, _err=output) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 1549, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 793, in __init__ self.wait() File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 849, in wait self.handle_command_exit_code(exit_code) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 877, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../projects/sel4-tutorials/settings.cmake /compile/sel4-tutorials-manifest/hello-camkes-0 STDOUT: STDERR:

2 2

Confirming correct syntax of items in devices.camkes.
by Travis Wheatley 02 Jul '20

02 Jul '20

I have been attempting to add support for both USB and SD persistent memory to my vm (See "Re: ramdisk vs. persistant rfs in VMs.” thread.). I seem to be having a problem with power management. In hopes of correcting this I wish to expose the power management unit to the VM. The related stanza looks like this in my device tree file. cci@fd6e0000 { compatible = "arm,cci-400"; reg = <0x0 0xfd6e0000 0x0 0x9000>; ranges = <0x0 0x0 0xfd6e0000 0x10000>; #address-cells = <0x1>; #size-cells = <0x1>; pmu@9000 { compatible = "arm,cci-400-pmu,r1"; reg = <0x9000 0x5000>; interrupt-parent = <0x4>; interrupts = <0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4>; }; }; The PMU appears to be a child of cci. I am unsure of the proper syntax to use in my devices.camkes file. Since it is a child does one specify the path as /cci/pmu? Does the parent also have to be exposed to the vm? Here is what the related lines inmy devices.camkes look like. Is this correct? vm0.dtb = dtb([ {"path": "/cci@fd6e0000"}, {"path": "/cci/pmu@9000"},

1 0

Re: [seL4] ramdisk vs. persistant rfs in VMs.
by Zhuang, Siwei (Data61, Kensington NSW) 27 Jun '20

27 Jun '20

Hi Travis, It looks like the issue is related to the power management. You may need to read the board's manual(e.g UG1085) to find out if USB and SDHCI rely on any other devices which you also need to pass through to your Linux VM. You may also try to recompile your Linux kernel with PM disabled. If it doesn't work for you, then you'll have to debug your Linux kernel to find the root cause of the error. Good Luck. - Siwei ________________________________________ From: Travis Wheatley <travis.wheatley(a)emergentspace.com> Sent: Friday, 26 June 2020 6:25 AM To: devel(a)sel4.systems Cc: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: ramdisk vs. persistant rfs in VMs. I have made some good progress thanks to Siwei’s advice. I have modified my .dts file and have made a usb controller as well as the sdhci controller available to the VM. However, there still seems to be some issues at start up. Here is what dmesg has to say about the usb controller(s) root@xilinx-zcu102-2019_1:~# dmesg | grep usb [ 1.754678] usbcore: registered new interface driver usbfs [ 1.761934] usbcore: registered new interface driver hub [ 1.768958] usbcore: registered new device driver usb [ 3.827826] usbcore: registered new interface driver asix [ 3.834976] usbcore: registered new interface driver ax88179_178a [ 3.842998] usbcore: registered new interface driver cdc_ether [ 3.850682] usbcore: registered new interface driver net1080 [ 3.858146] usbcore: registered new interface driver cdc_subset [ 3.865948] usbcore: registered new interface driver zaurus [ 3.873301] usbcore: registered new interface driver cdc_ncm [ 3.895799] usbcore: registered new interface driver uas [ 3.902820] usbcore: registered new interface driver usb-storage [ 3.916716] usbcore: registered new interface driver uvcvideo [ 3.991358] usbcore: registered new interface driver bcm203x [ 3.998824] usbcore: registered new interface driver bpa10x [ 4.006182] usbcore: registered new interface driver bfusb [ 4.013424] usbcore: registered new interface driver btusb [ 4.028142] usbcore: registered new interface driver ath3k [ 4.201363] usbcore: registered new interface driver usbhid [ 4.208699] usbhid: USB HID core driver [ 4.224831] usbcore: registered new interface driver snd-usb-audio [ 5.181742] dwc3-of-simple ff9e0000.usb1: failed to add to PM domain domain3: -13 [ 5.191629] dwc3-of-simple: probe of ff9e0000.usb1 failed with error -13 Any clue? Regarding the SD card, it is partitioned with a boot partition where uboot and the .elf file live and the remainder is the free space I hope to use as the filesystem. Here is what dmesg has to say about the sdhc interface. root@xilinx-zcu102-2019_1:~# dmesg | grep sdhc [ 4.049894] sdhci: Secure Digital Host Controller Interface driver [ 4.058026] sdhci: Copyright(c) Pierre Ossman [ 4.063768] sdhci-pltfm: SDHCI platform and OF driver helper [ 5.209925] sdhci-arasan ff160000.mmc: failed to add to PM domain domain4: -13 [ 5.219468] sdhci-arasan: probe of ff160000.mmc failed with error -13 [ 5.351710] mmc0: sdhci: ============ SDHCI REGISTER DUMP =========== [ 5.360229] mmc0: sdhci: Sys addr: 0x00000000 | Version: 0x00000000 [ 5.368759] mmc0: sdhci: Blk size: 0x00000000 | Blk cnt: 0x00000000 [ 5.377280] mmc0: sdhci: Argument: 0x00000000 | Trn mode: 0x00000000 [ 290.055387] random: fast init done [ 5.385810] mmc0: sdhci: Present: 0x00000000 | Host ctl: 0x00000000 [ 5.394331] mmc0: sdhci: Power: 0x00000000 | Blk gap: 0x00000000 [ 5.402860] mmc0: sdhci: Wake-up: 0x00000000 | Clock: 0x00000000 [ 5.411381] mmc0: sdhci: Timeout: 0x00000000 | Int stat: 0x00000000 [ 5.419902] mmc0: sdhci: Int enab: 0x00000000 | Sig enab: 0x00000000 [ 5.428441] mmc0: sdhci: AC12 err: 0x00000000 | Slot int: 0x00000000 [ 5.436962] mmc0: sdhci: Caps: 0x00000000 | Caps_1: 0x00000000 [ 5.445491] mmc0: sdhci: Cmd: 0x00000000 | Max curr: 0x00000000 [ 5.454021] mmc0: sdhci: Resp[0]: 0x00000000 | Resp[1]: 0x00000000 [ 5.462551] mmc0: sdhci: Resp[2]: 0x00000000 | Resp[3]: 0x00000000 [ 5.471089] mmc0: sdhci: Host ctl2: 0x00000000 [ 5.477023] mmc0: sdhci: ============================================ Seems to be getting the same -13 error when setting up it’s domain. So… what do I need to do to make these devices accessible from the linux command line? On Jun 24, 2020, at 8:58 PM, Zhuang, Siwei (Data61, Kensington NSW) <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Travis, The addresses are board specific. The document for your board is UG1085, https://www.xilinx.com/support/documentation/user_guides/ug1085-zynq-ultras… If all you need is a number, you can also find it in the dts files in u-boot, Linux kernel or seL4, https://github.com/seL4/seL4/blob/master/tools/dts/zynqmp.dts#L900, #L910 - Siwei ________________________________________ From: Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>> Sent: Thursday, 25 June 2020 5:49 AM To: devel(a)sel4.systems<mailto:devel@sel4.systems> Cc: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: ramdisk vs. persistant rfs in VMs. Thanks Siwei. This was very helpful. I do have a follow up question about the addresses used in the devices.camkes file. Are these board specific or standard locations for the microkernel? The board I am using is a zcu102. Not sure where/how to find the appropriate address to use for the sdhci device. — Travis On Jun 23, 2020, at 3:54 AM, Zhuang, Siwei (Data61, Kensington NSW) <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Travis, If you only need one VM to access the SD card. You could pass-through the SD card controller to Linux, recompile the Linux kernel with the proper driver. Then passing your rootfs on SD card via Linux kernel boot parameters. An example can be found in the "camkes-arm-vm" repo. Have a read about the "TK1 configuration" on this page, https://docs.sel4.systems/projects/camkes-arm-vm/ The configuration code can be found here, https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/apps/vm_minimal/tk1/d… https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/apps/vm_minimal/tk1/d… If you need to share the SD card between an native seL4 application and a VM or among multiple VMs, you'll need a virtual SD card driver. We only have a virtual USB driver at the moment. Use it as a reference to make your virtual driver. The code can be found here, https://github.com/SEL4PROJ/seL4_projects_libs/blob/master/libsel4vmmplatsu… https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/mod… You can of course partition the SD card, if your board supports boot from SD card. Consult the board's manual regarding how to boot from SD card. Note that, the Linux VM would have the access to your boot partition, hence the seL4 boot image could be compromised. To avoid that, you'll need to intercept the SD card access from the VM. The code here demonstrates one way of doing it, https://github.com/SEL4PROJ/seL4_projects_libs/blob/master/libsel4vmmplatsu… Hope these helps. - Siwei ________________________________________ From: Devel <devel-bounces(a)sel4.systems<mailto:devel-bounces@sel4.systems>> on behalf of Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>> Sent: Tuesday, 23 June 2020 6:47 AM To: devel(a)sel4.systems<mailto:devel@sel4.systems> Subject: [seL4] ramdisk vs. persistant rfs in VMs. I’ve been working with VMs running under SEL4 on ARM hardware. I have been able to boot to a command prompt in a VM. However, the filesystem being used is a ramdisk. I need some sort of persistent storage, preferably a regular rfs that lives on an SD card. Not exactly sure what modifications to make and where to cause the kernel to use a persistent rfs rather than the ramdisk. Barring that, wondering if the SD card can be divided into multiple partitions such that one can be the boot partition and the other mounted to provide persistent storage space. Hoping one of y’all can point me in the right direction. — Travis _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel

1 0

Re: [seL4] ramdisk vs. persistant rfs in VMs.
by Travis Wheatley 27 Jun '20

27 Jun '20

I have made some good progress thanks to Siwei’s advice. I have modified my .dts file and have made a usb controller as well as the sdhci controller available to the VM. However, there still seems to be some issues at start up. Here is what dmesg has to say about the usb controller(s) root@xilinx-zcu102-2019_1:~# dmesg | grep usb [ 1.754678] usbcore: registered new interface driver usbfs [ 1.761934] usbcore: registered new interface driver hub [ 1.768958] usbcore: registered new device driver usb [ 3.827826] usbcore: registered new interface driver asix [ 3.834976] usbcore: registered new interface driver ax88179_178a [ 3.842998] usbcore: registered new interface driver cdc_ether [ 3.850682] usbcore: registered new interface driver net1080 [ 3.858146] usbcore: registered new interface driver cdc_subset [ 3.865948] usbcore: registered new interface driver zaurus [ 3.873301] usbcore: registered new interface driver cdc_ncm [ 3.895799] usbcore: registered new interface driver uas [ 3.902820] usbcore: registered new interface driver usb-storage [ 3.916716] usbcore: registered new interface driver uvcvideo [ 3.991358] usbcore: registered new interface driver bcm203x [ 3.998824] usbcore: registered new interface driver bpa10x [ 4.006182] usbcore: registered new interface driver bfusb [ 4.013424] usbcore: registered new interface driver btusb [ 4.028142] usbcore: registered new interface driver ath3k [ 4.201363] usbcore: registered new interface driver usbhid [ 4.208699] usbhid: USB HID core driver [ 4.224831] usbcore: registered new interface driver snd-usb-audio [ 5.181742] dwc3-of-simple ff9e0000.usb1: failed to add to PM domain domain3: -13 [ 5.191629] dwc3-of-simple: probe of ff9e0000.usb1 failed with error -13 Any clue? Regarding the SD card, it is partitioned with a boot partition where uboot and the .elf file live and the remainder is the free space I hope to use as the filesystem. Here is what dmesg has to say about the sdhc interface. root@xilinx-zcu102-2019_1:~# dmesg | grep sdhc [ 4.049894] sdhci: Secure Digital Host Controller Interface driver [ 4.058026] sdhci: Copyright(c) Pierre Ossman [ 4.063768] sdhci-pltfm: SDHCI platform and OF driver helper [ 5.209925] sdhci-arasan ff160000.mmc: failed to add to PM domain domain4: -13 [ 5.219468] sdhci-arasan: probe of ff160000.mmc failed with error -13 [ 5.351710] mmc0: sdhci: ============ SDHCI REGISTER DUMP =========== [ 5.360229] mmc0: sdhci: Sys addr: 0x00000000 | Version: 0x00000000 [ 5.368759] mmc0: sdhci: Blk size: 0x00000000 | Blk cnt: 0x00000000 [ 5.377280] mmc0: sdhci: Argument: 0x00000000 | Trn mode: 0x00000000 [ 290.055387] random: fast init done [ 5.385810] mmc0: sdhci: Present: 0x00000000 | Host ctl: 0x00000000 [ 5.394331] mmc0: sdhci: Power: 0x00000000 | Blk gap: 0x00000000 [ 5.402860] mmc0: sdhci: Wake-up: 0x00000000 | Clock: 0x00000000 [ 5.411381] mmc0: sdhci: Timeout: 0x00000000 | Int stat: 0x00000000 [ 5.419902] mmc0: sdhci: Int enab: 0x00000000 | Sig enab: 0x00000000 [ 5.428441] mmc0: sdhci: AC12 err: 0x00000000 | Slot int: 0x00000000 [ 5.436962] mmc0: sdhci: Caps: 0x00000000 | Caps_1: 0x00000000 [ 5.445491] mmc0: sdhci: Cmd: 0x00000000 | Max curr: 0x00000000 [ 5.454021] mmc0: sdhci: Resp[0]: 0x00000000 | Resp[1]: 0x00000000 [ 5.462551] mmc0: sdhci: Resp[2]: 0x00000000 | Resp[3]: 0x00000000 [ 5.471089] mmc0: sdhci: Host ctl2: 0x00000000 [ 5.477023] mmc0: sdhci: ============================================ Seems to be getting the same -13 error when setting up it’s domain. So… what do I need to do to make these devices accessible from the linux command line?

1 0

ramdisk vs. persistant rfs in VMs.
by Travis Wheatley 25 Jun '20

25 Jun '20

I’ve been working with VMs running under SEL4 on ARM hardware. I have been able to boot to a command prompt in a VM. However, the filesystem being used is a ramdisk. I need some sort of persistent storage, preferably a regular rfs that lives on an SD card. Not exactly sure what modifications to make and where to cause the kernel to use a persistent rfs rather than the ramdisk. Barring that, wondering if the SD card can be divided into multiple partitions such that one can be the boot partition and the other mounted to provide persistent storage space. Hoping one of y’all can point me in the right direction. — Travis

2 3

CAmkES VM rootfs.cpio with Python3 Causes Error
by Turner, Ben 12 Jun '20

12 Jun '20

Hi, I have been attempting to create a VM to run as a CAmkES component, and it is a requirement that it has Python3. I have been using the vm_minimal app as a template to get started, and was successful at getting my own buildroot filesystem image running, however when I attempted to add the Python3 package, the resulting image resulted in the following error when it booted: ... <<seL4(CPU 0) [decodeInvocation/631 T0xfec34400 "rootserver" @106f0]: Attempted to invoke a null cap> create_objects@main.c:805 [Err seL4_InvalidCapability]: Untyped retype failed with unexpected error seL4 root server abort()ed Debug halt syscall from user thread 0xfec34400 "rootserver" halting... Kernel entry via Unknown syscall, word: 1 The only change I made to the image was to add the Python3 package, and that has caused this error. Is there something the vm_minimal app is missing that is required in order to get Python3 working? Kind regards, Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 5

camkes-vm-linux tutorial issue
by Nanfang Hu 11 Jun '20

11 Jun '20

When I try to build the tutorial and run ninja I got the following error. [1/31] Performing build step for 'hello-app' ninja: no work to do. [3/31] Performing configure step for 'poke-module' FAILED: poke-module-stamp/poke-module-configure cd /home/weiqi/test/camkes-vm-linux_build/poke-module && /usr/local/bin/cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_TOOLCHAIN_FILE=/home/w eiqi/test/tools/seL4/cmake-tool/polly_toolchains/linux-gcc-32bit-pic.cmake -DLINUX_KERNEL_DIR=/home/weiqi/test/camkes-vm-linux_build/out/linux-4.8.16 -DMODULE_HELPERS_FILE=/home/weiqi/test/projects/camkes-vm-linux/linux-module-helpers.cmake -GNinja /home/weiqi/test/camkes-vm-linux/modules && /usr/local/bin/cmake -E touch /home/weiqi/test/camkes-vm-linux_build/poke-module-stamp/pok e-module-configure CMake Warning (dev) in CMakeLists.txt: No project() command is present. The top-level CMakeLists.txt file must contain a literal, direct call to the project() command. Add a line of code such as project(ProjectName) near the top of the file, but after cmake_minimum_required(). CMake is pretending there is a "project(Project)" command on the first line. This warning is for project developers. Use -Wno-dev to suppress it. -- [polly] Used toolchain: Linux / gcc / PIC / c++11 support / 32 bit CMake Error at CMakeLists.txt:11 (DefineLinuxModule): DefineLinuxModule Function invoked with incorrect arguments for function named: DefineLinuxModule -- Configuring incomplete, errors occurred! See also "/home/weiqi/test/camkes-vm-linux_build/poke-module/CMakeFil es/CMakeOutput.log". See also "/home/weiqi/test/camkes-vm-linux_build/poke-module/CMakeFil es/CMakeError.log". [4/31] Completed 'hello-app' ninja: build stopped: subcommand failed. >

2 2

question about creating threads in sel4 based system
by sergey volkovich 10 Jun '20

10 Jun '20

Cabulertion. I trying to create my own sel4 based system, and currently i cannot understand next thing after calling seL4_Untyped_Retype i will be must somehow put execution data in memory. It can be implemented by using seL4_TCB_WriteRegisters. -- sever99

2 1

RISC-V (RV64) is the third ISA with verified seL4
by Heiser, Gernot (Data61, Kensington NSW) 09 Jun '20

09 Jun '20

Dear seL4 community, I’m extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. My blog discusses provides a bit more context for this announcement: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/ What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. Gernot for the Trustworthy Systems team and the seL4 Foundation

1 0

seL4 + TrustZone: Spanning both worlds
by Nick Spinale 08 Jun '20

08 Jun '20

On TrustZone-enabled Arm systems, seL4 could span both the secure and normal worlds. To do so would require extending untyped and frame capabilities with a bit associating them with either the secure or non-secure physical address space. In this email, I’ll touch on what a software stack based on this idea might look like, why that’s interesting, and exactly what extensions to the kernel it would require. I’m interested in your thoughts and feedback on this informal proposal. If there’s interest, I’ll draft a patch to illustrate it more precisely. # TrustZone background The security of a TrustZone-enabled system is achieved by partitioning all of the SoC’s hardware and software resources so that they exist in one of two worlds - the secure world for the security subsystem, and the normal world for everything else. From the point of view of an ARMv8-A processor, the system has two physical address spaces: one for secure transactions and another for non-secure transactions. Page table entries contain a field called the NS (non-secure) bit, which determines whether a page is mapped from the secure or non-secure physical address space. Furthermore, the processor state contains a global NS bit, which can only be modified by software executing at the highest exception level, EL3. When the NS processor state bit is set, the processor is said to be executing in the non-secure state, and can’t issue secure bus transactions, regardless of the values of the NS bits in its translation tables. A typical TrustZone software stack hosts a TEE (Trusted Execution Environment) on secure-world resources, and a REE (Rich Execution Environment) on normal-world resources. A so-called “secure monitor” runs in EL3, and uses the NS processor state bit to implement a coarse context switch called a “world switch”. The simplicity of this coarse context switch minimizes the attack surface of the secure monitor. # seL4 + TrustZone A formally verified microkernel such as seL4 can be trusted to protect secure hardware resources, and the TEE they host, using translation tables alone. That is, seL4 allows for a design where the processor always runs in state NS=0 (“secure state”), and normal-world software is restricted to non-secure world hardware resources using just the NS bits in the translation tables controlled by seL4. Such a software stack, with seL4 spanning both the secure and non-secure worlds, is attractive on multiple fronts. seL4 provides a higher level of assurance than typical EL3 monitor firmware, which we can now eliminate from the TCB. seL4 also provides a richer API than typical EL3 firmware, allowing for security critical secure-world components to be developed and verified at a higher level of abstraction. Furthermore, while the two-world model is organized around just one strong security boundary, seL4 allows for an unbounded number of equally strong security boundaries, as isolation is based on translation tables rather than the less flexible NS processor state bit. This design allows a seL4-based system to utilize non-secure hardware resources, while protecting the kernel and sensitive components inside secure hardware resources. This permits a threat model similar to that of a typical TrustZone-based TEE (such as OP-TEE or Trusty), which includes some hardware attacks, but without limiting seL4 userland components to the secure world alone. Such a software stack has been especially interesting since the release of ARMv8.4-A, which enables EL2 in the secure state (S-EL2). seL4 running in S-EL2 can host a rich operating system such as Linux to drive non-secure hardware resources. Compare this to a seL4-based software stack running a Linux VM without the help of TrustZone. In particular, consider a case where the Linux VM drives most of the hardware platform’s devices via direct passthru access. Reasoning about the interactions between hardware components on a SoC is difficult. Even after correctly programming the SMMU, a great deal of SoC-specific detail must be covered in order to convince yourself that a driver or VM can’t violate its isolation indirectly through a device within its reach. This sort of reasoning is an active area of research (see, for example, the Barrelfish OS project). However, for use cases where the trust model aligns with the SoC’s boundary between secure and non-secure hardware resources, TrustZone provides a straightforward means of ensuring the protection of critical software components from those with access to non-secure devices. # Extending seL4 Currently, untyped objects are either general purpose memory or device memory. To support the design I’ve proposed, untyped objects would need to be extended with another dimension: secure memory or non-secure memory. Non-secure general purpose memory would be subject to the same restrictions as device memory, with the exception that frames derived from non-secure general purpose untyped may be used as IPC buffers. Unlike the general-purpose/device dimension, the secure/non-secure dimension affects the mapping of a frame. The kernel would set the NS bit in page table entries according to whether that frame is secure. This extension would require modifying just a few lines of code in the kernel itself and would, of course, be optional and configurable. - - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - - The ideas presented in this email constitute research activity at Arm rather than an official position or recommendation. IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

3 3

Difficulty booting guest kernel on zcu102
by Travis Wheatley 05 Jun '20

05 Jun '20

I’ve been working with a VM and docker container created by the good folks at DornerWorks. I had a compile time error with the camkes-arm-vm-manafest tree called out in their "Getting Started” lab. However, I was able to successfully compile an image using the instructions and files in their single_vm_lab. I am loading that image onto an SD card with their pre-built boot.bin. At the U-boot prompt I load that image to 0x10000000 and subsequently type “go 0x10000000”. The image seems to start the initial boot just fine but I get an exception when it tries to jump to the kernel. image entry point. Looking at the value of esr_eli1 it appears that something is trying to write to a protected register. Wondering if there is some sort of switch setting on the board or special flags that need to be sent to u-boot to keep this from happening. Here is the console output: ZynqMP> fatload mmc 0 0x10000000 dorner 22183936 bytes read in 1472 ms (14.4 MiB/s) ZynqMP> go 0x10000000 ## Starting application at 0x10000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[10000000..1152e06f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 100f4058. Loaded DTB from 100f4058. paddr=[237000..23bfff] ELF-loading image 'kernel' paddr=[0..236fff] vaddr=[ff8000000000..ff8000236fff] virt_entry=ff8000000000 ELF-loading image 'capdl-loader' paddr=[23c000..1854fff] vaddr=[400000..1a18fff] virt_entry=4088d0 ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point... ELF-LOADER: Synchronous exception received: esr_el1: 86000004 elr_el1: ff8000000000 spsr_el1: 600003c5 far_el1: ff8000000000 abort() called.

1 0

Builds
by Matt Youill 04 Jun '20

04 Jun '20

Hi, Am in the process of learning seL4 and have managed to get, build and run the tutorials, which is great. Now looking at creating an application and I have a question about seL4 builds. The documentation here... https://docs.sel4.systems/projects/buildsystem/incorporating.html refers to a build setup that AFAICT is different to the reference application, which I think is here... https://github.com/seL4proj/sel4webserver Which is the best approach to follow? Best, Matt

2 1

Re: [seL4] Threads tutorial fails to initialize
by Weiqi Hu 04 Jun '20

04 Jun '20

Thank you for the suggestion but it seems like I need to access the init file one directory above. In the case of seL4test and build-x86 it needs to be init-build.sh On Sun, May 31, 2020 at 9:14 AM laokz <laokz(a)foxmail.com> wrote: > Hi Weiqi, > > Did you try init-build.sh( > https://docs.sel4.systems/GettingStarted#setting-up-your-machine)? I > recall this like issue before. > > Regards, > laokz > > I tried adding the --plat argument but it's the same error. Also, no build > directory was created on the attempts. > > I didn't have the same problem with the capabilities, untyped, and mapping > tutorials but it appears something is different for the threads tutorial. > > On Sat, May 30, 2020 at 5:11 PM Chubb, Peter (Data61, Kensington NSW) < > Peter.Chubb(a)data61.csiro.au> wrote: > > > >>>>> "Weiqi" == Weiqi Hu <weiqi.hu(a)gmail.com> writes: > > > > Weiqi> Hi, I've tried to start the threads tutorial but it fails to > > Weiqi> initialize or create a build directory. Any hints for moving > > Weiqi> forward? > > > > Looks like you omitted the --plat argument. > > > > Try > > ../init --plat pc99 --tut threads --solution > > > > You may need to delete the build directory before this will work. > > > > -- > > Peter Chubb Tel: +61 2 9490 5852 > > http://ts.data61.csiro.au/ > > Trustworthy Systems Group CSIRO's > Data61 > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > >

2 2

constituting seL4 TSC meeting
by Klein, Gerwin (Data61, Kensington NSW) 03 Jun '20

03 Jun '20

The technical steering committee (TSC) of the seL4 Foundation had its constituting meeting on 20 May, and the meeting minutes [1] are now published on the TSC page of the foundation [2]. The TSC is the body that sets the technical direction of seL4 and its proofs, including processes, contributions, documentation, etc. This first TSC meeting was mostly about processes and setting things up — future TSC meetings are planned to be public, and will be announced on this mailing list. One of the first things the TSC would like to do is make seL4 and its related repositories easier to contribute to. You may have seen a few things that already have happened: - more content on the docs site at foundation launch - DCO instead of CLA - first direct github CI tests that run on pull requests for the seL4 and l4v repos Some of the things we are planning to do: - make seL4 code and proof regression tests available directly on github as much as possible, to make it easier to see what breaks verification and what not - open up issues and pull request management more to the community so that pull requests can become less of a bottleneck - publish the source of the sel4.systems site, so people can make contributions - more documentation for the proofs If you have ideas what else the TSC could do to encourage contributions, please let us know! Either here on the mailing list, or if you prefer, by email to me directly. Cheers, Gerwin (for the TSC) [1]: https://sel4.systems/Foundation/TSC/notes/tsc-meeting-2020-05-20.pdf [2]: https://sel4.systems/Foundation/TSC/

1 0

UNSW seL4 teaching videos available
by Heiser, Gernot (Data61, Kensington NSW) 02 Jun '20

02 Jun '20

Dear seL4 community, I’m pleased to announce yet another contribution of UNSW Sydney to the seL4 community: This year I’m making the seL4-related videos from my UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel: https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site: https://www.cse.unsw.edu.au/~cs9242/current/ Enjoy, Gernot

2 1

mcs kernel compatible with camkes project
by Parvaneh Ahgajani 02 Jun '20

02 Jun '20

Hello all, I wanted to use camkes to create real-time application. In periodic application, it mentioned that "_period" and "_budget" only have affect on the MCS kernel. I tried to build application with kernel version 11.0.0-dev but it doesn't work. I wanted to know how I can have access to MCS kernel that is compatible with camkes project. Thank you, Parvaneh Aghajani.

2 1

Threads tutorial fails to initialize
by Weiqi Hu 01 Jun '20

01 Jun '20

Hi, I've tried to start the threads tutorial but it fails to initialize or create a build directory. Any hints for moving forward? weiqi@weiqi-ThinkPad-X250:~/sel4-tutorials-manifest-temp/threads$ sudo ../init --verbose --tut threads --solution Traceback (most recent call last): File "../init", line 96, in <module> sys.exit(main()) File "../init", line 85, in main args.task, initialised, tute_dir, build_dir, sys.stdout) File "/home/weiqi/sel4-tutorials-manifest-temp/projects/sel4-tutorials/common.py", line 100, in init_directories os.chdir(build_directory) FileNotFoundError: [Errno 2] No such file or directory: '/home/weiqi/sel4-tutorials-manifest-temp/threads_build'

2 2

Building picoserver example
by Russel emkil.minor 26 May '20

26 May '20

Dear seL4 developers, I am trying to built picoserver example https://github.com/seL4/camkes/tree/master/apps/picoserver <https://github.com/seL4/camkes/tree/master/apps/picoserver> using the following commands: $ ../init-build.sh -DPLATFORM=x86_64 -DCAMKES_APP=picoserver $ ninja But I am getting the following error: fatal error: pico_stack.h: No such file or directory Looks like I need to install libpicotcp. I found it here https://github.com/seL4/util_libs/tree/master/libpicotcp <https://github.com/seL4/util_libs/tree/master/libpicotcp> but no idea how to build and link to the example. Can you give me a hint how to proceed? Best regards, Ruslan Rezin.

2 1

seL4 Whitepaper Released
by Heiser, Gernot (Data61, Kensington NSW) 25 May '20

25 May '20

Dear seL4 community, I’m pleased to announce the seL4 Foundation whitepaper: The seL4 Microkernel – An Introduction This white paper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems. You can download it at https://sel4.systems/About/ Feedback welcome. Gernot PS: Some of you may have seen a pre-release version that was up on the Foundation web site since the Foundation launch. This is the complete version.

1 0

Trouble accessing linux guest through tun/tap
by Travis Wheatley 22 May '20

22 May '20

Greetings, I am working with the camkes-arm-vm qemu-arm-virt configuration. I started with the vm_minimal configuration and have added a tun/tap interface by creating the tap on my host thusly: # ip tuntap add tap0 mode tap # ip addr add 10.0.120.100/24 dev tap0 # ip link set dev tap0 up I have added support for what I beleive to be the appropriate interrupts by modifying my devices.camkes file thusly: vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; vm0.dtb_irqs = [35, 36, 37, 38]; Additionally, I have modified the settings.camkes thusly: if(${PLATFORM} STREQUAL "qemu-arm-virt") # force cpu set(QEMU_MEMORY "2048") set(KernelArmCPU cortex-a53 CACHE STRING "" FORCE) set(VmInitRdFile ON CACHE BOOL "" FORCE) set(VmPCISupport ON CACHE BOOL "" FORCE) set(VmVirtioNetArping OFF CACHE BOOL "" FORCE) set(VmVirtioNetVirtqueue ON CACHE BOOL "" FORCE) # set(qemu_sim_extra_args "-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01") set(qemu_sim_extra_args "-net nic,model=e1000 -netdev tap,id=mynet0,script=no,ifname=tap0 -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01") set(KernelArmExportPCNTUser ON CACHE BOOL "" FORCE) set(KernelArmExportPTMRUser ON CACHE BOOL "" FORCE) endif() This results in a tunl0 interface showing up on my linux guest. However, that interface does not have a mac address associated with it. I can use ifconfig to assign an IP address on the same subnet as the corresponding tap interface on the host. However, I can’t ping between the two. I thought this might be because I have VmVitruoNetArping set to OFF. However, I get compile time errors when I turn it on. Because the tunl0 inteface does not have the mac address specied in the qemu_sim_extra_args I am unsure of how to set up an arp table entry. Exctly what do I need to do to enable network communications between my linux guest and the host?

2 1

Help with creating a new project
by Yates, Tim 22 May '20

22 May '20

Hi, I am attempting to create a new CAmkES project. So far I have used the https://github.com/seL4/camkes-manifest.git repository and the https://github.com/SEL4PROJ/camkes-arm-vm-manifest repository and placed my .camkes file and components into the respective app folders for each. I then attempt to initialise my project as instructed here https://docs.sel4.systems/projects/camkes/ but it fails. It gives me the following error: hardware_gen.py: error: argument --dtb: can't open '/workspaces/microimpexor/seL4_build/build/kernel/kernel.dtb': [Errno 2] No such file or directory: '/workspaces/microimpexor/seL4_build/build/kernel/kernel.dtb' I am initialising my project with the following command: ../init-build.sh -DPLATFORM=qemu-arm-virt -DAARCH32=1 -DCAMKES_APP=appname -DSIMULATION=1 Some assistance on this matter would be greatly appreciated. Regards Tim Yates ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 1

some confuse about "bootstrap_use_current_simple" of bootstrap.c in libsel4allocman
by yadong.li 20 May '20

20 May '20

allocman_t *bootstrap_use_current_simple(simple_t *simple, size_t pool_size, void *pool) { allocman_t *allocman; int error; /* Initialize inside the current 1 level cspace as defined by simple */ allocman = bootstrap_use_current_1level(simple_get_cnode(simple), simple_get_cnode_size_bits(simple), simple_last_valid_cap(simple) + 1, BIT(simple_get_cnode_size_bits(simple)), pool_size, pool); if (!allocman) { LOG_ERROR("Failed to initialize an allocman"); return allocman; } ....... return allocman; } The params of "bootstrap_use_current_1level" below: cnode_size = simple_get_cnode_size_bits(simple), like 23, it is 8M endslot = BIT(simple_get_cnode_size_bits(simple)), also 8M I think we don't have so many endslot, because per slot is not only one byte Thank you very much

1 0

additional: some question about VisualCAmkES ？
by yadong.li 27 Apr '20

27 Apr '20

Hi， I found the VisualCAmkES tool can not parse grammar like import and marco in cmakes file, If I write very simple camkes file, only include one assembly and component. I want to know How can I use this VisualCAmkES tool to generate visual file in complex project like vm_minimal ? 发件人: yadong.li 发送时间: 2020年4月25日 21:06 收件人: 'devel(a)sel4.systems' 主题: some question about VisualCAmkES ？ Hi， I want to use VisualCAmkES for view，I follow the step of https://docs.sel4.systems/projects/camkes/visual-camkes/ I meet the below Problem， how can I resolve it ？ Thank you very much Syntax Error (u'/home/yadong.li/seL4_vm_11/ sel4_horizon/camkes-arm-vm/projects/vm/ apps/vm_cross_connector/vm_cross_connector.camkes:36:5: \x1b[31m\ x1b[1mVM_INIT_DEF\x1b[0m()', u' ', u"Syntax error in input at 'VM_INIT_DEF' (type ID) line 36 col 5", u"Syntax error in input at 'VM_GENERAL_COMPOSITION_DEF' (type ID) line 45 col 9", u"Syntax error in input at '(' (type _ANON_4) line 60 col 37")

1 0

some question about VisualCAmkES ？
by yadong.li 25 Apr '20

25 Apr '20

Hi， I want to use VisualCAmkES for view，I follow the step of https://docs.sel4.systems/projects/camkes/visual-camkes/ I meet the below Problem， how can I resolve it ？ Thank you very much Syntax Error (u'/home/yadong.li/seL4_vm_11/ sel4_horizon/camkes-arm-vm/projects/vm/ apps/vm_cross_connector/vm_cross_connector.camkes:36:5: \x1b[31m\ x1b[1mVM_INIT_DEF\x1b[0m()', u' ', u"Syntax error in input at 'VM_INIT_DEF' (type ID) line 36 col 5", u"Syntax error in input at 'VM_GENERAL_COMPOSITION_DEF' (type ID) line 45 col 9", u"Syntax error in input at '(' (type _ANON_4) line 60 col 37")

1 0

Re: [seL4] Trouble with the tun/tap interface in linux guest
by Travis Wheatley 23 Apr '20

23 Apr '20

Thank you for your reply Kent. I modified the devices.camkes in the corresponding project folder as suggested. However, I am still seeing the same behavior. Are there other items I need to add or is there something in the kernel that needs to be enabled? I tried swapping in an Ubuntu server 18.01 kernel. It boots, but I do not even see the tunl0 interface that I see when I boot the default vm_minimal image. Here is what the vm0.untyped_mmios block looks like in my devices.camakes file looks like vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; vm0.dtb_irqs = [35, 36, 37, 38]; I found that the vm_multi project devices.camkes has similar stanzas in the vm0.untyped.mmios block. However, the Interrupt controller item has an additional 0x1000 token in it: "0x8040000:0x1000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) I tried this in the vm_minimal configurationo but ../init.sh throws an error indicating that it doesn’t know how to parse that. I also was able to boot the vm_multi configuration in the emulator and noticed that it did, in fact, have both an eth0 and eth1 interface, but was not able to get them to work because the kernel seemed to be stuck in a loop looking for a non-existent DHCP server. Wondering if there is some other config somewhere that I need to get a working eth0 interface on the vm_minimal configuration? Message: 1 Date: Tue, 21 Apr 2020 20:57:24 +0000 From: Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>> To: "devel(a)sel4.systems<mailto:devel@sel4.systems>" <devel(a)sel4.systems<mailto:devel@sel4.systems>> Subject: [seL4] Trouble with the tun/tap interface in linux guest Message-ID: <207FF441-86A1-4CE3-88AD-8BACC908138D(a)emergentspace.com<mailto:207FF441-86A1-4CE3-88AD-8BACC908138D@emergentspace.com>> Content-Type: text/plain; charset="utf-8" Thanks to recent patches I have been able to build and boot the linux guest kernel under the simulator in the camkes-arm-vm project using the vm_minimal configuration. However, I am having trouble accessing it via the network interface. First I set up a tap interface as follows: # sudo ip tuntap add tap0 mode tap # sudo ip addr add 10.0.120.100/24 dev tap0 # sudo ip link set dev tap0 up Then I start the simulation using the following command line, which I believe should make the tap interface appear as an e1000 nic to the guest kernel: ./simulate --extra-qemu-args="-net nic,model=e1000 -net tap,script=no,ifname=tap0? In the linux guest the ?ip a? command shows that there is a tunl0 network device available. I have tried a couple of methods of activating it including using ifconfig to bring it up and assign it an ip address as well as the ?ip link set tun0 up? followed by the ?ip addr add 10.0.120.1/24 dev tunl0? command. According to ifconfig both of these bring the interface up and provide it with an ip address. However, I can?t ping the tap ip address from the guest nor can I ping the guest tunl0 interface from another console on the host. So, what am I missing? ------------------------------ Message: 2 Date: Tue, 21 Apr 2020 23:09:16 +0000 From: "Mcleod, Kent (Data61, Kensington NSW)" <Re: [seL4] Trouble with the tun/tap interface in linux guest> To: Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>>, "devel(a)sel4.systems<mailto:devel@sel4.systems>" <devel(a)sel4.systems<mailto:devel@sel4.systems>> Subject: Re: [seL4] Trouble with the tun/tap interface in linux guest Message-ID: <SYXPR01MB0832783D9CD6B3B03B0F04FFABD50(a)SYXPR01MB0832.ausprd01.prod.outlook.com<mailto:SYXPR01MB0832783D9CD6B3B03B0F04FFABD50@SYXPR01MB0832.ausprd01.prod.outlook.com>> Content-Type: text/plain; charset="iso-8859-1" It could be that the camkes configuration doesn't pass through the PCI device to the Linux guest? You need to add the Interrupts and PCI MMIO configurations below: ? ? ? ? vm0.untyped_mmios = [ ? ? ? ? ? ? ? ? ? ? "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) ? ? ? ? ? ? ? ? ? ? "0x10040000:17", // QEMU PCI MMIO ? ? ? ? ? ? ? ? ? ? "0x3eff0000:16", // QEMU PCI IO ports ? ? ? ? ? ? ? ? ? ? "0x40000000:29", // Linux kernel memory regions ? ? ? ? ? ? ? ? ? ? ]; ? ? ? ? vm0.dtb_irqs = ?[35, 36, 37, 38]; The device should then appear in the guest under eth0. Kent. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 71, Issue 24 *************************************

1 0

Trouble with the tun/tap interface in linux guest
by Travis Wheatley 22 Apr '20

22 Apr '20

Thanks to recent patches I have been able to build and boot the linux guest kernel under the simulator in the camkes-arm-vm project using the vm_minimal configuration. However, I am having trouble accessing it via the network interface. First I set up a tap interface as follows: # sudo ip tuntap add tap0 mode tap # sudo ip addr add 10.0.120.100/24 dev tap0 # sudo ip link set dev tap0 up Then I start the simulation using the following command line, which I believe should make the tap interface appear as an e1000 nic to the guest kernel: ./simulate --extra-qemu-args="-net nic,model=e1000 -net tap,script=no,ifname=tap0” In the linux guest the “ip a” command shows that there is a tunl0 network device available. I have tried a couple of methods of activating it including using ifconfig to bring it up and assign it an ip address as well as the “ip link set tun0 up” followed by the “ip addr add 10.0.120.1/24 dev tunl0” command. According to ifconfig both of these bring the interface up and provide it with an ip address. However, I can’t ping the tap ip address from the guest nor can I ping the guest tunl0 interface from another console on the host. So, what am I missing?

2 1

Incorporating the Build System - The CAmkES Perspective
by Turner, Ben 21 Apr '20

21 Apr '20

Hi, We are attempting to define a system that comprises 3 components that can talk to each other. We have managed to get the system built and working using the existing tutorial repo and the hello-camkes-0 app, however we are struggling to determine what precisely we would need to copy from this in order to define our own standalone application within the seL4 build system. We have read the existing documentation at https://docs.sel4.systems/projects/buildsystem/incorporating.html but cannot find any information on what additions are required when using the CAmkES and ARM capabilities. Any help you can provide would be appreciated. Kind regards, Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 1

TimeServer "IRQ already mapped" error
by Grant Jurgensen 17 Apr '20

17 Apr '20

Hi all, I'm trying to add a timer to my CAmkES component (all I need is a timestamp). I've been using this example component as a reference: https://github.com/seL4/camkes/tree/master/apps/timeserver My problem is that when I declare an instance of the global TimeServer component in my ".camkes" file, I get an error at build-time: "parse-capDL: IRQ already mapped: 68". I'm not sure what to make of this error. The only major difference between my project and the reference above is that I am building atop the camkes-arm-vm project. Could the VM be interfering here? Thanks, Grant Jurgensen

2 3

Benchmarks of seL4
by Leo Gaspard 16 Apr '20

16 Apr '20

Hello, I come wondering: the FAQ claims that seL4 is “the world's fastest microkernel”. However, I can only find benchmarks of just seL4, without comparison to other operating systems running on the same machine. Would you happen to have such comparative benchmarks? I'd be particularly interested by something against L4Re, as it'd probably allow me to guess at the performance of something similar to L4Linux ported to seL4. Thank you for all you do on seL4! Leo

6 12

Failed to find device frame in new verion on my environment
by yadong.li 16 Apr '20

16 Apr '20

Hi， I recently move my wrok to a new seL4 version (I checkout default.xml in project camkes-arm-vm on 2020.02.25), I have below error print: “create_object@main.c:659 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x90006000” 1、 I debug code, /**/ is my environment run parameter BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before) { paddr_t start = 0; /*---------------------add region, start = 0x1800000, end = 0x2080000 *---------------------add region, start = 0x20ff000, end = 0x2100000 *---------------------add region, start = 0x80000000, end = 0x90001000 *---------------------add region, start = 0x90003000, end = 0x90004000 */ for (word_t i = 0; i < ndks_boot.resv_count; i++) { if (start < ndks_boot.reserved[i].start) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, ndks_boot.reserved[i].start }); if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } start = ndks_boot.reserved[i].end; } /*---------------------add region, start = 0x90005000, CONFIG_PADDR_USER_DEVICE_TOP = 0xff, PPTR_TOP = 0xffffc0000000*/ if (start < CONFIG_PADDR_USER_DEVICE_TOP) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, CONFIG_PADDR_USER_DEVICE_TOP }); /* * The auto-generated bitfield code will get upset if the * end pptr is larger than the maximum pointer size for this architecture. */ if (reg.end > PPTR_TOP) { reg.end = PPTR_TOP; } if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } return true; } 2、 CONFIG_PADDR_USER_DEVICE_TOP = 0xff, I found print the value must use 0x%x, can’t use 0x%lx, it is wrong 3、My platform is cortexA53 kernel/src/plat/j2/config.cmake:28: set(KernelArmCortexA53 ON) 4、and I change follow KernelArmCortexA53： a) ‘math(EXPR KernelPaddrUserTop "(1 << 40) - 1")’ to ‘set(KernelPaddrUserTop "1099511627775")’ ----------the print is “Failed to find device frame” disappear 5、my pc tools install，follow the seL4 wiki， cmakes version is 3.12.2 (> 3.7.2) 6、I did not find error or warning when I ../init-build.sh -DAARCH64=TRUE …… ---------------is it need to install new tools? Or other problem Thank you very much.

2 1

RPi4: DTS memory device and vm_minimal
by Turner, Ben 16 Apr '20

16 Apr '20

Hi, I have been attempting to get the vm_minimal application running on the Raspberry Pi 4 platform, and I have managed to get to the point where I need to define the memory regions for the kernel and virtual machine. The issue is that I do not know what the correct values (if any) would be needed in the overlay-rpi4.dts that I have created. From what I have found to this point, the Pi platform implements a memory system that means it is not possible to define memory regions in a DTS file. These memory regions are user-defined and are not known until runtime. I think I know what the answer will be to this; is there a way to overcome the oddities of the RPi4 memory setup when attempting to create a seL4 CAmkES VM linux image? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 3

Trouble booting default cmakes-vm-arm project under QEMU
by Travis Wheatley 16 Apr '20

16 Apr '20

Sel4 Developers, Still learning to crawl here. I have built the cmakes-vm-arm project for the qemu-arm-virt target. I have QEMU version 3.1.0 installed on my host. When I run the simulation by executing the command “./simulate”. it appears as though Sel4 is booting and successfully downloading the kernel, dtb, and loader. However, I am running into problems when it starts booting the kernel. It looks to me like it might be booting the kernel OK with the exception of a warning about GIC interrupts and subsequently drops to user space. Following that I see errors about insufficient memory and invalid num_vcpus. Not quite sure how to correct this. Hoping one of y’all can point me in the right direction. Here is a copy of the output — Begin included text — $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] (my_virtual_env) trickdev@trickvm ~/cmakes-arm-vm/vm-build $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' paddr=[6023b000..61703fff] vaddr=[400000..18c8fff] virt_entry=407fe8 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/216 T0xff80bf815400 "rootserver" @400704]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> run(a)main.c<mailto:run@main.c>:1095 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) sel4platsupport_copy_irq_cap(a)device.c<mailto:sel4platsupport_copy_irq_cap@device.c>:41 Failed to get cap for irq irq_register_common(a)irq.c<mailto:irq_register_common@irq.c>:316 Failed to register an IRQ Assertion failed: (cspace->bitmap[index / BITS_PER_WORD] & BIT(index % BITS_PER_WORD)) == 0 (/home/trickdev/cmakes-arm-vm/projects/seL4_libs/libsel4allocman/src/cspace/single_level.c: _cspace_single_level_free: 100)

2 1

Best starting point for running VM Linux on a raspberry pi?
by Travis Wheatley 16 Apr '20

16 Apr '20

Greetings sel4 developers. Thus far I have successfully built and run the camkes-arm-vm on a TK1 platform as described here:https://docs.sel4.systems/projects/camkes-arm-vm/ I have also been able to boot to a u-boot prompt and run some sel4 test code as described here:https://docs.sel4.systems/Hardware/Rpi3.html My goal is to run a custom linux kernel under sel4 on the raspberry pi and am wondering what would be the best starting point. There is a tutorial about running a linux kernel under sel4 located here:https://docs.sel4.systems/Tutorials/camkes-vm-linux.html However, it only supports x86. There is also the camkes-arm-vm mentioned above but the raspberry pi is not among the supported platforms. Before reinventing the wheel I am hoping there might be some existing project or a better starting point for running a linux guest under sel4 on a raspberry pi that I can use. — Travis

2 1

Re: [seL4] Cross-core thread migration
by Millar, Curtis (Data61, Kensington NSW) 13 Apr '20

13 Apr '20

Hi Demi, > If I have a manycore machine, what is the best way to migrate a thread from > one core to another? Similarly, how can I send a capability (such as to > memory)? Cryptography is an option for the second one, but seems inelegant > and inefficient. When configured with SMP (which is not currently available in any verified config urations) a thread can be migrated to another core within a single kernel image cluster by changing its affinity. The MCS API will change this slightly; each scheduling context is associated with a core of the kernel image cluster so the scheduling context can be reconfigured to run on a different core (using that core's ScheduleControl capability) or a scheduling context already associated with that core can be bound to the thread to move it to that core. > Alternatively, are future versions of seL4 expected to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. IPC between cores in a single kernel image provides all of the necessary mechanisms for transferring data and capabilities between threads. In larger multicore machines, the cores would be split up into clusters where each cluster would essentially map to a single shared L2 cache (more generally, the clusters would be split to keep accesses to shared data structures in the kernel in the higher-level caches). I'm not sure how we would approach transferring kernel objects and capabilities between kernel images on different clusters whilst preserving the particular design goals that seL4 aims to implement. Cheers, Curtis

3 4

Support for 64-bit virtual machines on x86-64
by J Call 12 Apr '20

12 Apr '20

Hi all, I’m trying to use seL4 as a hypervisor on an embedded system. This particular SBC has 32 Gb of RAM and I’d like to install a couple of CentOS 8 64bit VMs side by side, but would like the vm’s to take advantage of more than 4Gb of RAM. Is there any word on seL4 supporting 64-bit virtual machines on the x86-64 architecture one day? Sincerely, Jonathan

2 1

Scheduler discussion on LWN
by Zach Lym 12 Apr '20

12 Apr '20

Red Hat's lead real-time scheduling engineer (who has a solid background in formal methods) posted an interested comment on an LWN article about seL4's scheduler research (https://lwn.net/Articles/745946/) While I disagree with the tone of the comment, I rarely see informed critiques of seL4 and context switching performance is core to microkernel viability. My apologies if this is an inappropriate venue for this discussion. --- "With the current scheduler, that driver must be given a high priority and trusted to not hog the CPU." So, they need to implement either RT throttling or the CBS, like Linux. "Another problem is data structures that are shared between criticalities....se of the priority-ceiling protocol can help." Nice, then they will see that the priority ceiling will add release jitter to the highest priority task, and then will notice that they will have to use other protocol, like, mutexes with priority inheritance? Where did I hear about it already... ah! On Linux! It is widely known that if you use priority ceiling, you will have scheduling "latency." But it really helps to reduce the response time... so, what do you prefer Response Time or Scheduling latency (release jitter or any scheduling delay, scheduler overhead... or any other name people do for it)? "Any process that exceeds its CPU budget during a given period can be throttled. Processes that have shorter periods are given a higher priority by the scheduler." Ok! here they have something like CBS, but they are using the fixed-priority rate monotonic scheduling approach! Nice! that is a technology from... 1969? But wait, if they already implemented this, why is the "network driver" a problem? - answer: because they cannot estimate the period of the packets arriving - RM is not flexible enough to all real-world cases! But that does not mean that this is the only solution. So my question is: Is there a sufficient & necessary schedulability test for their scheduler? "what happens if the client's budget runs out while the server is running?" Welcome to our world, check the "dl_boosted" variable on sched_deadline. "This new scheduler solves the problem, but it does not come for free: interrupt latency increases by 11% and scheduling itself is 19% more expensive. In both cases, the need to reprogram hardware timers is the source of most of the slowdown. But, he noted, scheduling in seL4 is "still an order of magnitude faster than Linux"" Welcome to our world again! And let me guess when you will start to have our numbers... When you finish implementing "some memory-management unit operations, and multicore operation"? Because on PREEMPT_RT we do this in microseconds, will they implementation continue working on ns (i.e., an order of magnitude faster than Linux) with such features? And I wonder, where is the mixed-criticality part of the schedulers...? Running Linux as a guest? I read the papers, and the work is very nice! Seriously! Very nice! But please, stop the comparison of orange and apples. It is not possible to compare this OS with Linux. Moreover, there are other OSs with such features running on real systems. Verified or not, they are certified for it.

2 1

答复: Devel Digest, Vol 71, Issue 10
by yadong.li 10 Apr '20

10 Apr '20

Subject: [seL4] TimeServer "IRQ already mapped" error Maybe the irq of Time exist in vm and TimeServer meanwhile. Try delete the tree node of time in your devices.camkes of you platform, like this: assembly { vm0.dtb = dtb([{}]); /*vm0.dtb = dtb([{"path": "/soc/serial@0xA5000000"}]);*/ -----only delete the conflict part } -----邮件原件----- 发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 devel-request(a)sel4.systems 发送时间: 2020年4月10日 10:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 71, Issue 10 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: setConsumed() in seL4_SchedContext_YieldTo (=?utf-8?B?bGFva3o=?=) 2. TimeServer "IRQ already mapped" error (Grant Jurgensen) ---------------------------------------------------------------------- Message: 1 Date: Thu, 9 Apr 2020 19:11:14 +0800 From: "=?utf-8?B?bGFva3o=?=" <laokz(a)foxmail.com> To: "=?utf-8?B?QW5uYSBMeW9ucw==?=" <anna(a)gh.st>, "=?utf-8?B?ZGV2ZWw=?=" <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Message-ID: <tencent_C27271A3F0A40CF84A7FDBB4F299EB059A09(a)qq.com> Content-Type: text/plain; charset="utf-8" Hello Anna, With your point, I am cleared - activateThread() does the completeYieldTo assurance before A yield to B again. Can I conclude that YieldTo() method is limited to 1:1 relationship? Thanks, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Thu, Apr 9, 2020 07:12 AM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi laokz, Yes, that scenario cannot happen. If B runs to block, and A is scheduled, the kernel will complete A's initial yieldTo call and clear the appropriate values before resuming A. Cheers Anna. From: laokz <laokz(a)foxmail.com> Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons <anna(a)gh.st>; devel <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Hello Anna, Thanks for the reply. Maybe I'v imagined an impractical scenario: 1. A yield to B. B->sc->scYieldFrom=A 2. B run then block. 3. A run then yield to B again. 4. Now at the beginning, setConsumed() called; because B is not runnable, so return_now=true and setConsumed() called again at the end. For cooperative threads, this indeed shouldn't happen but it depends. For example if B can block, then great care should be taken to forbid this edge case. Regards, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi, Thanks for the observation! It's true that setConsumed should only be called once per kernel entry, and it's not obvious just from the code snippets to observe that this is true. However, the semantics of YieldTo mean that both of these code paths cannot be executed in the same kernel entry. If return_now is true, this means that the current thread will be switched to and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is usually the case if the calling thread YieldTo a lower priority thread, or a thread that is not runnable. On the other hand if return_now is false, the YieldTo resulted in the thread being YieldedTo being switched to, so we return the result of the YieldTo on a different kernel entry (when we run the thread that called YieldTo again). With this context, take a look at the if block here: https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 Where you can see that we only set sc->scYieldFrom when we also set return_now to false. Glad to see someone looking at the MCS kernel. Anna. ------------------------------ Message: 2 Date: Thu, 9 Apr 2020 09:48:49 -0500 From: Grant Jurgensen <gajurgensen(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] TimeServer "IRQ already mapped" error Message-ID: <CAGJ6_3Cdhk9BrMD0roaCZvi7QZr1M7U3GA1jQ3=m0tMHaThSew(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" Hi all, I'm trying to add a timer to my CAmkES component (all I need is a timestamp). I've been using this example component as a reference: https://github.com/seL4/camkes/tree/master/apps/timeserver My problem is that when I declare an instance of the global TimeServer component in my ".camkes" file, I get an error at build-time: "parse-capDL: IRQ already mapped: 68". I'm not sure what to make of this error. The only major difference between my project and the reference above is that I am building atop the camkes-arm-vm project. Could the VM be interfering here? Thanks, Grant Jurgensen ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 71, Issue 10 *************************************

1 0

Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
by laokz 09 Apr '20

09 Apr '20

Hello Anna, With your point, I am cleared - activateThread() does the completeYieldTo assurance before A yield to B again. Can I conclude that YieldTo() method is limited to 1:1 relationship? Thanks, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Thu, Apr 9, 2020 07:12 AM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi laokz, Yes, that scenario cannot happen. If B runs to block, and A is scheduled, the kernel will complete A's initial yieldTo call and clear the appropriate values before resuming A. Cheers Anna. From: laokz <laokz(a)foxmail.com> Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons <anna(a)gh.st>; devel <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Hello Anna, Thanks for the reply. Maybe I'v imagined an impractical scenario: 1. A yield to B. B->sc->scYieldFrom=A 2. B run then block. 3. A run then yield to B again. 4. Now at the beginning, setConsumed() called; because B is not runnable, so return_now=true and setConsumed() called again at the end. For cooperative threads, this indeed shouldn't happen but it depends. For example if B can block, then great care should be taken to forbid this edge case. Regards, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi, Thanks for the observation! It's true that setConsumed should only be called once per kernel entry, and it's not obvious just from the code snippets to observe that this is true. However, the semantics of YieldTo mean that both of these code paths cannot be executed in the same kernel entry. If return_now is true, this means that the current thread will be switched to and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is usually the case if the calling thread YieldTo a lower priority thread, or a thread that is not runnable. On the other hand if return_now is false, the YieldTo resulted in the thread being YieldedTo being switched to, so we return the result of the YieldTo on a different kernel entry (when we run the thread that called YieldTo again). With this context, take a look at the if block here: https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 Where you can see that we only set sc->scYieldFrom when we also set return_now to false. Glad to see someone looking at the MCS kernel. Anna.

1 0

Re: [seL4] Cross-core thread migration
by Millar, Curtis (Data61, Kensington NSW) 09 Apr '20

09 Apr '20

On Tue, 2020-04-07 at 12:00 +1000, 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: setConsumed() in seL4_SchedContext_YieldTo (Anna Lyons) > 2. Cross-core thread migration (Demi Obenour) > > > ------------------------------------------------------------------- > --- > > Message: 1 > Date: Mon, 6 Apr 2020 04:16:00 +0000 > From: Anna Lyons <anna(a)gh.st> > To: laokz <laokz(a)foxmail.com>, devel <devel(a)sel4.systems> > Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo > Message-ID: > < > BYAPR13MB22292529DC4150329B0C44E6DCC20(a)BYAPR13MB2229.namprd13.prod.outlook.com > > > > Content-Type: text/plain; charset="iso-8859-1" > > Hi, > > Thanks for the observation! It's true that setConsumed should only be > called once per kernel entry, and it's not obvious just from the code > snippets to observe that this is true. > > However, the semantics of YieldTo mean that both of these code paths > cannot be executed in the same kernel entry. > > If return_now is true, this means that the current thread will be > switched to and sc->scYieldFrom should be NULL (as the YieldTo call > has completed). This is usually the case if the calling thread > YieldTo a lower priority thread, or a thread that is not runnable. On > the other hand if return_now is false, the YieldTo resulted in the > thread being YieldedTo being switched to, so we return the result of > the YieldTo on a different kernel entry (when we run the thread that > called YieldTo again). > > With this context, take a look at the if block here: > https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 > Where you can see that we only set sc->scYieldFrom when we also set > return_now to false. > > Glad to see someone looking at the MCS kernel. > Anna. > > > > Confidentiality Note:This email is intended only for the person or > entity to which it is addressed and may contain information that is > privileged, confidential or otherwise protected from disclosure. > Unauthorized use, dissemination, distribution or copying of this > email or the information herein by anyone other than the intended > recipient is strictly prohibited. If you have received this email in > error, please notify the sender immediately and destroy the original > message, any attachments thereto and all copies. > > > ------------------------------ > > Message: 2 > Date: Mon, 6 Apr 2020 02:23:08 -0400 > From: Demi Obenour <demiobenour(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Cross-core thread migration > Message-ID: > < > CAJEMUN_it3Uf4Bhs3dVvfLRPeQvznJ8BCJ+Rq2wLbqcLDDHyCw(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > If I have a manycore machine, what is the best way to migrate a > thread from > one core to another? Similarly, how can I send a capability (such as > to > memory)? Cryptography is an option for the second one, but seems > inelegant > and inefficient. Alternatively, are future versions of seL4 expected > to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. > > Sincerely, > > Demi > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 71, Issue 6 > ************************************ Hi Demi, > If I have a manycore machine, what is the best way to migrate a thread from > one core to another? Similarly, how can I send a capability (such as to > memory)? Cryptography is an option for the second one, but seems inelegant > and inefficient. When configured with SMP (which is not currently available in any verified config urations) a thread can be migrated to another core within a single kernel image cluster by changing its affinity. The MCS API will change this slightly; each scheduling context is associated with a core of the kernel image cluster so the scheduling context can be reconfigured to run on a different core (using that core's ScheduleControl capability) or a scheduling context already associated with that core can be bound to the thread to move it to that core. > Alternatively, are future versions of seL4 expected to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. IPC between cores in a single kernel image provides all of the necessary mechanisms for transferring data and capabilities between threads. In larger multicore machines, the cores would be split up into clusters where each cluster would essentially map to a single shared L2 cache (more generally, the clusters would be split to keep accesses to shared data structures in the kernel in the higher-level caches). I'm not sure how we would approach transferring kernel objects and capabilities between kernel images on different clusters whilst preserving the particular design goals that seL4 aims to implement. Cheers, Curtis

1 0

Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
by laokz 09 Apr '20

09 Apr '20

Hello Anna, Thanks for the reply. Maybe I'v imagined an impractical scenario: 1. A yield to B. B->sc->scYieldFrom=A 2. B run then block. 3. A run then yield to B again. 4. Now at the beginning, setConsumed() called; because B is not runnable, so return_now=true and setConsumed() called again at the end. For cooperative threads, this indeed shouldn't happen but it depends. For example if B can block, then great care should be taken to forbid this edge case. Regards, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi, Thanks for the observation! It's true that setConsumed should only be called once per kernel entry, and it's not obvious just from the code snippets to observe that this is true. However, the semantics of YieldTo mean that both of these code paths cannot be executed in the same kernel entry. If return_now is true, this means that the current thread will be switched to and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is usually the case if the calling thread YieldTo a lower priority thread, or a thread that is not runnable. On the other hand if return_now is false, the YieldTo resulted in the thread being YieldedTo being switched to, so we return the result of the YieldTo on a different kernel entry (when we run the thread that called YieldTo again). With this context, take a look at the if block here: https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 Where you can see that we only set sc->scYieldFrom when we also set return_now to false. Glad to see someone looking at the MCS kernel. Anna.

2 1

The seL4 Foundation is up!
by Heiser, Gernot (Data61, Kensington NSW) 08 Apr '20

08 Apr '20

See my announcement: https://sel4.systems/pipermail/announce/2020/000027.html My blog explains the reasons for it and what we want it to achieve: https://microkerneldude.wordpress.com/2020/04/07/the-sel4-foundation-what-a… And we really want to increase community engagement: here there are plenty of places to contribute: https://docs.sel4.systems/projects/available-user-components.html Gernot on behalf of all of us at Trustworthy Systems

1 0

Cross-core thread migration
by Demi Obenour 06 Apr '20

06 Apr '20

If I have a manycore machine, what is the best way to migrate a thread from one core to another? Similarly, how can I send a capability (such as to memory)? Cryptography is an option for the second one, but seems inelegant and inefficient. Alternatively, are future versions of seL4 expected to scale to manycore systems without needing a multikernel? That would presumably make the answer trivial. Sincerely, Demi

1 0

setConsumed() in seL4_SchedContext_YieldTo
by laokz 06 Apr '20

06 Apr '20

Hello, In kernel/src/object/schedcontext.c, setConsumed(sched_context_t *sc, word_t *buffer) does reset sc->scConsumed and overwrite ksCurThread- >msgRegisters[0] no matter who calls it. So in my understanding, it should be called only once in a syscall path, otherwise prior call info must lost. seL4_SchedContext_YieldTo's actual function invokeSchedContext_YieldTo() has the beginning: ``` if (sc->scYieldFrom) { schedContext_completeYieldTo(sc->scYieldFrom); assert(sc->scYieldFrom == NULL); } ``` and at its end: ``` if (return_now) { setConsumed(sc, buffer); } ``` Because schedContext_completeYieldTo actually called setConsumed(), so here might produce twice calling of setConsumed(). I don't know the practice usage of this method and can't tell it is trivial or not. From coding view, here exists the edge case. Regards, laokz

2 1

CAmkES, Virtual Machines and Multicore Guarantees
by Demi M. Obenour 01 Apr '20

01 Apr '20

> On 18 Mar 2020, at 10:13, Demi Obenour <demiobenour(a)gmail.com> wrote: > > On Tue, Mar 17, 2020, 9:29 PM Klein, Gerwin (Data61, Kensington NSW) < > Gerwin.Klein(a)data61.csiro.au> wrote: > >> >> >> > On 18 Mar 2020, at 08:59, Demi Obenour <demiobenour(a)gmail.com> wrote: >> > >> > On Tue, Mar 17, 2020, 7:32 PM Mcleod, Kent (Data61, Kensington NSW) < >> > Kent.Mcleod(a)data61.csiro.au> wrote: >> > >> > The closest you could get to a multicore system that leverages verified >> >> kernel configurations would be to setup a multikernel implementation >> where >> >> each core had its own instance of a verified seL4 configuration where >> any >> >> hardware resources are strictly partitioned between them. I'm not >> aware of >> >> any examples of this setup but there have been research projects that >> have >> >> used multikernel implementations of seL4 in the past. Also this still >> >> wouldn't give you an overall system with the same guarantees as a >> single >> >> seL4 as the different instances would need to trust each other to not >> >> overwrite each other's kernel data structures and is outside of the >> current >> >> proof assumptions. >> >> >> > >> > Assuming that the root tasks drop capabilities that could be >> problematic, >> > would this still be correct? This seems to follow from the existing >> seL4 >> > specification (no way to get rights to memory from nothing). >> >> You can set up a system to be completely separated from the root task, >> and yes, that would increase confidence. There was a PhD thesis a while ago >> that had a semi-formal but fairly rigorous argument for why and how this >> will work, but you’d still not be running the verified configuration of the >> kernel, i.e. you’d have code in there that was not verified, even if that >> code doesn’t do much in this setup and you can probably convince yourself >> manually that it is fine. >> > > Since the code is deterministic, and will only ever have one initial > condition, is it possible to prove it correct by simply running the binary > and looking at the state after it executes? That is, this code could be > viewed as an extension of the kernel init code. > > > That would work per system, yes, although you’d have to re-do that > certification every time you tweaked something in the setup of that system. > > We’ve thought about this approach also for kernel initialisation in > general, i.e. writing an automated check that the invariants are true after > the system is initialised. There are a lot of expensive calculations in > that check, though, so we haven’t really gone with that. Still remains an > option, though. (Expensive, because the invariants have things like “for > every cap, if there exists another cap to the same object, this cap must > have the following properties” etc, ie. lots of forall/exists combinations > over all of memory, which are no problem in logic, but hard on > computation). > > You’d also still have kernel code that runs later that is not verified, > mostly very simple stuff such as instead of a current thread, you have an > array of current threads (one per CPU). The PhD thesis[1] did look at that > and concluded it’s all fine, but compared to a full code-level verification > that’s obviously lower assurance. The thesis is from 2013, so a lot has > happened since then, but the general idea still holds. > > [1]: > https://ts.data61.csiro.au/publications/nictaabstracts/vonTessin:phd.abstra… > > > > > Also, why is verifying fine-grained locking so difficult? CertiKOS >> managed >> > to do it, so I am probably missing something. >> >> I don’t see that much fine-grained locking in CertKOS, it mostly uses >> separation. It’s easier for it to do so, because it has a significantly >> simpler API (in fact, it’s probably quite similar to a multikernel setup in >> seL4 + messaging between cores. The only setups I’ve seen have precisely >> one VM per core). >> > > I was not aware of that, thank you. > > > It seems to be even worse, actually -- according to the paper that Gernot > posted there is no communication between cores, which if I think back to > the projects I’ve seen is actually true there as well, they used shared > memory between VMs to communicate, not kernel primitives. It also has > cooperative scheduling which is fine for some systems, but not others. It’s > notoriously hard to figure out what features CertiKOS actually has, because > the papers of course concentrate on other aspects such as verification (as > do ours, it’s probably not that easy to figure out what is verified in > which version of seL4 either without a lot of reading, but we do try to be > explicit about it :-)). > > Gernot is obviously not very happy with them from a systems perspective. > From the verification side, they have done some pretty cool things, just > not to the systems level that Gernot would find acceptable ;-) > > > Thank you so much. I view seL4 as universal, in that it should be > possible to build virtually any desired OS on top of it, and I am glad that > a high-performance multicore version with fine-grained locking at least > appears feasible. > > > It’s definitely part of the vision. There is a lot of thinking about > fine-grained vs big-lock, because the seL4 big-lock is about the order of a > Linux fine-grained lock, with some caveats, but the idea is that we want > this to scale. Is it planned to scale beyond the area of small inter-core communication costs? Obviously, transferring large amounts of data between cores on hot paths won't scale. However, I am still not convinced that a multikernel is the best way to go: it has always seemed like a hack to work around kernel limitations, and it seems to make slow-path control-plane userspace code far more complex. Such code often isn't performance critical at all, so forcing it to be distributed seems like unnecessary complexity. Furthermore, replicating data structures (such as page tables) which are almost entirely read-only seems like it could create substantial overhead, although I am not sure if that is an issue in practice. Finally, as someone who writes Rust professionally, I find thread-affine APIs to be quite annoying to deal with. Resources that can't be safely accessed by more than one thread concurrently are easy to wrap in clean APIs, but resources that can't be sent across threads are much harder to wrap. Making kernel resources specifically per-core, and preventing them from being transferred between cores, seems likely to lead to a bunch of userspace frameworks of varying quality that try to work around this limitation. > Are there any papers that I could read to learn more? > > > We don’t have anything really published yet on the verification side, > because it’s all still ongoing work. There is one about the big-lock idea, > though: > > https://ts.data61.csiro.au/publications/nictaabstracts/Peters_DEH_15.abstra… I read and like that idea. My biggest worry, however, is that a big lock won't scale beyond a small number of cores. The idea that fine-grained locking might be possible to verify gives me hope, as I had previously given up on that. > Cheers, > Gerwin Cheers, Demi=

2 1

Get/Set multiple message registers with the one syscall?
by Ben Ph 01 Apr '20

01 Apr '20

I'm looking at `seL4_GetMR()` and `seL4_SetMR()`, which requires a syscall for each get/set. To my naive eye, it seems like you're much better off running `seL4_GetIPCBuffer()->msg` then reading/writing to each index as needed, turning multiple syscalls (one for each get/set) into just the one. Am I missing anything? I was planning on replacing my Get/Set calls with direct array writes, but I'm wondering if I've missed reasons why I shouldn't. Thanks, Ben

2 2

Running cmakes-arm-vm under QEMU.
by Travis Wheatley 01 Apr '20

01 Apr '20

Greetings sel4 developers. Thus far I have successfully been able to build and boot the cmakes-arm-vm project on a Jetson TK1 board. However, my project requires a 64 bit target. I have built the TX1 version of this project but unfortunately do not have a TX1 board to try it out on. I would like to be able to run under QEMU but am not quite sure how to assemble all of the bits needed to do so. I believe what I need is a raw kernel image, a ramdisk, and a dtb file but not sure how to extract these in the proper formats from the files produced in the build process. Is there any existing documentation or guidance that can help me get a 64 bit buildroot kernel running under an sel4 vm to boot under QEMU? — Travis

2 1

Thank you very much. 答复: question about stash and pop between templates
by yadong.li 23 Mar '20

23 Mar '20

-----邮件原件----- 发件人: Matthew Fernandez [mailto:matthew.fernandez@gmail.com] 发送时间: 2020年3月22日 2:00 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] question about stash and pop between templates I think I wrote the text you’re quoting, so I’ll attempt an answer. In connection templates, ‘me’ is not unique. I can’t remember exactly how this works, but ‘me’ either refers to the component instance of the end of the template you’re instantiating or to the connection itself. If you want to try and unravel the relevant code, it’s around lines 278-300 of the main function [0]. The ‘stash’ and ‘pop’ functions were implemented to expose some internals to advanced CAmkES users who wanted functionality beyond the template API. They were not widely used, and many of these users sidestepped them and used the even more questionable ‘_stash’ and ‘_pop’ variants. I would not be surprised if they do not work the way the documentation describes, and they should mostly be considered foot guns at this point. This is based on my ~5 year old memories so may be inaccurate or out of date. HTH [0]: https://github.com/seL4/camkes-tool/blob/master/camkes/runner/__main__.py#L… > On Mar 20, 2020, at 22:56, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi， > Recently, I try to learning about CMAKES > I have some question about stash and pop described as followes: > > “ > Passing Information Between Templates > You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” > What is the meaning of “between templates that share related me references.” ? > It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: > connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from > ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ > where can I found the code to share related ‘me’ between the instance. > > Thanks for your answer _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

question about stash and pop between templates
by yadong.li 22 Mar '20

22 Mar '20

Hi， Recently, I try to learning about CMAKES I have some question about stash and pop described as followes: “ Passing Information Between Templates You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” What is the meaning of “between templates that share related me references.” ? It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ where can I found the code to share related ‘me’ between the instance. Thanks for your answer

2 1

Plan to remove support for ARMv6 and KZM/imx31
by Mcleod, Kent (Data61, Kensington NSW) 20 Mar '20

20 Mar '20

We are planning on removing support for the KZM ARM11 platform in order to reduce maintenance burden. We are assuming that this is a dead platform and removing support won't affect anyone but it would be useful to know who if anyone is currently using this platform and how much interest there is in ongoing support. The platform was the original verification target of seL4 over 10 years ago and by now there doesn't appear to be any ways to obtain new hardware. It is starting to require more attention as the physical board we have is starting to intermittently fail independently from the KZM Qemu simulation target. Currently, the KZM platform is the only ARMv6 platform that we support and supporting it requires a few work-arounds for emulating mechanisms that newer hardware supports. Removing this platform also implies removing armv6 support. There is an older discourse topic for discussion on this topic here: https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-…

1 0

Would verifying ARM64 be any more difficult than verifying ARM32 was?
by Demi M. Obenour 19 Mar '20

19 Mar '20

Would verifying seL4 on ARM64 be any more difficult than verifying seL4 on ARM32 was? What about other architectures like POWER9? I hope I am not asking too many questions; I am just a curious outsider who hopes they can use seL4 someday. Sincerely, Demi

4 3

CAmkES, Virtual Machines and Multicore Guarantees
by Turner, Ben 18 Mar '20

18 Mar '20

Hi, In the seL4 FAQ section it states: "Multicore is presently supported on x64 and Arm v7 (32-bit) and v8 (64-bit). Verification of the multicore kernel is in progress (but presently as an unfunded background activity)." Considering only seL4 ----------------------------- My interpretation of this is that given a single seL4 application running on a device, it is not possible to currently guarantee the protections seL4 provides if the application invokes multiple threads across more than 1 core. Is this correct? Considering CAmkES ---------------------------- I would also like to know how CAmkES affects this. For example, looking at the vm_multi app for the exynos5422 in the camkes-arm-vm repository, what would the effect be of assigning unique CPU affinities to each of the VM components? Do the guarantees still hold in this situation? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

5 4

Configuring pinmux in am335x (beaglebone) can't be done from user mode
by Stephen Sherratt 18 Mar '20

18 Mar '20

Hi all, I've been experimenting with seL4 running on a Ninjablocks (https://www.engadget.com/2013/05/01/ninja-blocks/) that I had lying around. Inside there is a beaglebone, with a custom shield (or cape) containing a microcontroller (atmega328p), some LEDs and a radio. The beaglebone (which normally runs linux) sends json-encoded commands over a serial connection to the on-cape microcontroller, which runs firmware that decodes these commands and controls the LEDs and radio. The complication is that the am335x pins connected to the custom shield are multiplexed, and don't connect to a uart device by default (they are gpio pins by default). The "Control Module" in the am335x can be used to configure pin multiplexing, but it can't be written to in user-mode. From the am335x manual (http://www.ti.com/lit/ug/spruh73q/spruh73q.pdf, page 1449): "Note: For writingto the controlmoduleregisters,the MPUwill need to be in privileged modeof operationand writes will not work fromusermode." To test that the rest of my app works I added the control module to the beaglebone device tree overlay and hacked the kernel to configure the relevant pins to connect to the uart device during boot: https://github.com/stevebob/seL4/commit/4295035ac7fd720fb531b7e0893f1f1191e… And now I have a little rootserver that can control the colours of LEDs on the shield: https://github.com/stevebob/sel4ninja/blob/master/apps/hello-ninja/src/main… What would be the right way of configuring the control module in a seL4-based system, given that it has to happen in kernel mode? To configure the uart pins when running linux on the board, I had to add the following to the device tree: scm@0 { ... pinmux@800 { ... pinmux_uart0_pins { // <-- this was already here pinctrl-single,pins = <0x170 0x30 0x174 0x00>; phandle = <0x20>; }; pinmux_uart1_pins { // <-- I had to add this pinctrl-single,pins = <0x180 0x30 0x184 0x00>; phandle = <0x60>; }; The (seL4) kernel build system already has basic support for interpreting device trees. Would a reasonable solution to my problem be extending this support with a minimal statically-generated control module driver that configures pinmux during boot based on the device tree? There would still be a problem where each board could only have a single pinmux config (as specified by that board's device tree). It seems like an easy fix for this would be a config variable passed to the build system (similar to -DPLATFORM) that overrides the default device tree file. That way projects that want non-standard pinmux configs could bring their own device trees. Cheers, Steve

2 1

seL4 design principles
by Heiser, Gernot (Data61, Kensington NSW) 15 Mar '20

15 Mar '20

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use. https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/ Gernot

3 4

intel-vtd.c::vtd_get_n_paging looks so suspicious
by laokz 15 Mar '20

15 Mar '20

Hello all, kernel/src/plat/pc99/machine/intel-vtd.c::vtd_get_n_paging() confused me a lot. Wish to get any help. This func intends to calculate paging pages needed for all RMRRs. The following code 'filter the identical regions by pci bus id', and use them to figure out the final result. ``` for (word_t i = 1; i < rmrr_list->num; i++) { if (vtd_get_root_index(rmrr_list->entries[i].device) != vtd_get_root_index(filtered.entries[filtered.num - 1].device) && rmrr_list->entries[i].base != filtered.entries[filtered.num - 1].base && rmrr_list->entries[i].limit != filtered.entries[filtered.num - 1].limit) { filtered.entries[filtered.num] = rmrr_list->entries[i]; filtered.num++; } } ``` But vtd_map_reserved_page() says, every different devices(with diff bus-dev- func ID) have their own paging structures. Then why do filter here like this , yet the logic looks so confusing. And on line 313, it counts pages according to the specified level address bits. ``` size += get_n_paging(region, 32 - (VTD_PT_INDEX_BITS * i + seL4_PageBits)); ``` So what does 32 mean? Maybe a typo? Thanks, laokz

2 2

Using sel4.xml/sel4arch.xml to generate custom bindings
by Alexandre Mutel 12 Mar '20

12 Mar '20

Hello, I would like to use the sel4.xml API description files to generate custom bindings for a prototype language to interact directly with seL4 without going through libsel4 C API. I assume that the structure of these files could change, which I'm willing to accept, but wanted to know if these files are here to stay in the future? I understand also that I will still have to parse libsel4 C headers to recover the full API which I'm fine with too. Do you see any trouble following this approach or would you recommend something else?

2 1

May be an error in "alloc_free_io_port_range" of projects/seL4_projects_libs/libsel4vmmplatsupport/src/ioports.c
by yadong.li 12 Mar '20

12 Mar '20

Hi: background: I run virtio_net and virt_con in the lastest version, it is run OK, but I try to add another virito blk, I meet run error below: "Unhandled offset of 0x400 of size 4, reading Assertion failed: !"panic" (/home/yadong.li/seL4_vm_11/sel4_horizon/camkes-arm-vm/projects/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_in: 71)" I add print on my enviornmen, found: ********************start[0x1000], end[0x1400] /*net*/ ********************start[0x1400], end[0x1800] /*con*/ ********************start[0x1800], end[0x1c00] /*blk*/ ---------------------------virtio_con_io_in, con = 0x55f3238, offset = 0x400[0x1800:0x1400] port_no:1800 should belong "blk", but it recongnize as belong "con"(con may be not use the offset 0 feature), the boundary may be have some problem the function: static int alloc_free_io_port_range(vmm_io_port_list_t *io_list, ioport_range_t *io_range) { uint16_t free_port_addr = io_list->alloc_addr; if (free_port_addr + io_range->size < free_port_addr) { /* Possible overflow */ return -1; } io_list->alloc_addr += io_range->size; io_range->start = free_port_addr; io_range->end = free_port_addr + io_range->size; return 0; } I think "io_range->end = free_port_addr + io_range->size;" should change to "io_range->end = free_port_addr + io_range->size - 1;" ? Thank you very much!

2 1

Booting on a Jetson TK1 board.
by Travis Wheatley 12 Mar '20

12 Mar '20

Hello all, I am spinning up on sel4 and having difficulty booting a kernel on a Jetson TK1 board. I have successfully downloaded the cmakes repo and can build the x86 version of the code and run it as a simulation. I can also successfully build the TK1 version by changing the -DARCHETECTURE argument passed to init-build.sh to “tk1”. This results in a single image file named “capdl-loader-image-arm-tk1” to show up in my images folder (as opposed to both a kernel image and “userland” image that get created in the x86 version). So… I put that image on an SD card, plug it into the TK1, boot to a uboot prompt, and load the image using the command “fatload mmc 1 0x82000000 <filename>”. I can use “md” to see that the image is actually loaded properly. However, when I type “go 0x82000000” I see no output what so ever going out of the serial port. What I expect to see is similar output to what was displayed in the x86 simulation. I posted the question to the IRC channel yesterday and someone suggested using bootm or bootelf. No luck with either of these. So… hoping someone here might be able to give me a clue. — Travis

2 4

L4 Risc-v touchscreen board
by Luca Tapponi 27 Feb '20

27 Feb '20

I am newby in this sector and involved in a project to create a prototype (hardware and software) based on risc-v cpu and running L4-based microkernel. I need to control and program an attached touchscreen where I can create a simple graphic user interface too. I would appreciate any suggestion that bring me on the right road. Board should embed wi-fi network too. First step is to find the right hardware and second is to have development tools/environment to program the board. As much as possible open licensing should be adopted because the project falls in IT security solution and want to avoid any hidden backdoors. Thank you in advance. Best regards, Luca

1 0

devices.camkes: vm#.untyped_mmios: What does the integer after the addresses in this array represent?
by Turner, Ben 27 Feb '20

27 Feb '20

Hi all, As stated in the question, I'm not certain about how the integer part of the elements in the untyped_mmios array in devices.camkes are derived? E.g. in the TX2 devices.camkes file: vm0.untyped_mmios = [ "0x3886000:12", // GICV Iface. /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to guest-vm@f1000000 in the overlay DTS */ "0xF1000000:24", "0xF2000000:25", "0xF4000000:26", "0xF8000000:24", ]; I recognise that the range of addresses here covers the VM_RAM_SIZE specified, and so the pattern that emerges is: 24 --> 0x01000000 25 --> 0x02000000 26 --> 0x04000000 And so the above would cover the range 0xf1000000 --> 0xf9000000, which is the range of memory specified for the VM. Is this simply a case of the integer representing double the value with each increment. E.g: Integer Int Rep Hex 0 1 0x0000_0001 1 2 0x0000_0002 2 4 0x0000_0004 3 8 0x0000_0008 4 16 0x0000_0010 5 32 0x0000_0020 6 64 0x0000_0040 7 128 0x0000_0080 8 256 0x0000_0100 9 512 0x0000_0200 10 1024 0x0000_0400 11 2048 0x0000_0800 12 4096 0x0000_1000 13 8192 0x0000_2000 14 16384 0x0000_4000 15 32768 0x0000_8000 16 65536 0x0001_0000 17 131072 0x0002_0000 18 262144 0x0004_0000 19 524288 0x0008_0000 20 1E+06 0x0010_0000 21 2E+06 0x0020_0000 22 4E+06 0x0040_0000 23 8E+06 0x0080_0000 24 2E+07 0x0100_0000 25 3E+07 0x0200_0000 26 7E+07 0x0400_0000 27 1E+08 0x0800_0000 28 3E+08 0x1000_0000 29 5E+08 0x2000_0000 30 1E+09 0x4000_0000 31 2E+09 0x8000_0000 Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

3 2

two questions when I add virtio net with virtio_console meanwhile in arm-vm project
by yadong.li 24 Feb '20

24 Feb '20

hi, I had make virtio_console work OK on my environment（armv8）, But I meet two question when I add virtio net with virtio_console meanwhile. Question1: "add_io_port_range@io.c:111 Requested ioport range 0x6200-0x6600" for VIRTIO CON overlaps with existing range 0x6200-0x6600 for VIRTIO PCI NET According to the print above: common_make_virtio_con(virtio_emul_vm, vm->pci, vm->io_port, VIRTIO_IOPORT_START, VIRTIO_IOPORT_SIZE, VIRTIO_INTERRUPT_PIN, VIRTIO_CON_PLAT_INTERRUPT_LINE, backend); common_make_virtio_net(virtio_emul_vm, vm->pci, vm->io_port, VIRTIO_IOPORT_START + 0x1000, VIRTIO_IOPORT_SIZE, VIRTIO_INTERRUPT_PIN, VIRTIO_NET_PLAT_INTERRUPT_LINE, backend); a、above two function，I found they use the same VIRTIO_IOPORT_START， I modify VIRTIO_IOPORT_START of common_make_virtio_net to （VIRTIO_IOPORT_START + 0x1000）, is it OK? b、I also found（VIRTIO_CON_PLAT_INTERRUPT_LINE == VIRTIO_NET_PLAT_INTERRUPT_LINE）,is that OK? Whether it should be make interrupt line different ? Question2: "_utspace_split_alloc@split.c:272 Failed to find any untyped capable of creating an object at address 0xc0001000 Failed to find device cap for 0xc0001000" According to the print above: a、my PCI region define as below: #define PCI_CFG_REGION_ADDR 0xC1000000 #define PCI_IO_REGION_ADDR 0xC0000000 #define PCI_CFG_REGION_SIZE 0x1000000 #define PCI_IO_REGION_SIZE 0x1000 #define PCI_CFG_BAR_MASK 0xFFFFFFFF I found 'virtio_net_init' and 'virtio_console_init' will call the same function 'install_virtio_vpci_device', net and console will have the same PCI_IO_REGION_ADDR ? is it OK? b、If I want to support two or muti virtio device, which should I add a new macro define for virtio_net in a? for example add PCI_IO_REGION_ADDR for net or add PCI_CFG_REGION_ADDR ? c、Can you give me some list file to change for support for support net and console meanwhile? Thank you very much.

2 2

Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b
by Turner, Ben 21 Feb '20

21 Feb '20

Hi, I have been attempting to add support for the Raspberry Pi 3 b platform so that I can run the vm_minimal application on it. The platform supports ARM_HYP, so I believe it should be possible to get this working. I have reached to point where ninja errors on an implicit declaration for `set_gic_vcpu_ctrl_hcr`. From what I understand, this is to do with the ARM Generic Interrupt Controller, however the RPi3b doesn't have a GIC, it has a `bcm2836-armctrl-ic`. This occurs because the file vcpu.h defines an inline function that calls this function, however as the RPi3b doesn't have a GIC, neither the gic_v2.h or gic_v3.h files are provided in the build environment, and hence the build fails. I am unsure what this means in terms of implementation. What needs to be added or changed to get this compiling for the RPi3b? Thanks in advance Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

3 9

Announcing new releases: seL4-11.0.0, camkes-3.8.0, CapDL-0.1.0,
by Mcleod, Kent (Data61, Kensington NSW) 21 Feb '20

21 Feb '20

Announcing the releases of seL4, CAmkES, CapDL and updates of other supporting projects. **Note that this announcement refers to a series of release commits that occurred on 19-Nov-2019.** See below for links to release notes. In addition there are new ways to discuss seL4 and trustworthy systems: - seL4 Discourse at <https://sel4.discourse.group>, a forum for attempting to build up an seL4 knowledge base. - seL4 Mattermost at <https://mattermost.ts.data61.csiro.au/sel4-external/> for online messaging. (Signup link can be found on seL4 Discourse:<https://sel4.discourse.group/t/sel4-mattermost-sign-up-link/125> with a valid account). - seL4 RFCs at <https://sel4.atlassian.net/projects/RFC> for open discussion about major changes to the seL4 ecosystem. For more information see: <https://docs.sel4.systems/processes/#contact> Versioned Releases * seL4 11.0.0: The seL4 microkernel <https://docs.sel4.systems/releases/sel4/11.0.0> * CAmkES camkes-3.8.0: Component Architecture for microkernel-based Embedded Systems <https://docs.sel4.systems/releases/camkes/camkes-3.8.0> * CapDL 0.1.0: Collection of tools for generating, parsing and loading CapDL specifications of systems <https://docs.sel4.systems/releases/capdl/0.1.0> Update notes * seL4 Buildsystem: System configuration and building using mostly CMake <https://docs.sel4.systems/updates/buildsystem/11.0.x.html> * seL4Test: Test suite for seL4 <https://docs.sel4.systems/updates/sel4test/11.0.x.html> * sel4bench: sel4bench contains benchmarking applications and a support library for seL4 <https://docs.sel4.systems/updates/sel4bench/11.0.x.html> * user_libs: Userlevel libraries on seL4 <https://docs.sel4.systems/updates/user_libs/11.0.x.html> * The seL4 Run-time: A minimal runtime for running a C or C-compatible process in a minimal seL4 environment <https://docs.sel4.systems/updates/sel4runtime/11.0.x.html> * Elfloader: For preparing the hardware for seL4 on ARM and RISC-V <https://docs.sel4.systems/updates/elfloader/11.0.x.html> * seL4 tutorials: Collection of tutorials for learning to use seL4 and its ecosystem <https://docs.sel4.systems/updates/sel4-tutorials/camkes-3.8.x.html> * camkes-vm: x86 Virtual Machine build as a CAmkES component <https://docs.sel4.systems/updates/camkes-vm/camkes-3.8.x.html> * camkes-arm-vm: Arm Virtual Machine build as a CAmkES component <https://docs.sel4.systems/updates/camkes-arm-vm/camkes-3.8.x.html> * seL4webserver: A reference for implementing applications on seL4 <https://docs.sel4.systems/updates/sel4webserver/camkes-3.8.x.html> An seL4 discourse version of this email can be found at: <https://sel4.discourse.group/t/19-november-2019/126>

1 0

Re: [seL4] Multikernels and resource transfer
by Ge, Qian (Data61, Kensington NSW) 14 Feb '20

14 Feb '20

In a multikernel setup, each kernel manages its own memory allocation, as the main memory is distributed among all valid kernels. Hence, the described scenario does not apply. Regards, Qian. Message: 1 Date: Thu, 13 Feb 2020 00:49:11 -0500 From: Demi Obenour <demiobenour(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] Multikernels and resource transfer Message-ID: <CAJEMUN_L49O9btYx03Z35uQ6S21T80wPujP86Gd5XyymH4BQ6g(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency? Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi

1 0

Multikernels and resource transfer
by Demi Obenour 13 Feb '20

13 Feb '20

In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency? Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi

1 0

Beginner ARM_HYP questions
by tossel＠gmail.com 12 Feb '20

12 Feb '20

Greetings, I'm trying to understand how hypervisor functionality support is working in seL4 for aarch32/aarch64. In the documentation there is a list of platforms [1] for some of them ARM_HYP is said to be supported for some not. I was trying to grep through the kernel, but it seemed to me that ARM_HYP can be enabled on any ARM-based platform. I've tried to compile sel4test for exynos5422 (for which ARM_HYP is said to be enabled) and odroidc2 (for which it is said that it's not supported) with -DARM_HYP=ON manually set, and for both compilation succeeded. It failed for hikey, that should support it, but that's a different story. So my questions are - How is it defined whether ARM_HYP is supported for a board/SoC, provided that processor architecture supports it? What the platform support code should provide for hypervisor to work? - For platforms not supported by camkes-arm-vm (like, most of the platforms) how ARM_HYP can be tested? Thanks a lot, Anton Gerasimov [1] https://docs.sel4.systems/Hardware/

2 2

(no subject)
by abdi mahmud haji 11 Feb '20

11 Feb '20

hello can someone help me here what did i do wrong ,i have been trying to do camkes-vm-linux and i have followed the instruction on sel4-tutorials when i run ninja to build the file i have got an error as below ========================================================================== ninja [5/127] Building C object camkes-vm-li...ents/Init/src/virtio_net_vswitch.c.obj FAILED: ccache /usr/bin/gcc --sysroot=/home/sel4/sel4-tutorials-manifest/camkes-vm-linux_build -I../projects/camkes/vm/components/Init/src -I../projects/camkes/vm/components/VM/configurations -Icamkes-vm-linux/vm0/include -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/x86 -I../kernel/libsel4/sel4_arch_include/x86_64 -I../kernel/libsel4/sel4_plat_include/pc99 -I../kernel/libsel4/mode_include/64 -Ilibsel4/include -Ilibsel4/arch_include/x86 -Ilibsel4/sel4_arch_include/x86_64 -I../projects/sel4runtime/include -I../projects/sel4runtime/include/mode/64 -I../projects/sel4runtime/include/arch/x86 -I../projects/sel4runtime/include/sel4_arch/x86_64 -Iprojects/musllibc/build-temp/stage/include -Ilibsel4/autoconf -Ikernel/gen_config -Ilibsel4/gen_config -I../tools/camkes/libsel4camkes/include -I../projects/seL4_libs/libsel4debug/include -I../projects/seL4_libs/libsel4debug/arch_include/x86 -I../projects/seL4_libs/libsel4debug/sel4_arch_include/x86_64 -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/x86 -Iprojects/util_libs/libutils/gen_config -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/pc99 -I../projects/util_libs/libplatsupport/arch_include/x86 -Iprojects/util_libs/libplatsupport/gen_config -I../projects/seL4_libs/libsel4muslcsys/include -I../projects/util_libs/libcpio/include -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utils/arch_include/x86 -I../projects/seL4_libs/libsel4vspace/include -I../projects/seL4_libs/libsel4vspace/arch_include/x86 -I../projects/seL4_libs/libsel4vka/include -I../projects/seL4_libs/libsel4vka/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4vka/arch_include/x86 -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -I../projects/seL4_libs/libsel4simple/include -I../projects/seL4_libs/libsel4simple/arch_include/x86 -I../projects/seL4_libs/libsel4platsupport/include -I../projects/seL4_libs/libsel4platsupport/arch_include/x86 -I../projects/seL4_libs/libsel4platsupport/plat_include/pc99 -I../projects/seL4_libs/libsel4simple-default/include -I../projects/util_libs/libelf/include -Iprojects/seL4_libs/libsel4muslcsys/gen_config -I../projects/seL4_libs/libsel4sync/include -I../projects/projects_libs/libvirtqueue/include -Icamkes-vm-linux/libsel4camkes/gen_config -Iprojects/sel4runtime/gen_config -I../projects/seL4_libs/libsel4allocman/include -I../projects/seL4_libs/libsel4allocman/sel4_arch/x86_64 -I../projects/seL4_libs/libsel4allocman/arch/x86 -I../projects/seL4_libs/libsel4vmm/include -I../projects/util_libs/libpci/include -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/pc99 -I../projects/util_libs/libethdrivers/arch_include/x86 -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/liblwip/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Icamkes-vm-linux/vm/gen_config -I../projects/projects_libs/libvswitch/include -I../projects/camkes/global-components/components/FileServer/libFileServer-client/. -m64 -march=nehalem -D__KERNEL_64__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mtls-direct-seg-refs -Wno-main -std=gnu11 -MD -MT camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj -MF camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj.d -o camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj -c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch_send’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:50:23: warning: implicit declaration of function ‘virtqueue_driver_dequeue’ [-Wimplicit-function-declaration] int dequeue_res = virtqueue_driver_dequeue(node->virtqueues.send_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘emul_raw_tx’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:123:13: error: unknown type name ‘virtqueue_t’ virtqueue_t *destbuff; ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:147:19: warning: implicit declaration of function ‘virtqueue_driver_enqueue’ [-Wimplicit-function-declaration] err = virtqueue_driver_enqueue(destnode->virtqueues.send_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:157:19: warning: implicit declaration of function ‘virtqueue_driver_signal’ [-Wimplicit-function-declaration] err = virtqueue_driver_signal(destnode->virtqueues.send_queue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:170:17: warning: implicit declaration of function ‘virtqueue_driver_poll’ [-Wimplicit-function-declaration] if (virtqueue_driver_poll(destnode->virtqueues.send_queue) == 1) { ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch_recv’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:215:5: error: unknown type name ‘virtqueue_t’ virtqueue_t *rxdata_buff; ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:234:23: warning: implicit declaration of function ‘virtqueue_device_dequeue’ [-Wimplicit-function-declaration] int dequeue_res = virtqueue_device_dequeue(node->virtqueues.recv_queue, ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:249:27: warning: implicit declaration of function ‘virtqueue_device_enqueue’ [-Wimplicit-function-declaration] enqueue_res = virtqueue_device_enqueue(node->virtqueues.recv_queue, available_buff, available_buff_sz); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:275:11: warning: implicit declaration of function ‘virtqueue_device_signal’ [-Wimplicit-function-declaration] err = virtqueue_device_signal(node->virtqueues.recv_queue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘virtio_net_notify_vswitch’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:292:17: warning: implicit declaration of function ‘virtqueue_device_poll’ [-Wimplicit-function-declaration] if (virtqueue_device_poll(g_vswitch.nodes[i].virtqueues.recv_queue) == 1) { ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function ‘make_vswitch_net’: ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:312:44: warning: passing argument 1 of ‘camkes_virtqueue_driver_init’ from incompatible pointer type [-Wincompatible-pointer-types] err = camkes_virtqueue_driver_init(&send_virtqueue, mac_mapping.send_id); ^ In file included from ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0: ../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:64:5: note: expected ‘virtqueue_driver_t * {aka struct virtqueue_driver *}’ but argument is of type ‘virtqueue_driver_t ** {aka struct virtqueue_driver **}’ int camkes_virtqueue_driver_init(virtqueue_driver_t *driver, unsigned int camkes_virtqueue_id); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:317:44: warning: passing argument 1 of ‘camkes_virtqueue_device_init’ from incompatible pointer type [-Wincompatible-pointer-types] err = camkes_virtqueue_device_init(&recv_virtqueue, mac_mapping.recv_id); ^ In file included from ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0: ../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:72:5: note: expected ‘virtqueue_device_t * {aka struct virtqueue_device *}’ but argument is of type ‘virtqueue_device_t ** {aka struct virtqueue_device **}’ int camkes_virtqueue_device_init(virtqueue_device_t *device, unsigned int camkes_virtqueue_id); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:320:13: warning: implicit declaration of function ‘camkes_virtqueue_driver_free’ [-Wimplicit-function-declaration] camkes_virtqueue_driver_free(send_virtqueue); ^ ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:333:13: warning: implicit declaration of function ‘camkes_virtqueue_device_free’ [-Wimplicit-function-declaration] camkes_virtqueue_device_free(recv_virtqueue); ^ [5/127] Building C object camkes-vm-li...MakeFiles/sel4camkes.dir/src/dma.c.obj ninja: build stopped: subcommand failed. ================================================================== and why this happing

2 1

Problem booting camkes arm vmm on TK1 from SD Card
by Mike Clark 11 Feb '20

11 Feb '20

I'm using the docker image to build the CAmkES ARM VMM project using roughly the instructions here: https://docs.sel4.systems/VM/CAmkESARMVM.html (they are slightly out of date). I do: ../init-build.sh -DAARCH32=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1 ninja Then I copy the resulting image from the images directory to an SD card and put that in my TK1. When U-Boot starts I use the following commands to try to boot fatload mmc 1 0x10000000 capdl-loader-image-arm-tk1 bootelf 0x10000000 To which I get an error: No elf image at address 0x10000000 I tried with an older version of U-Boot (that worked following this same procedure about a year ago). It is U-Boot SPL 2014.10-rc2-g3127911 (Jun 07 2016 - 21:00:01) I also tried updating U-Boot to U-Boot SPL 2020.01-00442-gc00bd81ae0 (Jan 10 2020 - 11:10:18 -0500). Same error. Any thoughts or suggestions on how I get this to boot?

4 14