Hello Gerwin, On 2024-09-24 08:24, Gerwin Klein wrote:
(Apart from the whole discussion whether the concept of untyped object makes sense — for me, there are no untyped objects, only untyped caps and allocatable memory, but with the uniqueness constraint it doesn’t really matter, they are the same behaviourally).
I think they should have been called memory objects instead, "untyped" makes it sound more exotic than it actually is.
- IRQHandler: capIRQ
This just says what object the cap refers to, it’s not object state, it’s the pointer to the virtual object. Same also for SMC caps, IOPorts, SGI caps etc.
That makes sense and is indeed a better way of looking at it.
That is why a page cap is a page cap and not a frame cap: Because the object in question is not just the frame, it is a frame + mapping.
It’s possible that you can view it that way (I haven’t thought through all paths), but it is much more direct to view the cap itself as representing the mapping, because that is what it actually does and mappings behave a lot like caps. I’m not claiming it’s brilliant and easy to understand either way, it’s just what (mostly) solved the double parent problem you mention below.
My reasoning is: We have three parts here: The cap, the frame and the mapping. The same is true for UT: It has a cap, chunk of memory and some metadata. The second part we can call an object with some confidence, but the third part is neither a cap, nor really an object. But it is more an object than a cap, as what else is an object other than either memory or a collection of state? So in that sense both UT and pages are aggregate objects. It just happens that the metadata part fits inside the cap itself, at which point the cap itself becomes not just a reference, but part of the thing it gives access to and things get fuzzy.
For my own understanding, I don’t really like forcing everything into the simple cap/object paradigm when reality is more complex. Even in the case where you can prove that they are the same (Untypeds), I’ve found it easier to understand the behaviour when I mentally extend the cap concept and not try to have a layer of (mental) indirection via objects that aren’t really there. It can help explain things the first time because it matches existing concepts, but I find it dangerous for edge cases.
Agreed that forcing everything into cap/object paradigm isn't great, but that's what the manual does currently. Reality is that all caps are defined individually and any similarity in properties is an implementation choice. But to make talking about caps in the generic sense possible, it's much easier to pretend that they all conceptually have the same properties, like rights and badges, even for types that don't use them.
Page caps have the problem that they have two parents: Both the untyped they were allocated from and the VSpace the mapping is in, and seL4 can only clean up one automatically.
Agreed, that’s the source of the mapping info design wrinkle. The it is now seL4 can clean up automatically the one chain that matters for the kernel and can prevent the user from violating security on the other chain by more runtime checking (if used correctly, at least).
We tried a different design with shadow page tables many years ago that could do both automatically IIRC, but it was much more complex and needed more memory. Would still be worth revisiting this whole thing again at some point, but it’d be a fairly big redesign.
I don't think there is an easy solution and what seL4 has now is okay. Just the number of caps explodes exponentially if you use a lot of shared memory. (I ended up with more than 50K caps just for shared mappings.) Keeping track of a reverse mapping won't help for this though. For device memory it is very cumbersome to slice a UT in such way that the physical address is what you need, for that you just want to do a mapping without any hassle.
I think the page caps as they are cause a lot of unnecessary caps to be in the system. To me it would make more sense if you could have untyped for either kernel use or user space use, and if they're marked for user space use you can do virtual mappings on them without creating new caps. In a way being able to mark UT as device memory would do it, then it only needs to have one bit to mark if any kernel objects were allocated.
You’d still need to clean up mappings when the memory those mappings point into goes away. Not doing that could violate integrity eventually, because even if everything is user memory, you still need to account for which sub system the memory is for.
For top-level UTs things are simple: Once marked, always marked, and that's that. All it can be used for is doing mappings, it will never go away, so there is never a need to clean up. This is good enough for device memory (or shared memory regions defined in DTS). Sub-UTs are more complicated: If all mappings are be done via a PT which has the same parent UT as the mapping-only UT, everything is safe because then you know that all mappings are gone after revoking the parent UT. Because of this restriction it's probably at best an additional feature and not a replacement of Page caps. One thing that is currently hard to do is managing the available memory as you want from user space, because it gets it via very fragmented UTs at bootup, instead of nice lineair chunks. My idea doesn't solve that though, so perhaps a new concept is needed, like memory ranges that are not power-of-two. Greetings, Indan