Hello, I am trying to migrate a STM32MP2 Linux VM from the CAmkES VMM to the Microkit VMM. After filling the few platform definitions in vgic.h and vmm.h, I can boot the Linux VM up to the point where it faults during gic_init in linux: vmm|ERROR: unexpected memory fault on address: 0x4ac20004 This address happens to maps the GICC interface The Microkit VMM qemu example in the tutorial I used as a starting point only maps the GICV interface, so I tried adding the following region to the Microkit xml port description: <memory_region name="gic_cpu" size="0x2000" phys_addr="0x4ac20000" /> which cause the Microkit trace failure: ERROR: object 'frame_mr_gic_cpu_000000000', with paddr 0x00004ac20000..0x00004ac21000 is not in any valid memory region. Below are the valid ranges of memory to be allocated from: Valid ranges outside of main memory: [0x000000000000..0x000040000000) [0x000040000000..0x000048000000) [0x000048000000..0x00004a000000) [0x00004a000000..0x00004a800000) [0x00004a800000..0x00004ac00000) [0x00004ac00000..0x00004ac10000) [0x00004ac11000..0x00004ac12000) [0x00004ac12000..0x00004ac14000) [0x00004ac14000..0x00004ac18000) [0x00004ac18000..0x00004ac20000) [0x00004ac21000..0x00004ac22000) ... So there appears to be a hole exactly over 0x4ac20000..0x4ac21000, which is where the GICC registers live. Are these “valid ranges” derived directly from the kernel’s device resources to the root task? before checking the xml memory_region ? If so, what could cause the kernel to exclude exactly this page? Since this setup works with the CAmkES VMM, I would not expect a general device-tree parsing issue, Is there a way to trace valid device memory ranges construction in Microkit ? Thanks for any hints Best regards, Christian