Hi Sebastian,

Threads[1] can have (and usually do have) a CSpace associated with them, which is built up of CNode objects that hold capabilities. User level can manage how large these are and how they are organised. They would usually contain multiple, even many capabilities.

Capabilities can be transferred either by sending them explicitly via IPC or by sharing CNodes between threads. There is a separate discussion on the list ongoing about the IPC mechanism, because it currently allows sending of only one capability at a time, and the question is if there are situations where it would be necessary to atomically send more than one capability in one IPC.

Cheers,
Gerwin


[1]: Processes would usually come with some notion of separate address space, specific layout etc. Threads can share address spaces or live in separate ones. You can build the traditional notion of process with the seL4 mechanisms, but it’s not a primitive seL4 notion of itself.


On 16.02.2015, at 18:37, Sebastian Lau <sebastianlau25@gmail.com> wrote:

Cheers Gerwin and I've read some of the other 'posts' and I'm wondering, can a process only save or hold one capability and if so is there any way to build or have a workaround?


On Mon, 16 Feb 2015 20:24 Gerwin Klein <Gerwin.Klein@nicta.com.au> wrote:
Hi Sebastian,

when the kernel initialises, it creates a number of standard predefined capabilities and hands them to the initial thread (root task), including capabilities to the device regions in the machine, and Untyped capabilities to free memory. The initial task can then use these to set up the rest of the system (creating threads, page tables, IPC endpoints, loading executables, etc).

There is a separate tool (capDL-loader) that takes a static description of the capability distribution the initial thread should achieve and produces an initial thread for you that sets up the system accordingly. There is no requirement to use this tool, but it has been quite handy for us so far.

IPC is managed by kernel calls (Wait, Send, Call, Reply) that have an endpoint capability as argument.

Cheers,
Gerwin

On 16.02.2015, at 17:54, Sebastian Lau <sebastianlau25@gmail.com> wrote:

I have a question, how are capabilities assigned or given to processes? Is it through the kernel or can the root process (like init etc.) assign capabilities as well? Also is IPC managed by calls to the kernel? I have in mind to base something off of seL4 in the future but I'm not quite ready to start though and just want to get an understanding of how things work.

_______________________________________________
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.