Hello! I am trying to implement allocate_at() Libc:: function, which allocate memory region in given (desired) address. To implement I need to extend dataspace (as I understand, this is physical memory) at appropriate address, and later attach it to the local allocator.

I found that memory allocation code from base/include/region_map/region_map.h /** * Shortcut for attaching a dataspace at a predefined local address */ Local_addr attach_at(Dataspace_capability ds, addr_t local_addr, size_t size = 0, off_t offset = 0) { return attach(ds, size, offset, true, local_addr); }

does work for NOVA, but do not work for seL4 kernel for x86_64. This happens when I try to allocate 64k from pre-defined addresses like (try in order) 0xc000000000, 0x1c000000000, 0x2c000000000/etc… I create function int Libc::Mem_alloc_impl::Dataspace_pool::expand_at(size_t size, void * ptr, Range_allocator *alloc)

and inside it, in my call to try { new_ds_cap = _ram->alloc(size);

local_addr = _region_map->attach_at(new_ds_cap, addr_t(ptr), size); }

in seL4 it catch exception catch (Region_map::Region_conflict) {

while same calls in NOVA works ok. Problem happens in second call to attach_at(), new_ds_cap is ok.

Are there significant difference in the memory allocation process (for particular addresses ranges) between NOVA and seL4?

Thanks! Alexander