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 _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
