- Devel - lists.sel4.systems

seL4 developer hangout reminder
by Birgit Brecknell 07 Jul '24

07 Jul '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 9 Jul, 22:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 02 Jul '24

02 Jul '24

We’re pleased to announce the release of - seL4 13.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/13.0.0 - Microkit 1.3.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/1.3.0 - CAmkES 3.11.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.11.0 - capDL 0.3.0: Tools for generating, parsing and loading capability distribution specifications https://… [View More]

1 0

New release of seL4, Microkit, CAmkES, capDL and Rust support
by Gerwin Klein 02 Jul '24

02 Jul '24

We’re pleased to announce the release of - seL4 13.0.0: The seL4 microkernel https://docs.sel4.systems/releases/sel4/13.0.0 - Microkit 1.3.0: The seL4 Microkit for building static-architecture systems https://docs.sel4.systems/releases/microkit/1.3.0 - CAmkES 3.11.0: Component Architecture for microkernel-based Embedded Systems https://docs.sel4.systems/releases/camkes/camkes-3.11.0 - capDL 0.3.0: Tools for generating, parsing and loading capability distribution specifications … [View More]

1 0

seL4 MCS flavour with RISCV
by David Martin 01 Jul '24

01 Jul '24

Hello, I'm trying to understand the current situation of the MCS branch. Our setup: - Microchip Polarfire SoC (1xE51 RV64IMAC + 4xU54 RV64IMAFD) We are starting to "play" with threads but when coming to the scheduling of them, I'm a bit lost. If I understand correctly, the latest version of seL4 (12.1.0) if compatible with RV64IMAFD, so floating point operations included. The latest MCS version (10.1.1-mcs) on the contrary is only RV64IMAC so no FPU support. I haven't seen any MR nor … [View More]

1 0

CPU/ISA tuned specifically for seL4?
by Isaac Beckett 25 Jun '24

25 Jun '24

Hello! I recall reading about old CPUs/ISAs made for Lisp machines, with features and optimized for specifically running Lisp. And I’ve heard people discuss how current CPUs are optimized for C code and similar programming paradigms, and vice versa: C and others are optimized for those CPUs. This got me wondering, what might a CPU or instruction set designed more specifically to run seL4 look like? I’m guessing it might involve capability hardware like CHERI to accelerate seL4’s software … [View More]

3 2

seL4 developer hangout reminder
by Gerwin Klein 23 Jun '24

23 Jun '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 26 Jun, 08:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Success and Effort in seL4 x86_64 Virtualbox
by thomas.j.hampton＠gmail.com 21 Jun '24

21 Jun '24

Hey; configuration is a pretty big space and I didn't see anything specific, and may have bumped into a bug along the way. Here's some details about getting seL4test working, and using the EGA driver on this platform. Here's the commits I'm on: - sel4test 95522e9 - seL4 ddeb18a01 I managed to get seL4test running in VirtualBox on a Tiger Lake chip some weeks ago, not terribly impressive, things worked pretty well, generally. - I discovered that on the platform I needed to … [View More]

2 1

Assertion failure when booting seL4 image on x86 UEFI via Grub
by fennelfoxxo＠gmail.com 15 Jun '24

15 Jun '24

