1 Apr
2016
1 Apr
'16
3:29 a.m.
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
1 Apr
1 Apr
1:56 p.m.
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
<danielwang.ksu(a)gmail.com> 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
Devel(a)sel4.systems
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.
3:45 p.m.
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
<gernot(a)nicta.com.au> 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
<danielwang.ksu(a)gmail.com> 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
Devel(a)sel4.systems
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
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
2320
days inactive
2321
days old
2 comments
3 participants
participants (3)
-
Daniel Wang -
Gernot Heiser -
Gerwin Klein