Hello Alexander,
This happens when I try to allocate 64k from pre-defined addresses like (try in order) 0xc000000000, 0x1c000000000, 0x2c000000000/etc…
...
Are there significant difference in the memory allocation process (for particular addresses ranges) between NOVA and seL4?
On seL4, the virtual address space is limited to 8 GiB [1] on x86_64. On NOVA, the limit is much larger [2].
The memory allocation varies very much between the kernels. On seL4, it is particularly complicated because all virtual-memory structures have to be managed at the user level (Genode's core).
In general, one cannot make assumptions about the virtual address space layout that hold on all the different kernels. Even the location of the stack area may vary.
For this reason, 'attach_at' is not robust when used on the PD's region map. It is useful to manually manage the layout of so-called managed dataspaces (created via the Rm_session interface). Examples of such managed dataspaces are the linker area and the stack area.
[1] https://github.com/genodelabs/genode/blob/master/repos/base-sel4/src/core/pl... [2] https://github.com/genodelabs/genode/blob/master/repos/base-nova/src/core/pl...
Cheers Norman