Thanks Anna and Gernot for clarifying.
I think I should be able to make it work with Call/Reply. I don't really
like that the calling process isn't able to verify the identity/badge of
the replying process, but I realize why this is the case now. I have more
questions:
Is there a way on the receiving end to know if you have received a reply
cap?
Could the calling process somehow maliciously cause the replying process to
block on reply?
Thanks again,
Richard
On Tue, Sep 27, 2016 at 8:10 PM
On 28 Sep 2016, at 8:34 , Anna.Lyons@data61.csiro.au wrote:
This is a common misunderstanding: seL4_Call doesn’t generate a cap to the ep, but a cap to the thread that the seL4_Call went through (called the ‘reply cap’). seL4_Reply(Wait) sends directly to this thread via that capability, so the IPC is guaranteed to go to the caller.
What Anna describes is the implementation viewpoint.
The conceptual view is that seL4_Call() generates a transient (virtual) endpoint to which the invoker of Call gets a (transient, virtual) receive cap, and is made to block on a receive from that virtual EP. The destination of the Call gets the send cap to the virtual EP (which is called the Reply cap). The virtual EP vanishes once the reply cap is invoked.
Interposing on an EP should not be a problem.
Gernot _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-- Richard Habeeb Research Assistant, Computer Science, USF http://habeebr.bitbucket.org/