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