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
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