On 1/22/20, Klein, Gerwin (Data61, Kensington NSW) <gerwin.kl...@data61.csiro.au> wrote: > > 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. >
As I said, the base allocator is going to be a form of buddy allocator, which will use associative arrays to track mappings of addresses to capabilities. On top of that there is going to be a slab allocator that allocates a separate pool of untyped objects for each kernel object type, using bump allocation within each untyped. Since only bump allocation is possible within an untyped in the current version of seL4, the buddy allocator will have to allocate new untyped objects for each split in most cases. If retyping at arbitrary offsets were possible, there would be no need for the buddy allocator to keep any capabilities other than the top-level untyped objects and the objects requested by client code (intermediate orders could just use bitmaps). Also, there would be no need to use slab allocation for user pages; using slab allocation for user pages would probably lead to more fragmentation than allocating them directly from the buddy allocator. > > 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.. > Even if it were actually released, most likely it wouldn't be particularly useful for my purposes since I'm writing my root server in Rust rather than C. Speaking of unreleased code, the fact that there is any makes me worried that I may have to fork seL4 someday just because of the rather closed development process, which is a mismatch for the fully open, copyright-assignment-free development process (akin to that of the Linux kernel) that UX/RT will have. UX/RT is meant to be an OS for the real world and not yet another systems research project that is completely ignored outside academia. Therefore I am going to do everything I can to give it the best chance at real-world success, which includes a development model with as few barriers to contributing as possible. However, seL4 does seem to be a good match for UX/RT in general despite the development model and a few possible missing features. All of the other L4 kernels have architectural issues that would make them less than ideal for UX/RT, and none has a Rust toolchain for root servers AFAIK. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
