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
