Hi Gerwin, Thank you for getting back to me.

There has been no explicit decision about this. In terms of the API I think it might be reasonably easy to support this, but I haven't thought through the access control implications of it, i.e. if we could allow setting these bits as purely user-supplied attributes (assuming you present a cap to the table), or if they would need to be controlled by cap rights.

MPK

I will need to add this support in the kernel for my project at some point in the next few months. For when I try that: - I can create a fork or seL4 and start changing the kernel. I have no background in formal verification, so I cannot imagine that upstream will accept my changes. - Is there a guide on adding new systems calls to the kernel that I could follow along?

It's more a restriction of the current design of the relationship between virtual memory caps and virtual memory objects. Allowing sharing of lower-level tables would break that design (in that sense verification would of course forbid that). seL4 does allow sharing of address spaces and frames, though.

PT Sharing Thanks for the explanation. Do you see this restriction changing at any point? Sharing of PT would lead to smaller memory footprints when making a complete copy of the address space. Then again, the memory taken up by PT is typically of the order of 1% of the memory consumption of the process. So maybe it doesn't really matter. Sid

Cheers, Gerwin

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

This is very helpful. Thank you, Kent. -Sid On Sat, Mar 5, 2022 at 12:43 AM Kent Mcleod wrote:

[CAUTION: Non-UBC Email]

On Fri, Mar 4, 2022 at 4:16 AM Sid Agrawal wrote:

...

Hi Gerwin, Thank you for getting back to me.

...

There has been no explicit decision about this. In terms of the API I think it might be reasonably easy to support this, but I haven't

...

...

through the access control implications of it, i.e. if we could allow setting these bits as purely user-supplied attributes (assuming you

...

...

a cap to the table), or if they would need to be controlled by cap rights.

MPK

I will need to add this support in the kernel for my project at some

thought present point

...

in the next few months. For when I try that: - I can create a fork or seL4 and start changing the kernel. I have no background in formal verification, so I cannot imagine that upstream will accept my changes. - Is there a guide on adding new systems calls to the kernel that I could follow along?

A place to start would be looking at a commit where another invocation was added: https://github.com/seL4/seL4/commit/eb0553fa7563af1c5bb2dd2736c5563c49ef057e

...

...

It's more a restriction of the current design of the relationship

between

...

virtual memory caps and virtual memory objects. Allowing sharing of lower-level tables would break that design (in that sense verification would of course forbid that). seL4 does allow sharing of address spaces and frames, though.

PT Sharing

Thanks for the explanation. Do you see this restriction changing at any point? Sharing of PT would lead to smaller memory footprints when making a complete copy of the address space. Then again, the memory taken up by PT is typically of the order of 1% of the memory consumption of the process. So maybe it doesn't really matter.

It wouldn't be possible for the kernel to perform necessary TLB maintenance instructions in an efficient way. When a page would be unmapped from a shared page table, the kernel would be required to perform a TLB invalidate operation for all address spaces that the page may be mapped in. This could be a very large number of address spaces and so would require preemption points to break up a long running operation. However preemption points can lead to a different thread being scheduled and leaving the kernel. This thread now potentially has a VSpace that is affected by the in-progress operation or may want to also perform an invocation on the shared page table. The design and also the proofs would need to be updated to reflect an in-progress vspace invalidation in the kernel state. We would also need to handle whether other operations on the page table could be performed until the invalidation had completed and also how to handle revoking the page table etc. It ends up getting quite complicated unfortunately.

As Gerwin mentioned, you can already share entire VSpaces or share individual frames which so far has been sufficient to cover most sharing requirements.

Kent

...

Sid

...

Cheers, Gerwin

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems