Would it be possible to allow for any untyped memory to be mapped into a VSpace as read-only before it is the retyped into other kinds of memory? It seems it would be useful if a user-level memory manager could introspect the state of the kernel objects for the purposes of debugging or for avoiding duplication of things like VSpace layout.
A possible way I could think of doing this would to introduce some concept of an ‘observer frame’ that can be retyped from an untyped object with no children that aren’t also observer frames. These frames would have to align to frame sizes available on the given platform and would have to be read-only when mapped. An untyped with only observer frames as children could then be retyped in all the ways that an untyped with no children can currently be retyped (i.e. used for kernel objects or smaller untypeds).
Doing so would allow a user-level mapping of the physical address space (to the regions where user-level has capabilities to the untypeds) and could allow a user not only to traverse virtual address translation tables, but also to introspect and traverse CSpaces and the CDT.
@gerwin.klein, do you think such a system could be permissable in a verified configuration?
Drawbacks of this idea would be that any untypes smaller than the smallest frame size or any kernel objects in memory to which untypeds aren’t provided (such as the objects for the initial task) can’t be mapped.