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