- 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