seL4bench test getting stuck at ((init_arm_kernel_t)kernel_info.virt_entry)

Dear seL4 community members,

I am trying to run seL4bench for Arm 53 Core platform, but it is getting stuck.

Whereas, I am able to run seL4test application with the same ELF-loader & seL4 Microkernel which just boots fine and launches the seL4test application on my hardware, but fails for seL4bench test.

Here with the boot log for seL4bench test.

Boot log******************************************************************************

Starting application at 0x80867000 …

ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
paddr=[80867000…80a7c1a7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive…found at 808998a0.
Loaded DTB from 808998a0.
paddr=[8022b000…80239fff]
ELF-loading image ‘kernel’ to 80000000
paddr=[80000000…8022afff]
vaddr=[ffffff8080000000…ffffff808022afff]
virt_entry=ffffff8080000000
ELF-loading image ‘sel4benchapp’ to 8023a000
paddr=[8023a000…80472fff]
vaddr=[400000…638fff]
virt_entry=422940
Enabling MMU and paging
Jumping to kernel-image entry point…

Going for init_arm_kernel_t


After this console hangs.

While analyzing this, it was observed that, its getting stuck while providing the Information about the image we are loading.
at this ((init_arm_kernel_t)kernel_info.virt_entry)(user_info.phys_region_start,
user_info.phys_region_end,
user_info.phys_virt_offset,
user_info.virt_entry,
(word_t)dtb,
dtb_size);

The source for sel4 bench is taken from below link

If any other details are required or if this post belongs somewhere else, please let me know! Any guidance is appreciated.

Regards,
Vishal

The line you claim it is getting stuck on is where the elfloader jumps to kernel execution. At this point there could be a couple reasons why no more output appears on the console:

  • The kernel is compiled without debug printing and the user app doesn’t boot correctly,

  • The serial device selected for the kernel to use in debug is not the same as the elfloader

  • The target hardware isn’t compatible with the platform configuration seL4 was compiled for. Is your target platform a supported seL4 platform? If not you may need to override the Device tree that the kernel uses at build time to calculate the load addresses. The ELFloader can run from any address it is loaded from, but the kernel is compiled to a specific load address in physical memory. If this address is different at runtime, the kernel won’t boot.

Hi Kent,
Thankyou for your reply.
Here with our findings:

  • The kernel is compiled without debug printing and the user app doesn’t boot correctly,
    In our platform port , kernel is complied with debug prints we verified it using sel4test/hello world project integrated and running properly.
  • The serial device selected for the kernel to use in debug is not the same as the elfloader
    In our platform port , the serial driver in elfloader and kernel are same and working, when tested with sel4test/hello world project integrated which is running properly, giving all the serial output.

The problem is when we integrated the sel4bench, kernel is not getting executed and we see the debug prints till elfloader. The details of the log is provided in the my above post.

  • The target hardware isn’t compatible with the platform configuration seL4 was compiled for. Is your target platform a supported seL4 platform? If not you may need to override the Device tree that the kernel uses at build time to calculate the load addresses. The ELFloader can run from any address it is loaded from, but the kernel is compiled to a specific load address in physical memory. If this address is different at runtime, the kernel won’t boot.

In our platform port, as mentioned sel4test and hello world project are running properly and we are able to launch the kernel , after integrating the sel4bench the kernel is not getting launched.
In our dts overlay file the memory load address is mentioned as :

memory@80000000 {
device_type = “memory”;
reg = < 0x00 0x80000000 0x00 0x1f000000 >;
};

howcome the Kernel gets loaded properly with sel4test/hello world project integrated and complied whereas with sel4bench it fails.

The start address and the size of kernel is determined during the build which is common for any project we integrate at userlevel

What makes the sel4bench when integrated fails to launch the kernel.

Can you please give us hints where can be the bug.

Regards,
Vishal