I’ve added answers to some of these questions to the seL4 FAQ, 
https://wiki.sel4.systems/FrequentlyAskedQuestions

Most of them are actually answered in the documentation referenced on the seL4 
documentation page: https://wiki.sel4.systems/Documentation

Gernot

On 22 Sep 2016, at 6:51 , Daniel Wang 
<danielwang....@gmail.com<mailto:danielwang....@gmail.com>> wrote:

Hi all,

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 
user space?

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?

Thanks
-Dan
_______________________________________________
Devel mailing list
Devel@sel4.systems<mailto:Devel@sel4.systems>
https://sel4.systems/lists/listinfo/devel

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to