Sel4vm: Switch to use seL4_LargePageObject in VM's RAM register to reduce the memory overhead

I was working around with the default vm_minimal for qemu-arm-virt 64bits platform and tried to allocate 2GB RAM for the VM linux and got some allocation fail error.

./simulate: QEMU command: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic  -m size=4096  -kernel images/capdl-loader-image-arm-qemu-arm-virt 
ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at c1c94cc8.
Loaded DTB from c1c94cc8.
ELF-loading image 'kernel' to c0000000
ELF-loading image 'capdl-loader' to c0244000
Enabling hypervisor MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
Warning: Could not infer GIC interrupt target ID, assuming 0.
available phys memory regions: 1
reserved virt address space regions: 3
Booting all finished, dropped to user space
<<seL4(CPU 0) [decodeUntypedInvocation/205 T0x813f813400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>
run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1)
install_vm_devices@main.c:704 module name: map_frame_hack
install_vm_devices@main.c:704 module name: init_ram
ram_ut_alloc_iterator@guest_ram.c:304 Failed to allocate page
map_vm_memory_reservation@guest_memory.c:477 Failed to get frame for reservation address 0x8e83a000
Loading Kernel: 'linux'
Loading Initrd: 'linux-initrd'
Loading Generated DTB
vm_ram_touch@guest_ram.c:165 Failed to touch ram region: Not registered RAM region
32 bit ARM insts not decoded
Pagefault from [vm0]: write fault @ PC: 0xffff0000083bd92c IPA: 0xbffff000, FSR: 0x92000046
x0: 0xffff7dfffe63b000
x1: 0x0
x2: 0xfc0
x3: 0x4
x4: 0x0
x5: 0x40
x6: 0x3f
x7: 0x0
x8: 0xffff7dfffe63b000
x9: 0x0
x10: 0x40000000
x11: 0x0
x12: 0x3
pc: 0xffff0000083bd92c
x14: 0x0
sp: 0xffff000008e00000
spsr: 0x40000085
x13: 0xffff000008f7b530
x15: 0x18
x16: 0x1800
x17: 0x8b0
x18: 0xffffffffffffffff
x19: 0xbffff000
x20: 0xffff000008e08000
x21: 0xffff000008e4b308
x22: 0xffff7dfffe800000
x23: 0xffff000008e08000
x24: 0x0
x25: 0x0
x26: 0x0
x27: 0x0
x28: 0x40a50018
x29: 0xffff000008e03e60
x30: 0xffff000008a56160
Assertion failed: rt >= 0 (/host/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 620)

I found that it was caused by that the static memory pool of allocman was consumed up. Then I mentioned that the static memory pool was predefined default to 80MB size. (camkes-vm/templates/seL4AllocatorMempool.template.c at master · seL4/camkes-vm · GitHub)

I tried to add it to 140MB and VM Linux was boot successed. But 140MB / 2GB is an unexpected proportion to me.

Then I dived into the details of the related codes and found the default allocator for untyped frames is Buddy like and the RAM allocation is at a 4K granularity.

With this, a 2GB RAM region will need (2GB / 4KB) * 2 * (sizeof(node) + overload) = 120MB memory.

Here we may switch to use seL4_LargePage in VM RAM register, and the allocation granularity is 2M, and reduce the memory overhead to 120MB / 512 size.

Here is my trial:

