sigma0 memory space

[joel at nider.org]

I have been reading about the structure of L4Ka::Pistachio, and 
discovered that they use idempotent (1:1) page table mapping in their 
sigma0 process.  I am wondering if Fiasco also takes this approach?
If so, does the kernel also use idempotent mapping?

I would imagine that this would have some implications on demand paging 
in the kernel.  Does the kernel even use demand paging?  (I mean at 
some point during boot the kernel will start to use memory to store 
kernel objects - either the kernel 'guesses' how much it will ever need 
and statically allocates that memory, or it's going to have to ask for 
pages later on, which will be owned by some other process). 

I tried to read the code, but found it very hard to traverse - the C++ 
classes don't make it easy to follow a flow.  Can you please point out 
the file(s) where the kernel sets up the memory space for sigma0, and 
where it passes the initial ownership (from kernel space to sigma0 
space)?

Thanks,
Joel