Hi Norman! As I understand it, one way to deal with this kind of problem is to use retyping in combination with a user level buddy allocator. The idea is to maintain a list of untyped memory areas for each possible object size. In the scenario you've described, we start with one untyped memory object of size 0x2000. This means that there is no immediate way to handle a request for an object of size 0x400. But instead, we can find the next largest object size that is available---the 0x2000 object---and use retype to break it down in to two smaller untyped memory objects of size 0x1000. Of course, this is still not enough, so we repeat the process with two more retype calls so that we now have split the original untyped memory in to two untyped memory objects of size 0x400, one of size 0x800, and one of size 0x1000. Now one of those 0x400 objects can be used (via another call to retype) for the CNode that you wanted, and the remaining objects will be allocated in an appropriate manner to provide storage for the 0x800 CNode, the 0x1000 4K Page, and the final 0x400 CNode on each of the subsequent allocator calls in your scenario.
I don't believe there was any support at all for the FreeIndex scheme in early versions of seL4. But at some point, somebody noticed that there was unused space to store a FreeIndex in the capability object, and that this could be used to provide a lightweight mechanism for object allocation in simple programs that don't need a more sophisticated allocator. A simple server that requires only a static configuration of objects, for example, might be able to get by with a capability to just one small untyped memory area. At initialization time, it would a sequence of retype calls on that same untyped memory object to carve out the space that it needs for some appropriate collection of TCBs, endpoints, and other objects. Internally, the FreeIndex would be incremented after each retype, but once the initialization is complete, the server would be able to run without the need for any further allocation or allocator overheads. In other words, my *impression* (I'm not an authority here!) is that the "pure" seL4 way to handle problems like this is via repeated halving/retyping of larger objects. But I suspect that support for allocation from a single untyped memory via a monotonically increasing FreeIndex was added as a pragmatic step to simplify the task of constructing small applications. Hope this helps! All the best, Mark On Feb 4, 2016, at 5:12 AM, Norman Feske <[email protected]> wrote: > 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 > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
