There may well be some benefit in allowing the transfer of multiple capabilities in a single IPC. But let’s remember that this discussion actually started with Norman's request for a different feature, which he characterized as “capability re-identification” [1]. We only began a transition to the current conversation when Norman proposed a cunning encoding to represent a Genode capability by a triple of seL4 capabilities [2]. Are there alternative ways to solve Norman’s original problem, perhaps even without requiring a change to the current seL4 design?

I proposed one possible approach during the original conversation (the second half of [3]). Like Harry’s suggestion, it involves the use of a CNode object (although I wasn’t thinking about using it for the purpose of transferring multiple capabilities). In addition, with my proposal, that CNode is created as a side effect of a one-time registration operation and is shared between multiple CSpaces. Among other things, this should eliminate the overhead that Gerwin mentioned of having to allocate a new CNode for every transfer. Back in November, it wasn’t entirely clear whether my proposal could be adapted to Genode to solve the problem that Norman had described, and we didn’t explore it further. However, even if that specific approach won’t work, perhaps there is a variation, or a different strategy altogether, that might do the trick instead? In short, I still think it might be worth exploring other options to make sure that we’re treating the problem rather than the symptom …