project kernel/
diff --git a/src/plat/qemu-arm-virt/overlay-reserve-vm-memory.dts b/src/plat/qemu-arm-virt/overlay-reserve-vm-memory.dts
index f4c18af24..ddf682337 100644
--- a/src/plat/qemu-arm-virt/overlay-reserve-vm-memory.dts
+++ b/src/plat/qemu-arm-virt/overlay-reserve-vm-memory.dts
@@ -13,7 +13,7 @@
 		vm-memory@40000000 {
-			reg = <0x0 0x40000000 0x0 0x20000000>;
+			reg = <0x0 0x40000000 0x0 0x80000000>;

project projects/seL4_projects_libs/
diff --git a/libsel4vm/src/guest_ram.c b/libsel4vm/src/guest_ram.c
index 1d91906..24edfc5 100644
--- a/libsel4vm/src/guest_ram.c
+++ b/libsel4vm/src/guest_ram.c
@@ -169,14 +169,14 @@ int vm_ram_touch(vm_t *vm, uintptr_t addr, size_t size, ram_touch_callback_fn to = cookie;
     access_cookie.vm = vm;
     for (current_addr = addr; current_addr < end_addr; current_addr = next_addr) {
-        uintptr_t current_aligned = PAGE_ALIGN_4K(current_addr);
-        uintptr_t next_page_start = current_aligned + PAGE_SIZE_4K;
+        uintptr_t current_aligned = PAGE_ALIGN_2M(current_addr);
+        uintptr_t next_page_start = current_aligned + PAGE_SIZE_2M;
         next_addr = MIN(end_addr, next_page_start);
         access_cookie.size = next_addr - current_addr;
         access_cookie.offset = current_addr - addr;
         access_cookie.current_addr = current_addr;
         int result = vspace_access_page_with_callback(&vm->mem.vm_vspace, &vm->mem.vmm_vspace, (void *)current_aligned,
-                                                      seL4_PageBits, seL4_AllRights, 1, touch_access_callback, &access_cookie);
+                                                      seL4_LargePageBits, seL4_AllRights, 1, touch_access_callback, &access_cookie);
         if (result) {
             return result;
@@ -289,7 +289,7 @@ static vm_frame_t ram_ut_alloc_iterator(uintptr_t addr, void *cookie)
     if (!vm) {
         return frame_result;
-    int page_size = seL4_PageBits;
+    int page_size = seL4_LargePageBits;
     uintptr_t frame_start = ROUND_DOWN(addr, BIT(page_size));
     cspacepath_t path;
     error = vka_cspace_alloc_path(vm->vka, &path);

project projects/vm-examples/
diff --git a/apps/Arm/vm_minimal/qemu-arm-virt/devices.camkes b/apps/Arm/vm_minimal/qemu-arm-virt/devices.camkes
index e012012..28f845d 100644
--- a/apps/Arm/vm_minimal/qemu-arm-virt/devices.camkes
+++ b/apps/Arm/vm_minimal/qemu-arm-virt/devices.camkes
@@ -8,7 +8,7 @@
 #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB
 #define VM_RAM_BASE 0x40000000
-#define VM_RAM_SIZE 0x20000000
+#define VM_RAM_SIZE 0x80000000
 #define VM_RAM_OFFSET 0x00000000
 #define VM_DTB_ADDR 0x4F000000
 #define VM_INITRD_ADDR 0x4D700000
@@ -39,7 +39,10 @@ assembly {
         vm0.untyped_mmios = [
                     "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view)
-                    "0x40000000:29", // Linux kernel memory regions
+                    "0x40000000:30", // Linux kernel memory regions
+                    "0x80000000:30",
+        vm0.allocator_mempool_size = 0x100000; // 1MB
diff --git a/apps/Arm/vm_minimal/settings.cmake b/apps/Arm/vm_minimal/settings.cmake
index 42a5d86..a0b54a9 100644
--- a/apps/Arm/vm_minimal/settings.cmake
+++ b/apps/Arm/vm_minimal/settings.cmake
@@ -32,7 +32,7 @@ if(${PLATFORM} STREQUAL "odroidc2")
 if(${PLATFORM} STREQUAL "qemu-arm-virt")
     # force cpu
-    set(QEMU_MEMORY "2048")
+    set(QEMU_MEMORY "4096")
     set(KernelArmCPU cortex-a53 CACHE STRING "" FORCE)
     set(VmInitRdFile ON CACHE BOOL "" FORCE)
diff --git a/apps/Arm/vm_minimal/vm_minimal.camkes b/apps/Arm/vm_minimal/vm_minimal.camkes
index f6b98a4..d139e87 100644
--- a/apps/Arm/vm_minimal/vm_minimal.camkes
+++ b/apps/Arm/vm_minimal/vm_minimal.camkes
@@ -24,7 +24,7 @@ assembly {
         vm0.num_extra_frame_caps = 0;
         vm0.extra_frame_map_address = 0;
-        vm0.cnode_size_bits = 23;
+        vm0.cnode_size_bits = 18;
         vm0.simple_untyped24_pool = 12;


Welcome to Buildroot
buildroot login: root
# free -m
              total        used        free      shared  buff/cache   available
Mem:           2001          10        1988           1           1        1957
Swap:             0           0           0