Yes, I think the seL4 kernel is mapped into the virtual address space of all processes. I think the exact separation between user mode space and kernel space depends on the platform. For example, on the zynq7000 platform we have:

https://github.com/seL4/seL4/blob/master/src/plat/zynq7000/linker.lds

KERNEL_BASE = 0xe0000000; PHYS_BASE = 0x00000000; KERNEL_OFFSET = KERNEL_BASE - PHYS_BASE;

So there is ~3.5GB user mode space, ~500MB kernel space.

-Andrew

On Mon, Nov 21, 2016 at 7:13 PM, Mark Reus markreusva@gmail.com wrote:

Hi

I have a general case about memory allocation in particular with that of the Vspace. I have been reading some documents and trying to compare how it is in Linux Kernel. Any program Virtual memory in a Linux kernel is as shown in picture below where all processes have 1GB of virtual memory which is mapped to kernel space for faster context switches and system calls.

---

| Kernel Space (1GB) | |_____________________| | | | User Mode Space | | (3 GB) | | | |_____________________|

I have come across this this link http://os.inf.tu-dresden.de/pipermail/l4-hackers/2014/006262.html detailing a little about the sel4 memory management. But I haven't been able to completely comprehend it . I wanted to know if the seL4 kernel also has a similar mapping of kernel space.

Regards Mark

---

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