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

Reply via email to