- Devel - lists.sel4.systems

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 manually set all the '*HAVE_TIMER*' flags in the code to 0 - to get the tests to succeed on VirtualBox; CMake doesn't appear to support this transformation. - a major stumbling block was that these changes were being reverted each time I re-ran CMake, under my feet. So that's pretty cool... Some further exploration I discovered that there's the pc99/ega (ega.c) driver, since I'm curious about the requirements for starting to build a custom OS on top of seL4 for this platform, and seeing it run on the hardware in front of me (again, a Tiger Lake laptop). I spent many weeks trying to massage things into place. Reading and learning along side the bootstrap pathway; multiboot.S -> head.S -> boot_sys -> common -> char_dev ... to no avail. However I came into some time and decided to revisit the problem. - #define MULTIBOOT_GRAPHICS_TEXT 2 is an error; Multiboot1 spec has that this should be 1, instead - When I was trying to boot UEFI, this would manifest as a Protection Fault - Fixing this left the system booting, utilizing high amount of CPU, and then going quiet. - UEFI on this platform has unclear / additional requirements / doesn't actually support EGA/VGA text mode - https://www.reddit.com/r/osdev/comments/st0psl/framebuffer_output_for_multi…

2 1

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

16 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/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

1 0

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

13 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. Process 2 receives the message, and since we are running in non-MCS kernel, it will get a reply capability in its TCB. 3. Process 2 dies, for whatever reason, before it can reply to Process 1. If we wanted to unblock Process 1, what would be the correct approach? - I can use seL4_CNode_SaveCaller in Process 2 as soon as it receives a message, and store the slot number in some shared memory with the root task. Then when Process 2 dies, the root task is able to move the reply capability into its own cspace and send a reply indicating an error. This is not ideal for our purpose, because we do not want Process 2 to be able to perform any operations on its own cspace, but it needs its own root cnode capability in order to perform seL4_CNode_SaveCaller. - Is seL4_Call the wrong function for this purpose? We also considered using NBRecv and considering the call a failure after some timeout period. This is also not ideal since we would lose the convenience of the Call's reply cap, etc. - Is there some other solution that we are missing? As an aside: I notice that for the MCS kernel, if the reply cap is deleted, Process 1's thread state would be moved from ThreadState_BlockedOnReceive to ThreadState_Inactive. In non-MCS kernel, it seems that the state would remain ThreadState_BlockedOnReceive? Is there a reason for this? Best, Arya

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

Multikernel in RISCV
by David Martin 06 Jun '24

06 Jun '24

Hello, I'm currently working with seL4 & Polarfire (RISCV) and I'm working with a single core at the moment (doing some testing and understanding how seL4 works). Polarfire has 4 cores and I'd like to start using all of them in a multikernel configuration (every hart running its own sel4 kernel). I've found the following RFC: https://sel4.atlassian.net/browse/RFC-17 where Kent McLeod has done some work (https://github.com/kent-mcleod/camkes-manifest/blob/kent/multicore2/master.…) but only for ARM. Does someone know if the same approach will be taken for RISCV? or even better, if someone has already done it? Thanks, David.

3 5

seL4 developer hangout reminder
by Birgit Brecknell 27 May '24

27 May '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 29 May, 8: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

sel4bench grub iso
by Bengt.Lennicke＠mailbox.tu-dresden.de 24 May '24

24 May '24

Hello everyone, I am trying to create a grub iso image in order to run sel4bench on real hardware. The target architecture is x86_64 and I would prefer a grub iso because no changes to the hardware setup would be necessary then. What I did so far: I create the sel4bench images as follows mkdir sel4bench cd sel4bench repo init -u -u https://github.com/seL4/sel4bench-manifest.git repo sync mkdir build cd build ../init-build.sh -DPLATFORM=x86_64 ninja I get two elf images in the build/images directory as expected. Now in order to creat a bootable iso image i followed this guide https://www.gnu.org/software/grub/manual/grub/html_node/Making-a-GRUB-boota… Which means: mkdir -p iso/boot/grub grub-mkrescue -o grub.iso cp /path/to/kernel-x86_64-pc99 iso cp /path/to/sel4benchapp-image-x86_64-pc99 iso Then I add the grub.cfg under iso/boot/grub/grub.cfg menuentry "Load seL4 VM" --class os { multiboot /kernel-x86_64-pc99 module /sel4benchapp-image-x86_64-pc99 } There are a few lines missing from your offered grub stanza here https://docs.sel4.systems/Hardware/IA32 Mainly because I was having issues with getting it to run with them and without them I got further. Then I run grub-mkrescue -o grub.iso iso And try out the resulting iso as follows: qemu-system-x86_64 -cdrom grub.iso -nographic -enable-kvm -cpu Haswell,-vme,+pdpe1gb,+xsave,+xsaveopt,-xsavec,+fsgsbase,+invpcid,+syscall,+lm,enforce -m size=512M I get the following output: seL4 Benchmark ============== Switching to a safer, bigger stack... Setting up global fault handler... Failed to allocate object of size 140737488355328, error 1 Failed to allocate object of size 70368744177664, error 1 Failed to allocate object of size 35184372088832, error 1 Failed to allocate object of size 17592186044416, error 1 Failed to allocate object of size 8796093022208, error 1 Failed to allocate object of size 4398046511104, error 1 Failed to allocate object of size 2199023255552, error 1 Failed to allocate object of size 1099511627776, error 1 Failed to allocate object of size 549755813888, error 1 Failed to allocate object of size 274877906944, error 1 Failed to allocate object of size 137438953472, error 1 Failed to allocate object of size 68719476736, error 1 Failed to allocate object of size 34359738368, error 1 Failed to allocate object of size 17179869184, error 1 Failed to allocate object of size 8589934592, error 1 Failed to allocate object of size 4294967296, error 1 Failed to allocate object of size 2147483648, error 1 Failed to allocate object of size 1073741824, error 1 Failed to allocate object of size 536870912, error 1 Failed to allocate object of size 268435456, error 1 ipc Benchmarks ============== irquser Benchmarks ============== arch_simple_get_IOPort_cap not implemented Failed to get capability for IOPort range 0x43-0x43 PIT command failed! [Cond failed: error] Failed to init timer Benchmark failed, result 1 Register dump: rip: 0x4138a0 rsp: 0x10011640 rflags: 0x246 rax: 0x10000000 rbx: 0x10011660 rcx: 0x420c48 rdx: 0xffffffffffffffff rsi: 0x1 rdi: 0x2 rbp: 0x10011680 r8: 0x2b r9: 0x12008180c100f r10: 0x1 r11: 0x206 r12: 0x10011d88 r13: 0x10011d98 r14: 0x0 r15: 0x0 fs_base: 0x7494d0 gs_base: 0x0 [Cond failed: result == NULL] Failed to run benchmark irquser So ipc seems to run fine but irquser is not. Now I am only interested in the benchmark IPC for now. And maybe FAULT as well later. So I do not need to get irquser to run. Therefore I do the following setup again: mkdir sel4bench cd sel4bench repo init -u -u https://github.com/seL4/sel4bench-manifest.git repo sync mkdir build cd build ../init-build.sh -DPLATFORM=x86_64 and not i run ccmake . which opens a configuration screen where I can choose which benchmarks I want to include in the image. I disable everything except FASTPATH (this does not seem to be a benchmark) and IPC. I run ninja again and use the resulting images are build into an iso as stated above. Now running qemu results in this: Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa87000 end=0xd4e6a0 size=0x2c76a0 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fee0000 type 1 Adding physical memory region 0x100000-0x1ffe0000 Physical Memory Region from 1ffe0000 size 20000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Got VBE info in multiboot. Current video mode is 3 ACPI: RSDP paddr=0xf5b20 ACPI: RSDP vaddr=0xf5b20 ACPI: RSDT paddr=0x1ffe1550 ACPI: RSDT vaddr=0x1ffe1550 Kernel loaded to: start=0x100000 end=0xa14000 size=0x914000 entry=0x10040b ACPI: RSDT paddr=0x1ffe1550 ACPI: RSDT vaddr=0x1ffe1550 ACPI: FADT paddr=0x1ffe1404 ACPI: FADT vaddr=0x1ffe1404 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffe1478 ACPI: MADT vaddr=0x1ffe1478 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x242000 v_entry=0x449631 v_start=0x400000 v_end=0x642000 p_start=0xd4f000 p_end=0xf91000 Moving loaded userland images to final location: from=0xd4f000 to=0xa14000 size=0x242000 Starting node #0 with APIC ID 0 Mapping kernel window is done available phys memory regions: 1 [100000..1ffe0000] reserved virt address space regions: 1 [ffffff8000100000..ffffff8000c56000] Booting all finished, dropped to user space seL4 Benchmark ============== Switching to a safer, bigger stack... Setting up global fault handler... vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 140737488355328, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 70368744177664, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 35184372088832, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 17592186044416, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 8796093022208, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 4398046511104, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2199023255552, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 1099511627776, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 549755813888, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 274877906944, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 137438953472, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 68719476736, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 34359738368, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 17179869184, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 8589934592, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 4294967296, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2147483648, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 1073741824, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 536870912, error 1 vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 268435456, error 1 ipc Benchmarks ============== libsel4muslcsys: Error attempting syscall 228 libsel4muslcsys: Error attempting syscall 96 JSON OUTPUT [{"Benchmark": "One way IPC microbenchmarks", "Results": [{"Function": "seL4_Call", "Direction": "client->server", "Client Prio": 254, "Server Prio": 254, "Same vspace?": true, "IPT .... All is well in the universe. Fin So the benchmark runs but now a libsel4muslcsys error is new. syscall 228 is sys_clock_gettime so I assume it is important for the benchmark and even so it is not terminating I am not sure whether the results are correct with that error. So somehow removing the other benchmarks resulted in an error in the ipc benchmark which was not there or at least not shown there when compiling with all benchmarks. When trying to find out which removal is causing the problem a variety of other problems is appearing. Do you think the musllib error is related to the missing lines in the grub.cfg? If so do you have an idea which one? Why do the different benchmarks influence each other, am I compiling it wrong? If there are information missing feel free to let me know and I will try to add them Kind regards, Bengt

