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
paddr=[c1b39000..c2fa90d7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at c1c94cc8.
Loaded DTB from c1c94cc8.
paddr=[c0242000..c0243fff]
ELF-loading image 'kernel' to c0000000
paddr=[c0000000..c0241fff]
vaddr=[80c0000000..80c0241fff]
virt_entry=80c0000000
ELF-loading image 'capdl-loader' to c0244000
paddr=[c0244000..c173cfff]
vaddr=[400000..18f8fff]
virt_entry=408d88
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
[c0000000..140000000]
reserved virt address space regions: 3
[80c0000000..80c0242000]
[80c0242000..80c0243ddc]
[80c0244000..80c173d000]
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
Context:
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
m--------
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 @@
ranges;
vm-memory@40000000 {
- reg = <0x0 0x40000000 0x0 0x20000000>;
+ reg = <0x0 0x40000000 0x0 0x80000000>;
no-map;
};
};
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
access_cookie.data = 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")
endif()
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)
endif()
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;
}
}
Runing
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
#