difference in genode memory allocation for NOVA and seL4

[Norman Feske]

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/platform.cc#L511
[2]
https://github.com/genodelabs/genode/blob/master/repos/base-nova/src/core/platform.cc#L410

Cheers
Norman

-- 
Dr.-Ing. Norman Feske
Genode Labs

https://www.genode-labs.com · https://genode.org

Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth