From: Devel <email@example.com> on behalf of Daniel Wang
Sent: Thursday, September 22, 2016 6:51 AM
Subject: [seL4] Questions about Memory Management in seL4
Sorry to bother, I have some basic questions about seL4 memory management. Can
someone help me?
1. where is the kernel's address space?
I know there are basically three methods:
a) separate virtual address space, e.g. through changing page tables on entry
into privileged mode to access
b) physical space, e.g. through disable automatic hardware translation of
virtual addresses on entry into privilege mode
c) privilege region in each process's virtual address space, e.g. through page
table to map kernel address into use-mode process.
My question is which of this is being used by seL4 microkernel?
2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel
objects, but it seems all dynamically allocated in thread running/creating
time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in
The memory for these objects is in kernel space (the user can't access them),
but the user is responsible of allocating the memory for such objects (using
retype untype), and give it to the kernel. Any operation on such objects
3. I read that after the kernel boot up, it passes all resources, untyped
memory to the first thread. Are those untyped memory physical memory or virtual
memory in a single page?
The reason I ask is I'm learning the code of the UNSW AOS project (two of the
assignment projects are implementing frame and papers). I'm confused that
before the implementation of frames and pages what kind of memory is passed to
the the first thread? I saw int AOS project, it uses ut_table_init(),
ut_steal_mem(), I wonder what kind of memory it operates on?
The root thread is granted system resources (including untyped memory).
Information about untyped memory is held by seL4_BootInfo and contains
"physical" start and end addresses for each untyped region. No virtual
addresses are involved. For example, if you want to read/write to some
(untyped) memory, you have to retype_untype it into a frame, and then map it to
your address space.
Devel mailing list