Forward: some thoughts about map vs. copy vs. membranes

[Marcus Brinkmann]

Hi,

just filing some random thoughts for the archive.

The discussion about mechanisms for capability delegation was framed
by contrasing L4's map model and other kernels (Mach, EROS) copy
model.  Later, on cap-talk, a third idiom came up: membranes, which
have mapping semantics plus every capability fetched through a
membraned capability is limited by the lifetime of the membrane as
well.  For example, if you look up a file object in a directory
object, with membrane semantics the file capability is revoked also
when the directory capability is revoked.

It is worth repeating the difficulty in implementing a generic
membrane: If a membraned capability is fetched through a membraned
capability, the lifetime of that capability is now generally bound by
two membranes.  Repeating such operations establishes a N-to-M
relationship between membranes and capabilities, which raises storage
allocation concerns.  Only special cases are easy to handle, for
example if the two membranes are already related (one dominating the
other).  Unfortunately, membrane semantics are often desirable.

The main point I want to get across in this mail is that the
discussion about map and copy was at best misleading.  By switching to
a different point of view, it can be shown that ***L4 X.2 implements
membrane semantics*** rather than map semantics.  So, the discussion
should not have been about map vs. copy but about membranes vs. copy.

It's easy to show that L4 X.2 implements membrane semantics: First,
the only delegatable capabilities are frame capabilities, so there is
only one object type to consider.  The only "fetch through" operation
allowed is to take a sub-flexpage of a mapped flexpage.  This
sub-flexpage is dominated by the containing flexpage, which is exactly
what membrane semantics requires.  (Think of the flexpage as a
directory, which contains one capability for each sub-flexpage of the
flexpage).  This covers all possible operations on flexpages, the only
delegatable objects.  Note that for all delegations, the special case
described above applies: the (implicit) "membranes" involved in a
single operation can be totally ordered by a dominance relation.  Thus
there is one membrane (the lowest) which expires when any of the other
membranes expires.  This is the only membrane that needs to be stored
for a given object, thus we have a constant space requirement.  QED

The semantic problem that the L4 communities face is how to extend
these semantics to delegation of other object types like threads and
communication end points, for which the totally ordered dominance
relation does not exist.  As far as I can see, Karlsruhe and Dresden
drop membrane semantics and switch to map semantics, while Sydney
switches essentially to copy semantics (this is my first impression, I
have still to analyze their rules in detail.  In fact, seL4 seems to
use a hybrid model, where untyped memory is delegatable with membrane
semantics, while, while all typed objects are delegatable by copy.
There is also a special exception---the revocable bit---for
communication endpoints with badges, replacing EROS wrapper objects).

I will try to give a complete description of seL4 in some later mail.

Thanks,
Marcus