Scheduler failing on Raspberry Pi 4

New to seL4
1

Hi,
I’m trying to get the basic sel4 example (as outlined here: Raspberry PI 4 Model B | seL4 docs) running on a Raspberry Pi 4 4 GB.
I went through the steps according to the instructions and finally got sel4 booting. Unfortunately, the example stopped working after dropping into user space; see output below. Any help would be much appreciated.

U-Boot 2023.10-rc4-00074-gf8cc8e3116 (Sep 27 2023 - 14:21:36 +0200)

DRAM: 948 MiB (effective 3.9 GiB)
RPI 4 Model B (0xc03115)
Core: 209 devices, 16 uclasses, devicetree: board
MMC: mmcnr@7e300000: 1, mmc@7e340000: 0
Loading Environment from FAT… OK
In: serial,usbkbd
Out: serial,vidconsole
Err: serial,vidconsole
Net: eth0: ethernet@7d580000
PCIe BRCM: link up, 5.0 Gbps x1 (SSC)
starting USB…
Bus xhci_pci: Register 5000420 NbrPorts 5
Starting the controller
USB XHCI 1.00
scanning bus xhci_pci for devices… 2 USB Device(s) found
scanning usb for storage devices… 0 Storage Device(s) found
Hit any key to stop autoboot: 0
U-Boot> editenv sel4
edit: fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711 && go 0x10000000
U-Boot> saveenv
Saving Environment to FAT… OK
U-Boot> sel4
Unknown command ‘sel4’ - try ‘help’
U-Boot> run sel4
5153024 bytes read in 462 ms (10.6 MiB/s)

Starting application at 0x10000000 …

ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3
paddr=[10000000…104ea0ff]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive…found at 1013aa20.
Loaded DTB from 1013aa20.
paddr=[123d000…1243fff]
ELF-loading image ‘kernel’ to 1000000
paddr=[1000000…123cfff]
vaddr=[ffffff8001000000…ffffff800123cfff]
virt_entry=ffffff8001000000
ELF-loading image ‘sel4test-driver’ to 1244000
paddr=[1244000…1649fff]
vaddr=[400000…805fff]
virt_entry=40ef20
Enabling MMU and paging
Jumping to kernel-image entry point…

Bootstrapping kernel
available phys memory regions: 3
[1000000…3b400000]
[40000000…fc000000]
[100000000…200000000]
reserved virt address space regions: 3
[ffffff8001000000…ffffff800123d000]
[ffffff800123d000…ffffff800124356b]
[ffffff8001244000…ffffff800164a000]
Booting all finished, dropped to user space
seL4 failed assertion ‘isSchedulable(candidate)’ at /host/kernel/src/kernel/thread.c:371 in function schedule
halting…
Kernel entry via Interrupt, irq 0

2

The documentation is a bit out of date, I’ll try fix that this week.

When building sel4test, you want to add RPI4_MEMORY=4096 since it defaults for the 8GB model but you have a 4GB model. The scheduler is failing because the kernel is assuming it has 8GB of physical memory but in reality that’s not true.

So your build command will look something like this instead:

../init-build.sh -DPLATFORM=rpi4 -DAARCH64=1 -DRPI4_MEMORY=4096

Hope this helps.

3

I’ve made a PR now to fix the documentation for future users Fixes and improvements to Raspberry Pi 4B documentation by Ivan-Velickovic · Pull Request #203 · seL4/docs · GitHub.