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 <[email protected]> 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 > <[email protected]> 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:[email protected]] On Behalf Of Yuxin Ren >> Sent: Friday, 17 October 2014 5:21 AM >> To: [email protected] >> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel > -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
