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