Re: [seL4] Questions about Capability model

2016-09-21 Thread Daniel Wang 
Thank you for your quick response. by producer-consumer I mean if a message is 
sent to an EP and is received by another thread, is it gonna be consumed? Is 
there a way to send broadcast message to multiple receiver to the same EP? 

Thanks
-Dan
> On Sep 20, 2016, at 6:46 PM, gernot.hei...@data61.csiro.au wrote:
> 
>> On 21 Sep 2016, at 3:29 , Daniel Wang  wrote:
>> 
>> Hi all,
>> 
>> I’m new to the capability concept of seL4. Please correct me if I’m wrong. 
>> My understand of the capability is that it is a reference to a chunk of 
>> memory that allocated for specific purpose. Say if I want to do IPC between 
>> two threads A and B, I will need to apply an chunk of memory as endpoint, 
>> which give me a capability that I can pass from thread A to thread B is that 
>> correct? Also it is ok to assume the message passing mechanism in IPC is a 
>> producer-consumer model?
>> 
>> The reason I ask it because I’m thinking is it possible for three (or more) 
>> threads that need to communicate with each other using the same endpoint, or 
>> it has to be paired for each two of those threads to use an endpoint?
> 
> Caps are object references with implied access rights. They get produced by 
> the kernel when some Untyped memory is retyped into a specific object type 
> (eg a TCB or an array of endpoints).
> 
> Not sure what you mean with producer-consumer. Anyone who holds a cap with 
> send rights can send to the EP, anyone with a cap with receive rights can 
> receive. There can be any number of senders or receivers.
> 
> Gernot
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel


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

Re: [seL4] Questions about Capability model

2016-09-20 Thread Gernot.Heiser 
On 21 Sep 2016, at 9:07 , Daniel Wang  wrote:
> 
> Thank you for your quick response. by producer-consumer I mean if a message 
> is sent to an EP and is received by another thread, is it gonna be consumed? 
> Is there a way to send broadcast message to multiple receiver to the same EP? 

the IPC model is rendez-vous, synchronous message transfer. Broadcast a 
higher-level abstraction that has no place in a minimal microkernel. See also 
https://www.cse.unsw.edu.au/~cs9242/16/lectures/01-intro.pdf

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

Re: [seL4] Questions about Capability model

2016-09-20 Thread Gernot.Heiser 
> On 21 Sep 2016, at 3:29 , Daniel Wang  wrote:
> 
> Hi all,
> 
> I’m new to the capability concept of seL4. Please correct me if I’m wrong. My 
> understand of the capability is that it is a reference to a chunk of memory 
> that allocated for specific purpose. Say if I want to do IPC between two 
> threads A and B, I will need to apply an chunk of memory as endpoint, which 
> give me a capability that I can pass from thread A to thread B is that 
> correct? Also it is ok to assume the message passing mechanism in IPC is a 
> producer-consumer model?
> 
> The reason I ask it because I’m thinking is it possible for three (or more) 
> threads that need to communicate with each other using the same endpoint, or 
> it has to be paired for each two of those threads to use an endpoint?

Caps are object references with implied access rights. They get produced by the 
kernel when some Untyped memory is retyped into a specific object type (eg a 
TCB or an array of endpoints).

Not sure what you mean with producer-consumer. Anyone who holds a cap with send 
rights can send to the EP, anyone with a cap with receive rights can receive. 
There can be any number of senders or receivers.

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

[seL4] Questions about Capability model

2016-09-20 Thread Daniel Wang 
Hi all,

I’m new to the capability concept of seL4. Please correct me if I’m wrong. My 
understand of the capability is that it is a reference to a chunk of memory 
that allocated for specific purpose. Say if I want to do IPC between two 
threads A and B, I will need to apply an chunk of memory as endpoint, which 
give me a capability that I can pass from thread A to thread B is that correct? 
Also it is ok to assume the message passing mechanism in IPC is a 
producer-consumer model?

The reason I ask it because I’m thinking is it possible for three (or more) 
threads that need to communicate with each other using the same endpoint, or it 
has to be paired for each two of those threads to use an endpoint?

Thanks
-Dan
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel