October 2020 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

4 4

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