> On 26 Jan 2020, at 12:55, Andrew Warkentin <andreww...@gmail.com> wrote:
>
> Actually, it would probably be better to make seL4_Untyped_Replace
> take a parent untyped capability and a child capability (of any type)
> of that untyped to revoke and replace. That would allow replacing an
> object any number of times.
Still not quite sure I understand correctly what seL4_Untyped_Replace would do.
The description above sounds like the following:
- c_u: a cap to an untyped
- c_o: a cap to an object retyped from that untyped, i.e. c_u is the direct
parent of c_o
- you want a retype operation that is equivalent to:
- revoke c_o
- delete c_o. There is now a hole in somewhere in the space covered by c_u.
- retype a new object of equal or smaller size into the space made
available by that hole
If I got that right, then this operation could be a bit harder to verify than
the merge operation, but probably not much. We’d probably eliminate the revoke
again and put that in user space, but you’d still be left with reasoning about
a potentially long-running delete, followed by a retype. The retype would be
justified by knowing that we have just reclaimed that area of memory and the
only other authority to it is the untyped and its parents. This is a bit
different to the reasoning we have so far for knowing that an area of memory is
unused (and also not pointed to by any other kernel objects). The usual
reasoning goes from invariants about untypeds without children, which wouldn’t
quite fit here. The proof here could probably still re-use most of that
reasoning, but it would need a bit more digging to be sure it doesn’t blow out
into a long project.
To be able to make use of the result of that free-space reasoning, the end of
the delete would have to be atomic with the beginning of the retype, otherwise
the authorising untyped could disappear during the call. That should be
reasonably easy inside the kernel.
In terms of kernel design, this one is harder to justify to the minimality
principle, because you could achieve the same effect with the additional
untyped cap that I think you were mentioning before, i.e. between c_u and c_o,
have a cap c_u2 of the size that is needed for c_o, and revoke/retype that one
(which also neatly covers what could go wrong if the authorising cap
disappears, e.g. because some overlord server revoked everything — the kernel
would catch that at invocation time of the in-between untyped).
Given the size of most objects, one untyped cap per object sounds like not too
bad of an overhead, but of course this also means managing the relationship
between these untypeds and the object caps.
Cheers,
Gerwin
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
