Re: [seL4] Determining when would-have-blocked

Hi Corey, The badge doesn't help with NBSend, in fact the kernel won't tell you if NBSend has succeeded or not. This is intentional, to prevent a back channel when communicating between untrusted components. Cheers, Anna. On 4/01/2016 10:13 am, Gerwin Klein wrote:

Hi Corey,

yes, the idea is that endpoints are badged when you send messages.

Cheers, Gerwin

...

On 2 Jan 2016, at 05:58, Corey Richardson wrote:

Looking at the manual and the C impl, it seems there is no robust way to determine if a non-blocking send failed. How should an application handle this?

NBRecv sets the badge register to zero when the recv "failed" - is it expected that most/all endpoints will be badged? I'm still trying to get a feel for what a system designed for this model would look like.

-- cmr +16032392210 http://octayn.net/ _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

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.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel