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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