Hello all! This is my first time posting here, but I'll try to provide all the detail I can, and I'm grateful for any advice others have to fix this issue. I've been trying to boot the seL4 Hello World tutorial in QEMU with UEFI support on the x86 platform, with the help of the Grub bootloader. It seems I can load the kernel okay, but an error occurs when the kernel tries to load the rootserver: > seL4 failed assertion 'mods_end_paddr > boot_state.ki_p_reg.end' at /home/fennel/… [View More]grubbuild/stacktest/sel4-tutorials/kernel/src/arch/x86/kernel/boot_sys.c:452 in function try_boot_sys From my research, it seems to be happening because grub is loading the rootserver module at a lower address than expected. These two lines from serial output during boot indeed show that the module end address is lower than the kernel end address: > module #0: start=0x751000 end=0x7954c8 size=0x444c8 name='' > Kernel loaded to: start=0x100000 end=0xc12000 size=0xb12000 entry=0x100298 When running the same hello world project using ./simulate in the build directory, the rootserver module is placed at a higher address and boots ok: > module #0: start=0xc13000 end=0xc574c8 size=0x444c8 name='images/hello-world-image-x86_64-pc99' > Kernel loaded to: start=0x100000 end=0xc12000 size=0xb12000 entry=0x100298 Does anyone know if this is a mistake in how I am compiling and building the project, my QEMU settings, or perhaps an issue with how Grub is handling loading the module? Booting from Grub should be possible in theory (https://docs.sel4.systems/Hardware/IA32.html) so any guidance is appreciated. Thank you! - Fennel STEPS TO REPRODUCE: # Contents of grub.cfg - place in current directory menuentry "Load seL4" --class os { insmod efi_gop insmod efi_uga insmod all_video set root='(hd0,gpt1)' multiboot2 /EFI/BOOT/sel4kernel module2 /EFI/BOOT/sel4rootserver } # End of grub.cfg # Compile Grub 2.06 from source to ./grub-2.06 wget https://ftp.gnu.org/gnu/grub/grub-2.06.tar.gz -O grub.tar.gz # Download grub source tar -xvzf grub.tar.gz -C ./ && rm grub.tar.gz # Unzip and remove original file cd grub-2.06 && ./autogen.sh && ./configure --target=x86_64 --with-platform=efi && make # Configure & compile # Install, configure, and compile hello-world seL4 project to ./sel4-tutorials mkdir sel4-tutorials cd sel4-tutorials repo init -u https://github.com/seL4/sel4-tutorials-manifest # Install tutorials repo sync ./init --plat pc99 --tut hello-world cd hello-world_build cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -DKernelHugePage=OFF -G Ninja . # Disable huge page requirement ninja # Create final image as disk.img mkdir EFI EFI/BOOT grub-2.06/grub-mkimage -d grub-2.06/grub-core -o EFI/BOOT/BOOTX64.EFI -O x86_64-efi -p "" configfile fat part_gpt gzio multiboot video efi_gop efi_uga normal chain boot multiboot2 all_video cp sel4-tutorials/hello-world_build/images/kernel-x86_64-pc99 EFI/BOOT/sel4kernel cp sel4-tutorials/hello-world_build/images/hello-world-image-x86_64-pc99 EFI/BOOT/sel4rootserver cp grub.cfg EFI/BOOT/grub.cfg dd if=/dev/zero of=disk.img bs=1M count=35 # 35MB is just about the smallest FAT32 partition possible mformat -i disk.img@@2048s -v "EFI SYSTEM" -F # Create fat32 partition 2048 sectors in mcopy -i disk.img@@2048s -s EFI :: parted -s disk.img mklabel gpt mkpart '"EFI SYSTEM"' fat32 2048s 100% set 1 esp on # Create partition entry for ESP # Run in QEMU (most of these arguments are copied from the seL4 ./simulate script - replace OVMF path with your path to OVMF_CODE.fd for UEFI boot) qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce -serial mon:stdio -m size=512M -drive if=pflash,format=raw,readonly=on,file=PATH_TO_OVMF_CODE.fd -drive file=disk.img [View Less]

1 0

Unblocking the caller of seL4_Call when the receiver is killed
by Arya Stevinson 12 Jun '24

12 Jun '24

Hello, I'll give a brief introduction since this is my first message here. I'm an undergraduate research assistant at the University of British Columbia, and I'm working with Margo Seltzer (https://www.seltzer.com/margo/) in the Systopia Lab. I'm helping with development of Sid Agrawal's (https://sid-agrawal.ca/) project built on seL4. I'm trying to determine what is the correct way to handle this situation: 1. Process 1 makes an seL4_Call to an endpoint that Process 2 is listening on. 2. … [View More]

2 2

seL4 developer hangout reminder
by Birgit Brecknell 06 Jun '24

06 Jun '24

Hi all A friendly reminder that the seL4 developer hangout is on again next week. Tue 11 Jun, 22:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0