Hi Yanyan, Thanks for your reply. I've already used only 1 core and a minimal device tree. Here's my apps/Arm/vm_minimal/rockpro64/devices.camkes: #include <configurations/vm.h> #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB #define VM_RAM_BASE 0xb0000000 #define VM_RAM_SIZE 0x10000000 #define VM_RAM_OFFSET 0 #define VM_DTB_ADDR 0xbf000000 //(LINUX_RAM_BASE + 0x0f000000) #define VM_INITRD_ADDR 0xbd700000 // DTB_ADDR - INITRD_MAX_SIZE assembly { composition {} configuration { vm0.linux_address_config = { "linux_ram_base" : VAR_STRINGIZE(VM_RAM_BASE), "linux_ram_paddr_base" : VAR_STRINGIZE(VM_RAM_BASE), "linux_ram_size" : VAR_STRINGIZE(VM_RAM_SIZE), "linux_ram_offset" : VAR_STRINGIZE(VM_RAM_OFFSET), "dtb_addr" : VAR_STRINGIZE(VM_DTB_ADDR), "initrd_max_size" : VAR_STRINGIZE(VM_INITRD_MAX_SIZE), "initrd_addr" : VAR_STRINGIZE(VM_INITRD_ADDR) }; vm0.linux_image_config = { "linux_bootcmdline" : "earlycon=uart8250,mmio32,0xff1a0000 earlyprintk=serial,ttyS2,1500000 debug loglevel=8 console=ttyS2,1500000", "linux_stdout" : "serial2:1500000n8", }; vm0.num_vcpus = 1; vm0.dtb = dtb([ {"path": "/serial@ff1a0000"}, ]); vm0.untyped_mmios = ["0xfff20000:16", // Interrupt Controller Virtual CPU interface (Virtual Machine view) "0xb0000000:27"]; /* vm0.irqs = [27]; // INTERRUPT_VTIMER */ } } My components/VM_Arm/plat_include/rockpro64/plat/vmlinux.h: #define LINUX_RAM_BASE 0xb0000000 #define LINUX_RAM_PADDR_BASE LINUX_RAM_BASE #define LINUX_RAM_SIZE 0x10000000 #define PLAT_RAM_END 0xc0000000 #define LINUX_RAM_OFFSET 0 #define DTB_ADDR 0xbf000000 #define INITRD_MAX_SIZE 0x1900000 //25 MB #define INITRD_ADDR (DTB_ADDR - INITRD_MAX_SIZE) //0xBD700000 #define IRQ_SPI_OFFSET 32 #define GIC_IRQ_PHANDLE 0x01 static const int linux_pt_irqs[] = { /*27, // VTCNT */ }; static const int free_plat_interrupts[] = { 50 + IRQ_SPI_OFFSET }; static const char *plat_keep_devices[] = { "/timer", "/xin24m", "/amba", "/pmu_a53", "/pmu_a72", "/psci", }; static const char *plat_keep_device_and_disable[] = {}; static const char *plat_keep_device_and_subtree[] = { "/interrupt-controller@fee00000", }; static const char *plat_keep_device_and_subtree_and_disable[] = {}; GIC_REDIST_SGI_PADDR is introduced in a GICv3 virtualization support code change at https://github.com/seL4/seL4_projects_libs/commit/143d48c0f99d3e35a9fd27deb7.... Do you know what does the error "sel4utils_reserve_range_at_no_alloc@vspace.c:595 Range not available at 0xfef10000, size 0x10000" mean? Thanks. Regards, Alex