[seL4] The path where the kernel jumps to apps

Hesham.Almatary at data61.csiro.au Hesham.Almatary at data61.csiro.au
Wed May 31 13:45:55 AEST 2017


Hi Shijun,

_sel4_start sets up the stack (for the root task) as libmusl expects, 
and then jumps to _start (from libmuscl) and *NOT* the one at 
sel4platsupport/crt0.S. The _start function you're after (called by 
_sel4_start) exists in libmuslc for each arch e.g. 
libmuslc/arch/arm/crt_arch.h.


Cheers,
Hesham

On 31/05/17 12:59, shijun zhao wrote:
>
> 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
>
>
>
> _______________________________________________
> Devel mailing list
> Devel at sel4.systems
> https://sel4.systems/lists/listinfo/devel


More information about the Devel mailing list