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

Hi Andrew,

On 22 Jan 2020, at 16:52, Andrew Warkentin wrote:

Speaking of things that would be useful for large dynamic systems, are there any plans to add seL4_Untyped_RetypeAtOffset from the old experimental branch to the current mainline kernel?

No, unfortunately not. This feature set (the “searchable CDT”) didn't make the cut for master. We dropped it, because with the incremental retype feature that did make it into master, we were able to figure out reasonable user-space solutions to everything we wanted to do, and the verification effort for the searchable CDT was too high for what the feature achieved.

I am writing a buddy untyped allocator for UX/RT, and being able to retype at arbitrary offsets would reduce overhead quite a bit because I could just retype from the highest-order untyped objects most of the time rather than having to create two child untyped objects per split.

It’s been a few years, so I might misremember the discussion from back then, but I think with incremental retype it should not be necessary any more to make child untypeds per object. The specific user-space design mostly depends on how you want to do object reclamation. I remember we were talking about using pools of untypeds for that, but it was just one of multiple options. I have the vague impression that someone wrote a user-space library for dynamic kernel object allocation somewhere that might be able to do what you need. Might have been just a prototype that was never published, though. If someone knows more, please jump in..

If not, I will probably end up re-adding it myself later on (sometime after UX/RT is running actual user programs).

If you have a specific use case that doesn’t work well with incremental retype, feel free to go into more detail of what you need. It’d be good to know if we missed something fundamental in that decision or if we’re just disagreeing on what “reasonable effort” in user space is ;-). We did accept some double book-keeping, i.e. tracking of things at user space that the kernel already knows, but we convinced ourselves that there should not be any big performance impact and that a reasonable object allocation abstraction could be implemented in a library. Cheers, Gerwin