July 2023 - 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

CMake error “Variable 'KernelArch' is not set.” Happens when building RISCV based seL4 system.
by sueboxian＠gmail.com 25 Jul '23

25 Jul '23

Hi, I met a CMake error, “Variable KernelArch is not set” when I tried to build a seL4 project based on the open source code of the UNSW course, Advanced Operating System, aka. AOS. The original version uses odroidc2 as the building platform, and I want to build it with the riscv gnu toolchain and simulate it on qemu-riscv-virt. Here is the repository: https://github.com/SEL4PROJ/AOS-manifest The building hierachy is as the basic build system structure, with init-build.sh, setting.cmake and CMakeLists.txt in the top level. And the top level contains kernel, tools, and project folders, in which there are CMakeLists.txt and .cmake files. Since I have no experience on cmake, I tried to compare the manifest xml between AOS project and seL4test project. I found that the major difference between them are in “init-build.sh”, “setting.cmake” and the “CMakeList.txt” in the top level. There are also some unused libraries in AOS project. I tried deleting the “set PLATFORM odroidc2” command in the setting.cmake, and added the DCROSSCOMPILER=riscv-unknown-linux-gnu, DPLATFORM=qemu-riscv-virt in the build command. But they doesn’t work. After checking the “/kernel/configs/seL4Config.cmake”, it says that the error is caused since KernelArch is left as empty string… And I want to ask whether I have set anything improperly.... I will appreciate for any help. Thank you for reading my question!

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 24 Jul '23

24 Jul '23

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

1 0

Soft-float problem happens when building seL4test using riscv64-unknown-linux-gnu-gcc toolchain
by sueboxian＠gmail.com 15 Jul '23

15 Jul '23

Hi, I met a problem when building seL4test project with riscv toolchain, with the float operations compiled as soft-float. Here are my configuration commands:  python3 ~/bin/repo init -u https://github.com/seL4/sel4test-manifest  python3 ~/bin/repo sync  mkdir build-riscv  cd build-riscv  ../init-build.sh -DPLATFORM=qemu-riscv-virt -DCROSS_COMPILER_PREFIX=riscv64-unknown-linux-gnu- -DSIMULATION=TRUE  ninja The terminal reported "can't link double-float modules with soft-float modules" errors when compiling fpu.c, and thus stopped compilation. I have tried rebuilding the glibc version riscv toolchain, with multilib enabled. But it doesn't work. I also checked the terminal, it says that I'm compiling with march=riscv64imac_zicsr_zifencei -mabi=lp64, which as the best of my knowledge, means compiling the float as soft-float. I want to know whether I lossed something. I would appreciate for any help. Thanks in advance.

3 6

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jul '23

10 Jul '23

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

1 0