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