difference in genode memory allocation for NOVA and seL4

[Alexander Tormasov]

	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