Virtual address ranges used in seL4 initial thread after boot?
I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!) In addition, I like to know the address range used for the stack of the initial thread, as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?) I am on version 12.0 of seL4 for my project. Thank you! -Ben
On 9/4/2024 6:12 PM, Ben McCart wrote:
I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!)
In addition, I like to know the address range used for the stack of the initial thread, as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?)
I am on version 12.0 of seL4 for my project.
<snip> I did find the following in boot.c: v_region_t ui_v_reg = { .start = ui_p_reg_start - pv_offset, .end = ui_p_reg_end - pv_offset }; And I found the following in boot.h: void init_kernel( paddr_t ui_p_reg_start, paddr_t ui_p_reg_end, sword_t pv_offset, vptr_t v_entry, paddr_t dtb_addr_p, uint32_t dtb_size #ifdef ENABLE_SMP_SUPPORT , word_t hart_id, word_t core_id #endif What I have not yet found is how the 'ui_p_reg_start' and 'pv_offset' parameters are derived/constructed to make the call to init_kernel().
Hello Ben, On 2024-09-05 01:12, Ben McCart wrote:
I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!)
Like the manual mentions, you can use linker symbols to find most virtual addresses. What virtual addresses are used depends on the user image and is defined in the ELF file.
In addition, I like to know the address range used for the stack of the initial thread,
The default root task in most seL4 project use sel4runtime, which uses a static 16kb stack with the C variable name _stack_base and _stack_top, see e.g: https://github.com/seL4/sel4runtime/blob/master/crt/sel4_arch/x86_64/sel4_cr... You can use readelf(1) or objdump(1) on the binary of your userland image to find other symbols. However, the seL4 kernel also supports other user images than those based on sel4runtime, so the seL4 manual can only provide generic information.
as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?)
The reserved virtual address range is platform specific. Usually platforms only support a limited range of virtual address space, e.g. 48 bits out of 64 bits only. The upper bits are set to 1 for kernel virtual addresses and to 0 for user space virtual addresses. I think this is exported by libsel4 as seL4_UserTop. Greetings, Indan
participants (2)
-
Ben McCart -
Indan Zupancic