Hello, while moving Genode's seL4 support to seL4 version 2, I stumbled over the dynamic allocation within untyped memory regions. In the old experimental branch that I used previously, the retype-untyped operation allowed me to manually specify an offset where the new kernel object should be placed within the untyped memory region. So I was able to manage the allocation of untyped memory manually. In short, I added each initial untyped memory region to a roottask-local "phys-mem" allocator. Each time when creating a kernel object, I asked this allocator for a region of the required size and alignment, determined the untyped-memory capability that belongs to the found region, and used this capability to create the kernel object(s) at the calculated offset within the untyped-memory region. This worked very well. After switching to version 2, I found the retype-untyped operation to lack the offset argument (which admittedly was never present in the non-experimental version). Instead of accepting an offset parameter, the kernel maintains a built-in allocator per untyped-memory region. (please correct me if my understanding is wrong) The allocator is basically a simple offset value ("FreeIndex") that is increased with each allocation. Since I no longer have the chance to specify the offset explicitly, I have to rely on the allocation policy of the kernel and hit the following problem: There exists an untyped memory region of size 0x2000. Initially, the FreeIndex is 0. Now, I am creating the following kernel objects within the untyped-memory region: 1. CNode with totalObjectSize 0x400: -> The allocation increases FreeIndex to 0x400. 2. CNode with totalObjectSize 0x800: -> The FreeIndex gets aligned to 0x800 (natural alignment of the to-be-created CNode). This creates a gap between 0x400 and 0x800. -> The allocation increases FreeIndex to 0x1000. 3. seL4_IA32_4K with a totalObjectSize 0x1000: -> The allocation increases FreeIndex to 0x2000. 4. CNode with totalObjectSize 0x400: <<seL4 [decodeUntypedInvocation/209 T0xe3fc9900 "rootserver" @2013228]: Untyped Retype: Insufficient memory (1 * 1024 bytes needed, 0 bytes available).>> Since FreeIndex equals the size of the untyped memory region, the kernel concludes that untypedFreeBytes is 0. Even though there exists a gap of 0x400 within the untyped memory region that satisfies the alignment of the to-be-created kernel object, the kernel won't allow me to use it. In contrast, with the retype-untyped-at-offset operation, such a situation never occurred. Right now, I am a bit puzzled about how to proceed and have the following questions in the back of me head: * What is the rationale behind fixing the allocation policy within untyped memory regions in the kernel. Doesn't this design contradict with the principle of avoiding policy in the kernel? In my specific case, this policy seemingly makes my life much more difficult. To use the kernel in a deterministic way, I would need to model the kernel's allocation behavior in the user land. * From what I gather from the kernel's source code, the built-in allocator would not allow me to reuse parts of untyped memory regions because 'FreeIndex' is always increasing. E.g., after revoking the CNodes of steps 1 and 2, I still cannot create any new kernel objects within the untyped memory region because FreeIndex remains equal the size of the untyped memory region. Is this correct? * Is it possible to give me the retyped-untyped-at-offset operation back? ;-) e.g., in the form of a patch? Or alternatively, are there any best practices that I could follow wrt managing untyped memory? Maybe I'm just approaching the problem from the wrong angle? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

First an explanation of the kernel branches/versions. The master branch has never had the retype at offset functionality, this has always been solely on the experimental branch. As the master branch is what is verified, this is what we release and are versioning. You could continue to use the experimental branch, and retain the use of retype at offset, but you will have to leave behind the nice versioning.

Now for a slightly more detailed exploration of retype strategies. Mark had things mostly correct here. Originally the kernel required you to retype an entire untyped at once. That is, you could take a single untyped and split it into N objects of equal size. Thus resulting in the common paradigm of splitting them in half as this provided an easy way to book keep and implement a user level allocator. But this is also inefficient, as you end up with many intermediate untyped capabilities.

To make efficient allocation practical untypeds were changed for so called 'incremental retype'. This is what you see currently in the verified kernel, with the freeIndex. The reason the freeIndex is monotonic increasing is because the kernel has no way to know if any previous memory is now free or not. The kernel only knows two things * Initially none of the memory of the untyped is used, so freeIndex is set to 0 * After the untyped is revoked all retyped objects are destroyed, so we know none of the memory is used, so freeIndex can be set to 0 But any other question of 'is there an object at this address?' cannot be efficiently answered. I say 'efficiently' because it is not impossible, rather the operation would be potentially very long running and a malicious user could exploit this. In particular a user could force an O(n) operation, where N is the amount of memory under control of the user.

But being able to retype many objects directly out of a single untyped does not help if you if you want to potentially free them and allocate other objects. For example, if you want to create some object of size X, you instead need to create an untyped of size X and then your object. Now if you want to delete that object you can, and create a new object of size X (or multiple objects of size < X) using that intermediate untyped.

On the experimental kernel there is a different in kernel data structure for managing capabilities (specifically a heap instead of a doubly linked list). Now the same question of 'is there an object at this address?' can be answered in O(log(n)) time, which is considered far more reasonable, and so retype at offset can be written.

For writing actual user level allocators what Mark said is basically what we tend to do. Have a buddy allocator, manage different untyped pool sizes etc. You can see examples of an untyped manager that we wrote for using on the master branch here https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/src/utspace/s…, note that it is part of a larger allocator but should still give some of the logic.