Hi,

I’m tracing the path where sel4 kernel jumps to an application, such as hello-1.

From the Makefile for apps I know that the entry of the hello-1.bin is _sel4_start which is defined in the sel4_crt0.S (the directory is sel4_tutorials/projects/sel4_libs_libsel4platsupport/src/arch/arm). The _sel4_start function first calls a C function called sel4_InitBootInfo, and finally jumps to the _start function which is defined in the crt0.S. However the _start in crt0.S calls the sel4_InitBootInfo again. What confuses me is that the sel4_InitBootInfo function requires an input argument passed by R0, however the R0 has been set to zero in the _sel4_start function, so I think the calling of sel4_InitBootInfo in the _start will not run correctly.

Or is the path where the kernel jumps to the app (_sel4_start->_start->main) wrong?

I paste referred codes below:

/******sel4_crt0.S********************/

_sel4_start:

    /* Setup a stack for ourselves. */

    ldr     sp, =_stack_top

    /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */

    bl      seL4_InitBootInfo

    ............

    mov     r0, #0 // The R0 is modified, so it doesn't store the bootinfo structure anymore!

    ............

    /* Now go to actual _start */

    ldr     pc, =_start

/*********crt0.S********************/

_start:

    /* Setup a stack for ourselves. */

    ldr     sp, =_stack_top

    /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */

    bl      seL4_InitBootInfo //Since R0 has been modified by _sel4_start, sel4_InitBootInfo will not run correctly.

    

    /* Call constructors and other initialisation functions. */

    bl      _init

    /* Call main. */

    bl      main

    b       exit

Best Regards,

Shijun Zhao