Hello Alex, What is GIC_REDIST_SGI_PADDR? The VMM emulates GICD and GICR (per core). If my memory serves right, the Linux kernel code looks for an end flag when scanning the GICR region, that is probably why the scan fails if you change the size. I suggest you start with single core and trim the device tree to just include serial, timer, GIC, memory, and core nodes. Regards, Yanyan From: Alex Ling via Develmailto:devel@sel4.systems Sent: Friday, 16 July 2021 10:16 PM To: devel@sel4.systemsmailto:devel@sel4.systems Subject: [seL4] Cannot reserve memory for camkes VM guest Hi All, I'm trying to bring up camkes VM Linux guest on Firefly RK3399 board which is with a GICv3 ARMv8. I'm using the "rockpro64" target and my work is based on [1] and [2]. When I run the "capdl-loader-image-arm-rockpro64", there's error "Range not available at 0xfef10000, size 0x10000". Bootstrapping kernel Booting all finished, dropped to user space Undelivered IRQ: 132 Install gic v3 sel4utils_reserve_range_at_no_alloc@vspace.c:595 Range not available at 0xfef10000, size 0x10000 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0xfef10000 of size 65536 vm_install_vgic_v3@vgic_v3.c:87 Error installing vgic Assertion failed: !err (/mnt/data3/projects/rk3399/build/seL4/camkes-vm-app/projects/vm/components/VM_Arm/src/main.c: main_continued: 1098) Here's my projects/seL4_projects_libs/libsel4vmmplatsupport/plat_include/rockpro64/sel4vmmplatsupport/plat/devices.h content: #define GIC_VERSION_3 #define GIC_PADDR 0xfee00000 #define GIC_DIST_PADDR (GIC_PADDR + 0x00000000) #define GIC_DIST_SIZE 0x10000 #define GIC_REDIST_PADDR 0xfef00000 #define GIC_REDIST_SIZE 0xC0000 #define GIC_REDIST_SGI_PADDR (GIC_REDIST_PADDR + 0x00010000) #define GIC_REDIST_SGI_SIZE 0x10000 I think the problem is related to GIC_REDIST_SIZE. I set it to 0xC0000 according to the rockpro64 device tree file in kernel/tools/dts/rockpro64.dts interrupt-controller@fee00000 { compatible = "arm,gic-v3"; #interrupt-cells = < 0x04 >; #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; interrupt-controller; reg = < 0x00 0xfee00000 0x00 0x10000 0x00 0xfef00000 0x00 0xc0000 0x00 0xfff00000 0x00 0x10000 0x00 0xfff10000 0x00 0x10000 0x00 0xfff20000 0x00 0x10000 >; interrupts = < 0x01 0x09 0x04 0x00 >; phandle = < 0x01 >; I tried to reduce it to 0x10000 and it can boot to VM guest but the guest Linux will fail in gic_iterate_rdists() because it cannot read from GIC's GICR_TYPER register correctly. Did I miss anything? Any suggestion is highly appreciated. Thank you very much! [1] https://github.com/seL4/seL4/pull/378 [2] https://github.com/seL4/seL4_projects_libs/tree/sylvain/gicv3 Regards, Alex _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems