January 2024 - 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

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 14 Aug '24

14 Aug '24

Hi everyone, I am getting a link failure during the build of sel4test-tests: /usr/bin/ld: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a(__stdio_exit.o): copy relocation against non-copyable protected symbol `__stdin_used' collect2: error: ld returned 1 exit status Searching t'interwebs seems to imply this is a gnarly problem caused by the nuances of various build tools - but one that should not apply to Arm. You can summarise everything I did before the build like this: sudo apt install ninja-build libxml2-utils repo pip3 install pyyaml typing hardware pyfdt jinja2 jsonschema six future ply python3-protobuf grpcio-tools cd && mkdir xxx && cd xxx Then to follow your build repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build && cd build ../init-build.sh -DPLATFORM=bcm2711 ninja And yes I know it is not supported and the BCM2711 is for the Pi 4. I am evaluating ;) Any help greatly appreciated. Thanks, Smiley

3 4

fault processing
by Leonid Meyerovich 26 Jan '24

26 Jan '24

I am working on fault processing. When I am a fault I am calling void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char *thread_name) from sel4libsutils library I have tested it for "page fault" condition and it works fine - I am getting seL4_Fault_VMFault fault type But in certain case I have got seL4_Fault_VCPUFault type, which is not implemented sel4libsutils library I try to process this fault similar to seL4_Fault_VMFault to get all neccessary registers, but the kernel does not have functions like seL4_Fault_VCPUFault_get_IP. What is the message format for VCPU fault? Thanks

2 3

seL4 fault processing
by Leonid Meyerovich 25 Jan '24

25 Jan '24

My root task (root thread created by kernel) checks for fault from the other threads, which are created in root thread with badged fault_ep seL4_Word badge; seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap, &badge); if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault ) { process_fault(messageInfo, badge); } Normally I don't have any faults, but every time I have seL4_MessageInfo_get_label(messageInfo) == 4, which is not in seL4_Fault_tag enumeration type enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 }; Could somebody explain? Thanks,

4 5

seL4 root task executable memory region
by Leonid Meyerovich 24 Jan '24

24 Jan '24

I assume that the code segment of the root task starts from __executable_start address. Does it point to ELF header? Or code starts directly from this address? Thank you,

1 0

seL4 fault handling
by Leonid Meyerovich 23 Jan '24

23 Jan '24

Hello, Where can I find a comprehensive description of fault message registers for every of the following faults enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 }; Thanks, LM

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 21 Jan '24

21 Jan '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jan 24, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Gerwin Klein 09 Jan '24

09 Jan '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jan 10, 6pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0