The seL4_CNode_CancelBadgedSends is a CNode invocation but this invocation only exists to clear send queue on an IPC endpoint. This makes the API somewhat astonishing. Why not have the invocation directly on an endpoint?
Short answer: because this call is expected to be done by a thread managing a cspace, not a thread which invokes the capability in its current cspace.
Longer: this is the distinction between the two types of addressing in the seL4 API. Calls expected to be used by threads managing cspaces use cspace addressing (cnode, depth, cptr) to access anywhere in the cspace regardless of the cspace layout, and calls which are most commonly used by threads invoking those capabilities are achieved by direct invocation on a cap expected to be in the current cspace.
For more info on capability addressing: https://docs.sel4.systems/Tutorials/capabilities.html
Also, by allowing the direct addressing, most common invocations fit into registers. Not that this currently saves much: every invocation looks up the IPC buffer anyway. But I have a patch that’s waiting for a verification engineer to take a look at that fixes that.
This invocation only really makes sense to be used when the caller holds exclusive access to the original capability to a badged endpoint and has just revoked that capability. I would expect this to be used by any component handing out capabilities that can be used to perform IPC with it rather than those in particular that are responsible for managing cspaces.
Good point. However, in any case it’s not a hotpath invocation so it doesn’t need to be efficient.
It does mean that any server who wants to perform this on a badged endpoint in it’s immediate cspace but doesn’t have a capability to its own cspace can’t call this.
Is that a reasonable scenario? Servers that hand out caps to clients usually send copies of their own endpoint.
@RamboBones added this invocation, maybe he can remember specific reasons?
The reason this is a cnode invocation is a necessity of the seL4 model. Remember that frequently when you say ‘invocation’ what you are really saying is ‘an IPC where the kernel acts as the recipient and provides a reply’. For an endpoint there is already a recipient for the messages, it is whoever is waiting to receive from the endpoint. As a result an ‘invocation’ on an endpoint is synonymous with ‘RPC to some user space process’.
2 Likes
I think that reasoning is sufficiently astonishing that I think that should be explained in the documentation of the function but it makes sense.