Hello Norman. I'm not really qualified to talk about why the kernel only allows copying of a single cap. The kernel designers certainly wanted to put a hard limit on the amount of work that can happen in a single IPC, but I don't know why they allowed three cap lookups on the sender side but only one cap save on the receiver. I can talk about the cap-unwrapping mechanism. Let me clarify how it works somewhat. The kernel will unwrap capabilities if they are to the same endpoint as the receiver is receiving on. It does not matter whether or not the capabilities have badges. The idea is that there's little point copying to a server a collection of capabilities with which to talk to itself. The receiver can identify which of the sender's capabilities were unwrapped by inspecting the "msgCapsUnwrapped" field. That's its kernel name - libsel4 calls it the capsUnwrapped field of seL4_MessageInfo. It's a bitfield of length 3, with one bit per possible cap transfer attempt. It tells you which caps were unwrapped. For example, if the sender tried to send caps A, B, C to server X, and caps A and C are in fact caps to the server's endpoint anyway, then the server will receive a message with extraCaps=11 (three caps used in the message) and capsUnwrapped=101 (first and third cap were unwrapped) and it will find a delegate of cap B wherever it specified its receive pointer. If it A, B, C are sent and only A is a cap to the server's endpoint, the server will receive a delegate of B, C will be dropped, and capsUnwrapped=001 will indicate that A was unwrapped (note the first cap is in bottom position). I think that the server will receive extraCaps=10 - that is, it will not be told that the sender was attempting to send three caps. I suppose this should be part of the client protocol, and the kernel mechanisms should focus on telling the server what has actually been modified. I hope that's helpful, Thomas. On 11/02/15 21:48, Norman Feske wrote:
Hello,
after a rather long break, I picked up my work with porting Genode to seL4. More specifically, I try to find a good way to realize Genode's RPC mechanism with seL4 IPC. But admittedly, I am struggling a bit.
Ideally, each Genode RPC should be realized as a seL4 IPC call. Unfortunately, however, I find the kernel interface too restrictive to do that. There are two issues.
1. Delegation of multiple capabilities at once
According to Chapter 4.2.2 of the manual, the kernel allows the delegation of merely a single capability for each IPC whereas the Genode API does not have such a restriction. It effectively renders my idea for working around the capability re-identification problem [1] by representing each Genode capability by a tuple (or triple) of seL4 endpoint capabilities moot.
[1] http://sel4.systems/pipermail/devel/2014-November/000112.html
Is there a fundamental reason for this restriction? If not, would you be open to make the kernel more flexible with regard to the maximum number of delegations per IPC?
2. Aliasing of unwrapped capabilities with delegated capabilities
I understand that the kernel will automatically "unwrap" capabilities if the receiver imprinted a badge into the received capability. In my experiments, the mechanism works as expected. However, how can the receiver determine, which capability got unwrapped if multiple capabilities were transferred?
For example, if the sender specifies three capabilities, two of them "unwrappable" and one delegated, the receiver will see 3 capabilities. The delegated cap is written to the specified 'ReceivePath' whereas the badges of the two unwrapped caps can be read from the message buffer. But I see no way for the receiver to decide, which of the three capability arguments got unwrapped and which got delegated. How could the receiver determine this information?
Best regards Norman
________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.