2 2

Register for the seL4 summit 2024
by Birgit Brecknell 17 May '24

17 May '24

The seL4 summit 2024 [0] will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: * Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions * Networking with other seL4 experts and enthusiasts * Reception and dinner Register here [1] The early bird cut-off date is 15 September 2024. Local seL4 Sydney-siders will look into organising some informal activities for Monday 14 October 2024, before the summit kicks off, for anyone who wants to join. Gernot may also organise a bush walk for the weekend before the summit. Stayed tuned for more info! [0] https://sel4.systems/Foundation/Summit/2024 [1] https://events.linuxfoundation.org/sel4-summit/ Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Loading a large sel4test image on Odroid-C4 Fails
by Linh Pham 16 May '24

16 May '24

Hello, I am running into an issue with booting up an sel4test image on the Odroid-C4. When the calculated memory bound for the sel4test-driver's ELF is around 100MB or larger, I get an asychronous data abort like so: ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[c3d2000..e068117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at c502760. Loaded DTB from c502760. paddr=[256000..261fff] ELF-loading image 'kernel' to 0 paddr=[0..255fff] vaddr=[8000000000..8000255fff] virt_entry=8000000000 ELF-loading image 'sel4test-driver' to 262000 paddr=[262000..6cd7fff] vaddr=[400000..6e75fff] virt_entry=443090 "Error" handler, esr 0xbe000011 elr: ffffffff1a4996e4 lr : ffffffff1a497654 (reloc) elr: 000000000c3d96e4 lr : 000000000c3d7654 x0 : 0000000001ad7340 x1 : 0000000000000000 x2 : 0000000006a75348 x3 : 000000000c3dfdc0 x4 : 0000000001b494c8 x5 : 000000000c3dca50 x6 : 0000000000262000 x7 : 0000000000000001 x8 : 0000000000000008 x9 : ffffffffffffffff x10: 0000000000000000 x11: 0000000000000002 x12: 00000000f4fef9e0 x13: 0000000000000001 x14: 00000000f4fef9e0 x15: 0000000000000000 x16: 0000000020000000 x17: 0000000000c0c0c0 x18: 00000000f0f3dda0 x19: 000000000c3dfff0 x20: 0000000020000000 x21: 0000000000000002 x22: 00000000f0f769c0 x23: 0000000000000002 x24: 00000000f2ff556c x25: 0000000000000000 x26: 0000000000000000 x27: 0000000000000000 x28: 00000000f0f6d380 x29: 000000000c3dfda0 Code: f94017e0 91002000 f90017e0 f94007e0 (f1001c1f) Resetting CPU ... Our sel4test image is large because we're using a static heap. Note that the relevant region from the log output is [262000..6cd7fff], the exception occurs when trying to write into memory in this range. After some investigation, writing to physical address 0x5100000 is what causes the problem. I haven't been able to find any documentation on why this physical address range can't be written to. Is this some sort of device memory region? I was able to eventually boot by changing the ELF loader to load into a much higher memory address (e.g. somewhere around 0x80000000), but I would like to have a clearer idea of the Odroid's memory layout so that I could choose an address range that is definitely safe to load the image into. Thank you, Linh

2 2