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 <[email protected]> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel > _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
