[seL4] Questions about Userspace memory allocation

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?

2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time?

Thanks -Dan