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 -- [email protected] > To unsubscribe send an email to [email protected] > _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
