To elaborate on that: the loop you are seeing, with map_kernel_window and later on for untyped regions, is the initialisation that mostly records what memory is available in the machine and assigns authority (capabilities) to memory regions so users can invoke the retype mechanism which replaces in-kernel memory allocation (which is what Gernot hints at below).
The seL4 code tutorials have some examples on retyping, which might make it easier to understand than the papers. Cheers, Gerwin > On 1 Apr 2016, at 1:56 PM, Gernot Heiser <[email protected]> wrote: > > The kernel doesn’t really allocate memory (for reasons explained in various > papers). All it has is static data and a stack. This is part of its isolation > story, as well as policy freedom. > > Gernot > >> On 1 Apr 2016, at 3:29 , Daniel Wang <[email protected]> wrote: >> >> Hi all, >> >> I’m trying to understand the seL4 kernel source code. I think the memory >> mapping between physical memory and virtual memory is a key point since it >> is directly related to how kernel functions and manage badges. I noticed >> that the kernel turns on the paging very early. Can someone help me or point >> out some resources how kernel memory is allocated? Especially how during and >> after the booting what the kernel memory snapshot looks like and things like >> that. >> >> For example, I traced to map_kernel_window() function and even before that >> there is some pptr to paddr conversion. I would really appreciate the help. >> >> Thanks >> -Dan >> _______________________________________________ >> Devel mailing list >> [email protected] >> https://sel4.systems/lists/listinfo/devel > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
