Running helloworld project build in release mode on ARMV8 Hardware hangs while loading kernel Image

seL4 kernel
1

Dear seL4 community members,

I am trying to run helloworld project build in release mode(Image size: 500K) on AVNET MaaxBoard based on ARMv8/Cortex-A53 which is a seL4 supported platform, but it is getting stuck at
“Jumping to kernel-image entry point…”. But the same project when build in Debug mode with image size approx 1.7M works fine.

The build instruction used are :

$ ../init-build.sh -DPLATFORM=maaxboard -DAARCH64=1 -DRELEASE

$ ninja

Here with the boot log for helloworld test************************************************************.

Fastboot: Normal
Normal Boot
Hit any key to stop autoboot: 0
u-boot=>
u-boot=>
u-boot=> fatls mmc 0:1
5584704 sel4test-driver-image-arm-maaxboard
2244864 sel4benchapp-image-arm-maaxboard
466688 hello-image-arm-maaxboard

5 file(s), 0 dir(s)

u-boot=> fatload mmc 0:1 0x40000000 hello-image-arm-maaxboard
466688 bytes read in 33 ms (13.5 MiB/s)
u-boot=> bootelf 0x40000000

Starting application at 0x40763000 …

ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
paddr=[40763000…407ce137]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive…found at 4079c388.
Loaded DTB from 4079c388.
paddr=[4022e000…40238fff]
ELF-loading image ‘kernel’ to 40000000
paddr=[40000000…4022dfff]
vaddr=[ffffff8040000000…ffffff804022dfff]
virt_entry=ffffff8040000000
ELF-loading image ‘hello’ to 40239000
paddr=[40239000…40372fff]
vaddr=[400000…539fff]
virt_entry=401bf0
Enabling MMU and paging
Jumping to kernel-image entry point…

I also tried to run on similar ARM Cortex-A53 hardware and getting the same problem i.e debug build is running and release build is getting stuck while loading the kernel image.
If any other details are required or if this post belongs somewhere else, please let me know! Any guidance is appreciated.

Regards,
Vishal

2

If the debug build works, but the release one doesn’t, it probably means that your user space UART driver is not initialized properly. I think the tutorials assume you build them in debug mode. A release kernel will not print anything itself, the last print you see is by done by Elfloader.

If you want to use the driver framework of util_libs/libplatsupport, you need to init it properly. For the UART itself you need to call platsupport_serial_setup_simple, in addition to setting up the rest of the framework. See sel4test/apps/sel4test-driver/src/main.c at master · seL4/sel4test · GitHub. See also the library tutorials Libraries initialisation & threading | seL4 docs.

If you just want printing to work on a non-debug kernel, you can also enable CONFIG_KERNEL_PRINTING instead of doing the above.