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