How to get a capability of a virtual address - Devel - lists.sel4.systems

newer
IPC performance for slowpath

How to get a capability of a virtual address

older
Where to begin for Linux on seL4...

Yuxin Ren

17 Oct 2014 17 Oct '14

5:21 a.m.

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

Attachments:

attachment.html (text/html — 3.6 KB)

Reply

Sign in to reply online Use email software

Show replies by date

Kevin Elphinstone

17 Oct 17 Oct

4:36 p.m.

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.

Reply

Sign in to reply online Use email software

Yuxin Ren

18 Oct 18 Oct

5:03 a.m.

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.

Reply

Sign in to reply online Use email software

Tim Newsham

8:25 a.m.

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

Reply

Sign in to reply online Use email software

Yuxin Ren

8:41 a.m.

Your reply is really helpful. Bur if I want to use those initial caps, for example share it with others, is there any functions to get those caps? I mean if I have to hard-code to use those caps? For example, I want to use cap for BootInfo frame, I should hard-code it as "0x9"? Thank you very much. Yuxin On Fri, Oct 17, 2014 at 5:25 PM, Tim Newsham wrote:

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.

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

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

On Fri, Oct 17, 2014 at 8:03 AM, Yuxin Ren wrote: 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

Reply

Sign in to reply online Use email software

Tim Newsham

9 a.m.

use the CPTR listed in the documentation in APIs that require a CPTR, such as putting them into a the caps[] buffer of an IPC_Buffer when sending a message to another thread or passing them into the Mint API to mint a new capability based on it. The use of capabilities is covered extensively in http://sel4.systems/Docs/seL4-manual.pdf On Fri, Oct 17, 2014 at 11:41 AM, Yuxin Ren wrote:

Your reply is really helpful. Bur if I want to use those initial caps, for example share it with others, is there any functions to get those caps? I mean if I have to hard-code to use those caps? For example, I want to use cap for BootInfo frame, I should hard-code it as "0x9"?

Thank you very much. Yuxin

On Fri, Oct 17, 2014 at 5:25 PM, Tim Newsham wrote:

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

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

Reply

Sign in to reply online Use email software

3685

Age (days ago)

3686

Last active (days ago)

Download

5 comments

3 participants

tags

participants (3)

Kevin Elphinstone
Tim Newsham
Yuxin Ren