The first process is special and gets certain capabilities
from the kernel which are documented in the kernel
specification and guide.  See section 8.1 "Initial
Thread's Environment" of http://sel4.systems/Docs/seL4-manual.pdf.

After this point your OS can keep track of whichever
capabilities it creates and assigns to other processes
in whatever manner it chooses.

On Fri, Oct 17, 2014 at 8:03 AM, Yuxin Ren <ryx@gwmail.gwu.edu> wrote:
> Hi Kevin,
>
> First, thank you for your reply very much.
> But I cannot understand those very well.
> Generally speaking, how does the OS personality get and know all caps for
> its own?
> More accurate, take the init process for example(which I am focusing on),
> how does it know which cap it has?
> I think it has to resort to the kernel, as the init process is created by
> the kernel, and I assume the kernel will set up caps for it.
>
> Thanks again.
> Yuxin
>
> On Fri, Oct 17, 2014 at 1:36 AM, Kevin Elphinstone
> <Kevin.Elphinstone@nicta.com.au> wrote:
>>
>> In general, seL4 provides low-level  mechanisms, not high-level
>> abstractions.
>>
>>
>>
>> The vm model and process model are high-level abstractions of an OS
>> personality on seL4, and as such, the OS personality is expected to keep the
>> information required to implement those abstractions.
>>
>>
>>
>> So I would expect the OS personality running on seL4 to keep track of the
>> frame caps used to create VM objects/address-spaces, which threads are in
>> what processes, etc..
>>
>>
>>
>> There are some libraries that ease building OS personalities, which are
>> the ones you are using. Those libraries walk a thin line between helpful
>> libraries to aid the construction of OS personalities, and largely defining
>> the OS personality.
>>
>>
>>
>> We make no claims as to the line striking the right balance, this is
>> evolving over time, with tension pulling the line in either direction.
>>
>>
>>
>> So if my understanding of the current support libraries is correct, what
>> you’re after is part of the book-keeping you should be managing when
>> creating your OS personality on seL4 – it is not provide by the libraries
>> nor seL4.
>>
>>
>>
>> -          Kevin
>>
>>
>>
>>
>>
>> From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Yuxin Ren
>> Sent: Friday, 17 October 2014 5:21 AM
>> To: devel@sel4.systems
>> Subject: [seL4] How to get a capability of a virtual address
>>
>>
>>
>> Hi All,
>>
>>
>>
>> In sel4, how can a process/thread get the capability of its virtual
>> address?
>>
>> I know there is function
>>
>>  vspace_get_cap(vspace_t *vspace, void *vaddr)
>>
>>
>>
>> But how can I know the current vspace the process/thread is in?
>>
>>
>>
>> Thank you very much.
>>
>> Yuxin
>>
>>
>> ________________________________
>>
>> 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
>



--
Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com