Hello Gerwin,
On 2024-09-23 12:58, Gerwin Klein wrote:
The other cap state is also not for
properties of the object the cap points to. That’s probably where
the main confusion is, because it sounds like object state. Maybe one
analogy is that it is state of a "view" of the object.
What does make things weird is if object state is stored in caps,
because that causes for the user unexpected limitation to what you
can do with the caps.
Hm, I think it comes down to a question of design perspective in the
end.
In terms of behaviour, there is no object state stored in caps in
seL4, it’s always been cap state.
I don't think that's true:
- Untyped: capFreeIndex
- IRQHandler: capIRQ
- SchedControl: core
E.g. Aarch64:
- Frames, PT, VSpace: capFMappedAddress
- ASIDPool: capASIDBase and capASIDPool
All that is part of the object state, or even the object itself if
there is nothing else.
You fundamentally can’t really
store object state in caps, because caps and objects are
observationally different — to change actual object state stored in
caps you’d have to find all caps for that object and change it there
as well.
Exactly, and that's why caps with object state in them can't be copied
or have other restrictions, if that state is not read-only.
E.g. the mapping info for a page is where the concept of "cap" is
stretched a little. The mapping info is a property of the mapping, not
of the frame object the cap points to. I.e. the mapping is represented
by the cap, not the frame object. You could choose to not represent
the mapping with a cap, and instead use a new kind of object or some
other mechanism (that’s where it’s a question of design
perspective), but the cap state is not trying to represent object
state of the frame object. It’s something in addition to the object
that can be different in each cap to the object.
Because frames can be mapped in multiple locations and address spaces,
and all these mappings point to the same frame and represent authority
to read/write etc, modelling that situation as state in the cap was a
reasonable fit, but it does stretch the concept a bit, because it’s
now more than just pointer + authority.
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.
Untyped have the same property: They point to a chunk of memory, but
the untyped object is more than that, and that extra state is stored
in the cap itself.
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.
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.
The restrictions on copying are mostly not because of the cap state
(some are), but because of the limited depth of the capability
derivation tree (CDT). If we added another pointer to all caps (which
would double cap size), the CDT could be a proper tree and we could
remove a lot of these strange restrictions. Currently the cap state
sometimes doubles as indication on which level in the CDT a cap is,
and that’s where a lot of the copying restrictions come in.
That's true for IRQControl caps and other such caps that are almost
stateless and can be derived somehow into other caps, like IRQHandlers.
Then it's a matter that each cap only having one parent and revocation
becomes impossible or tricky to get right. But for others like untyped
the restrictions are because there is writeable state in the cap itself.
Anyway, cap restrictions depend on implementation details which are
opaque to the user.
Greetings,
Indan
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
