Hi Daniel On Tue 11-Apr-2017 1:33 AM, Daniel (Xiaolong) Wang wrote: Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? If the initial thread wants a stack or a heap, then it has the responsibility of allocating and managing that. Typical rootservers that we write will use an entry point that has a statically allocated stack that can be set prior to calling main (https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/sel4_ar...) and will use minimal C library with a small static heap (https://github.com/seL4/seL4_libs/blob/master/libsel4muslcsys/src/sys_moreco...) 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? I don't really understand this question as I'm not sure what you mean by 'booting time'. During kernel boot seL4 must allocate enough memory to hold the init threads image (as the init thread has described itself in its ELF sections) as well as allocate a TCB, cnode, IPC buffer and bootinfo frame. The limit is how much physical memory available to the kernel. I don't know what you mean by default. Adrian