In seL4, capabilities are used to refer to blocks of memory. You can delegate access to parts of your address space simply by passing the capability to another process. You can also implement nested processes, by providing them with only the capabilities to talk to you. Memory in seL4 is typed. For example, some memory regions hold capabilities; to preserve the unforgeable guarantee, they can only be modified by the microkernel. On boot, the kernel reserves some memory for itself and then delegates the remainder of the memory to a process as an untyped memory (UM) capability. -- http://www.informit.com/articles/article.aspx?p=1994798

On Mon, Aug 31, 2015 at 3:57 AM, Raymond Jennings <shentino@gmail.com> wrote:
Is there an easy way for one task to share address space with another task directly or does it have to go through the kernel/os and be emulated?

I noticed that support for mapping memory is mostly low level assignment of physical frames to virtual frames via page tables, unlike Mach which uses memory objects.


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




--
Jeroen "Slim" van Gelderen