This is very helpful. Thank you, Kent. -Sid
On Sat, Mar 5, 2022 at 12:43 AM Kent Mcleod <[email protected]> wrote: > [CAUTION: Non-UBC Email] > > On Fri, Mar 4, 2022 at 4:16 AM Sid Agrawal <[email protected]> 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 > 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? > > > > 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 -- [email protected] > > > To unsubscribe send an email to [email protected] > > > > > _______________________________________________ > > 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]
