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

[Jonathan S. Shapiro]

On Wed, 2007-09-05 at 19:22 +0200, Marcus Brinkmann wrote:
> 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.

Unfortunately, it is worse than this. If a capability is returned across
a membrane boundary by an operation of the form:

        cresult = c0->method(data args, c0, c1, ..., cn)

then the lifetime of cresult is bounded by the lifetimes of c0 .. cn.
While a binary tree can express this dependency, the logical dependency
chain is not restricted to two inputs per output. The problem is that we
cannot know at the time of membrane formation which capability in {c0,
cn} will die first.

> It's easy to show that L4 X.2 implements membrane semantics...

Because membrane injection is not restricted to cases of delegation,
membranes require full interposition of all invocations in general. In
order for L4 kernel to implement membrane semantics, it would be
required to do full causal dependency tracking across IPC.

The L4 map primitive does implement a restricted sub-case of membrane
semantics, but this sub-case is not useful. The problem is that (1) a
generalized membrane can only be implemented at user level, and (2) when
a user-level implementation exists, the additional membranes inserted by
the kernel in the case of map are at best not helpful and at worst may
create challenges for selective membrane revocation.


I may have failed to understand something here, but I think your
analysis of membrane support in L4 was incomplete.
-- 
Jonathan S. Shapiro
Managing Directory
The EROS Group, LLC
www.coyotos.org, www.eros-os.org