Latest seL4 tests fail on Raspberry Pi 3

New to seL4
1

Hello!

I am trying to get seL4 tests on Raspberry Pi 3 B as described here: Raspberry PI 3 Model B and Model B+ | seL4 docs

I am using the latest sel4test-manifest.

First, building U-boot according to the instructions doesn’t seem to work - no output on the terminal.

Using the prebuild U-boot from https://sel4.systems/Info/Docs/u-boot-working-rpi3-32bit-v2017.11.bin results in this output:

U-Boot> fatload mmc 0 0x00001200 sel4test-driver-image-arm-bcm2837
reading sel4test-driver-image-arm-bcm2837
5289144 bytes read in 363 ms (13.9 MiB/s)
U-Boot> bootelf 0x00001200
CACHE: Misaligned operation at range [01848000, 01848034]
CACHE: Misaligned operation at range [01849000, 01853b08]
CACHE: Misaligned operation at range [01853b08, 01854a7b]
CACHE: Misaligned operation at range [01854a7c, 01854a84]
CACHE: Misaligned operation at range [01858000, 01865048]
CACHE: Misaligned operation at range [01865048, 01d24848]
CACHE: Misaligned operation at range [01d34848, 01d348a4]
CACHE: Misaligned operation at range [01d348a4, 01d348d4]
## Starting application at 0x01848000 ...

ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
  paddr=[1848000..1d348d3]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 1975354.
Loaded DTB from 1975354.
   paddr=[1040000..1043fff]
ELF-loading image 'kernel' to 1000000
  paddr=[1000000..103ffff]
  vaddr=[e0000000..e003ffff]
  virt_entry=e0000000
ELF-loading image 'sel4test-driver' to 1044000
  paddr=[1044000..1449fff]
  vaddr=[10000..415fff]
  virt_entry=1e230
Enabling MMU and paging
Jumping to kernel-image entry point...

DIDRv: 6, armv 80, coproc baseline only? no.
Bootstrapping kernel
available phys memory regions: 1
  [1000000..8000000]
reserved virt address space regions: 4
  [e0000000..e0040000]
  [e0040000..e0043593]
  [e0044000..e044a000]
  [ff000000..ff100000]
Booting all finished, dropped to user space
ps_fdt_walk_irqs@fdt.c:229 Could not find a parser for this particular interrupt                                                                                                                                                                                                                                          controller
helper_fdt_alloc_simple@ltimer.h:78 Simple FDT helper failed to register irqs (-                                                                                                                                                                                                                                         2)
bcm_system_timer_init@system_timer.c:214 Failed to allocate with fdt
ltimer_default_init@ltimer.c:112 system timer initialisation failed
init_timer@main.c:181 [Cond failed: error]
        Failed to setup the timers
seL4 root server abort()ed
Debug halt syscall from user thread 0xe6feb400 "sel4test-driver"
halting...
Kernel entry via Unknown syscall, word: 1

Interestingly, using a manifest that corresponds to the last edits on the RPi3 platform page, I can get sel4tests to run.

Was there a breaking change introduced? Or based on the output, can you tell if there is something else going on?

Regards

2

It doesn’t look like this platform is part of the default CI suite anymore. Supported Platforms | seL4 docs probably shouldn’t say that the platform is supported by the seL4 Foundation. Likely what happened is that updates for rpi4 are incompatible with the rpi3, but they share the same drivers that sel4test uses (util_libs/libplatsupport/src/mach/bcm at master · seL4/util_libs · GitHub).
There were recent changes that were attempting to resolve build failures it seems: Fix RPi3 build failure by JoonasOnatsu · Pull Request #140 · seL4/util_libs · GitHub

3

Hm, yes, it fell out of CI because the board didn’t work after the move, and like always what is not tested breaks over time. Ivan promised to have a look at getting it running again on Mon and updating the instructions with it.

Apologies @mpodhradsky, this should really have been working.

We should probably try to automate the connection between what is in CI and what is listed in the docs as supported. We already have the CI data available as yaml. Surely something can be done there.

4

@gerwin.klein having some automated updates to the list of supported platforms would be excellent.

If RPi3 is no longer practical to support, that is OK for us (they are hard to get these days anyway), but if it is an easy fix, then it would be great.

I just learned about your HW CI testing and I am very impressed by that! Any chance this can be expanded on at least a subset of CAMKES apps?