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 <[email protected]> wrote:

> On 28 Sep 2016, at 8:34 , [email protected] 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
> [email protected]
> https://sel4.systems/lists/listinfo/devel
>
-- 
Richard Habeeb
Research Assistant, Computer Science, USF
http://habeebr.bitbucket.org/
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to