As an alternative to seL4_Untyped_RetypeAtOffset, would it maybe be possible to add an seL4_Untyped_Merge invocation that would take two adjacent untyped objects and a third slot for a destination and merge them into a single untyped, revoking the original two untypeds, and an seL4_Untyped_Replace invocation that would be similar to seL4_Untyped_Retype except that it would revoke the original untyped (failing if called on an initial untyped object). These would allow almost comparable optimizations to seL4_Untyped_RetypeAtOffset (although some "filler" untyped objects for free blocks would still have to be created). Could these be implemented without a searchable CDT? Would they be any easier to verify?
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
