November 2020 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 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 15 Oct '24

15 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 18 May '23

18 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

whether seL4 support c++ code
by yadong.li 02 Dec '20

02 Dec '20

Hi， I have two questions about whether seL4 support C++: 1. When we create a component, whether the src file of component can be c++ style file like **.cxx, or **.cpp ? I found it will print “camkes.environment.c : undefined reference to run” error when compile 2. If our app code write by c++, how can I use it in seL4 environment as native component？Is there some example ？ Thank you very much.

3 2

Building a simple RISC-V project
by porter.188＠osu.edu 29 Nov '20

29 Nov '20

I am trying to build a simple RISC-V seL4 project. I mean "hello world" simple. I using version 12.0.0. I looked at the documentation here https://docs.sel4.systems/projects/buildsystem/incorporating.html to follow what the project layout is. I also followed this project for x86 v10.0.0. https://github.com/manu88/SeL4_101 I was able rebuild this last one for RISC-V after modifying the CMakeLists.txt to include the proper libraries in my hello project. When I try to use the seL4 12.0.0 kernel there are some configuration differences that I haven't figured out yet. Can anyone shed some light on what the parameters are that need to be set for RISC-V? The verified config in ../kernel/configs/RISCV64_verified.cmake are this, is this all that need set? I suppose these could be modified as necessary. 12 set(KernelSel4Arch "riscv64" CACHE STRING "") 13 set(KernelPlatform "hifive" CACHE STRING "") 14 set(KernelPTLevels "3" CACHE STRING "") 15 set(KernelVerificationBuild ON CACHE BOOL "") 16 set(KernelMaxNumNodes "1" CACHE STRING "") 17 set(KernelOptimisation "-O2" CACHE STRING "") 18 set(KernelRetypeFanOutLimit "256" CACHE STRING "") 19 set(KernelBenchmarks "none" CACHE STRING "") 20 set(KernelDangerousCodeInjection OFF CACHE BOOL "") 21 set(KernelFastpath ON CACHE BOOL "") 22 set(KernelPrinting OFF CACHE BOOL "") 23 set(KernelNumDomains 16 CACHE STRING "") 24 set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "") 25 set(KernelRootCNodeSizeBits 19 CACHE STRING "") 26 set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

2 1

CAmKes Ethdriver Odroid-C2
by Nkem Ogosi 25 Nov '20

25 Nov '20

Hi all, I'm trying to add an odroid-c2 ethdriver implementation and I'm quite confused bout an error im getting. ERROR:CAmkES:CPP failed: /home/nkem/learningHydra/projects/global-components/components/Ethdriver/Ethdriver.camkes:13:10: fatal error: plat/eth_devices.h: No such file or directory ERROR:CAmkES: #include <plat/eth_devices.h> ERROR:CAmkES: ^~~~~~~~~~~~~~~~~~~~ ERROR:CAmkES:compilation terminated. ERROR:CAmkES: CMake Error at /home/nkem/learningHydra/projects/camkes-tool/camkes.cmake:545 (message): Failed to generate /home/nkem/learningHydra/build/ast.pickle Call Stack (most recent call first): It suggests I'm missing the eth_devices header for the odroid-c2 platform but I think I have added all the necessary files in the correct folders. Is there any way to know exactly what files I need or where to look to debug this issue. Thanks, Nkem

2 1

Re: Quotation
by Chubb, Peter (Data61, Kensington NSW) 24 Nov '20

24 Nov '20

>>>>> "Andrew" == Andrew Warkentin <andreww591(a)gmail.com> writes: Andrew> How are these spammers getting onto the list? Is there some Andrew> kind of configuration issue? The person sending it subscribed then unsubscribed. I've temporarily set all messages to moderated to try to catch any others who are doing this. PeterC -- Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group CSIRO's Data61

1 0

Connectivity of 2 sel4 powered systems
by ogosinkem＠gmail.com 23 Nov '20

23 Nov '20

Hi all, I asked earlier about how to connect the odroid-c2 board via Ethernet and I was wondering what additional files I would need to get a CAmkES implementation of an ethernet driver working for this board. Thanks, Nkem Ogosi

1 0