Re: [seL4] Are there any plans to re-add seL4_Untyped_RetypeAtOffset?

On 26 Jan 2020, at 12:55, Andrew Warkentin 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