Troubles booting VM with large memory(e.g VM_RAM_SIZE >= 2048MB)

seL4 kernel
1

Hello all,

Reference to seL4 Docs/Projects/CAmkES ARM VMM, I have successfully run a VM (a Linux guest OS and config VM_RAM_SIZE = 1024MB) on a new ARM(ArmV8a CortexA55) platform.
But when I tried to increase the ram size assigned to VM, I encountered the following error:

==============================================================================
ram_ut_alloc_iterator@guest_ram.c:295 Failed to allocate page
map_vm_memory_reservation@guest_memory.c:470 Failed to get frame for reservation address 0xae7c0000 reservation_size:60000000

…

vm_ram_touch@guest_ram.c:160 Failed to touch ram region: Not registered RAM region
32 bit ARM insts not decoded

Pagefault from [Linux]: write fault @ PC: 0xffff000008d9132c IPA: 0xaffff000, FSR: 0x92000046
Context:
x0: 0xffff7dfffe639000
x1: 0x0
x2: 0xfc0
x3: 0x4
x4: 0x0
x5: 0x40
x6: 0x3f
x7: 0x0
x8: 0xffff7dfffe639000
x9: 0x0
x10: 0x1000
x11: 0x6f01c3b8
x12: 0xc0000000
pc: 0xffff000008d9132c
x14: 0x0
sp: 0xffff000009668d80
spsr: 0x40000085
x13: 0x60000000
x15: 0x4
x16: 0x1800
x17: 0xffff7dfffe81c3b4
x18: 0x8
x19: 0xaffff000
x20: 0xffff0000096a1fd0
x21: 0xffff7dfffe80009c
x22: 0x58389df
x23: 0xffff0000091ce000
x24: 0x4b78e0
x25: 0x47b87c
x26: 0x0
x27: 0xa0000000047b818
x28: 0x614f0018
x29: 0xffff000009643eb0
x30: 0xffff0000094f7ad0
m--------
Assertion failed: rt >= 0 (/home/hjl/workdir/vmm_sel4_sdx_android/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 623)

config file for reference：

  1. overlay dts
    reserved-memory {
    #address-cells = < 0x02 >;
    #size-cells = < 0x02 >;
    ranges;

     vm-memory@60000000 {
     reg = < 0x00 0x60000000 0x00 0x60000000 >;
     no-map;
 };

    };

  2. devices.camkes

    #define VM_INITRD_MAX_SIZE 0x5000000 //80 MB
    #define VM_RAM_BASE 0x60000000
    #define VM_RAM_OFFSET 0
    #define VM_RAM_SIZE 0x60000000
    #define VM_DTB_ADDR 0x6F000000
    #define VM_INITRD_ADDR 0x6A000000

    vm0.untyped_mmios = [
    “0x35436000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view)
    /* The purpose of these untyped regions is to force the untyped
    * allocator to treat this memory region as reserved so that when we
    * try to ensure that the VMM is placed into this region in RAM, it
    * will definitely be available for placement.
    *
    * This address pertains to vm-memory@60000000 in the overlay DTS
    */
    “0x60000000:28”, // RAM
    “0x70000000:28”, // RAM
    “0x80000000:28”, // RAM
    “0x90000000:28”, // RAM
    “0xa0000000:28”, // RAM
    “0xb0000000:28”, // RAM
    ];

  3. guest linux dts

    memory@60000000 {
    device_type = “memory”;
    reg = <0x00 0x60000000 0x00 0x60000000>;
    };
    ==============================================================================

In contrast, I tried to expand the VM memory based on QEMU and encountered the same problem.
config file for reference：

  1. settings.cmake
    if(${PLATFORM} STREQUAL “qemu-arm-virt”)
    set(QEMU_MEMORY “4096”)
    set(KernelArmCPU cortex-a53 CACHE STRING “” FORCE)
    set(VmInitRdFile ON CACHE BOOL “” FORCE)
    endif()

  2. overlay-reserve-vm-memory.dts
    reserved-memory {
    #address-cells = < 0x02 >;
    #size-cells = < 0x02 >;
    ranges;

     vm-memory@40000000 {
 	reg = <0x0 0x40000000 0x0 0x50000000>;
 	no-map;
 };

    };

  3. devices.camkes

    #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB
    #define VM_RAM_BASE 0x40000000
    #define VM_RAM_SIZE 0x50000000
    #define VM_RAM_OFFSET 0x00000000
    #define VM_DTB_ADDR 0x4F000000
    #define VM_INITRD_ADDR 0x4D700000

    vm0.untyped_mmios = [
    “0x8040000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view)
    “0x40000000:29”, // Linux kernel memory regions
    “0x60000000:29”, // Linux kernel memory regions
    “0x80000000:28”, // Linux kernel memory regions
    ];

  4. guest linux dts

    memory@40000000 {
    reg = <0x0 0x40000000 0x0 0x50000000>;
    device_type = “memory”;
    };

Anyways anyone any help can provide would be awesome and thanks in advance for any help!

2

I have also struggled to get VMs booting with large memory sizes. Back when I was looking into the problem I made this write up on some of my findings. It was for a RHEL8 VM running on x86 so your mileage my vary, but I figure it might give you some new ideas to try. Hope it helps.

seL4 x86 VM RAM guide

This covers how to allocate higher RAM amounts to VMs on seL4 on x86. This is
far from a conclusive guide but does cover some findings.

An old Dell Optiplex was used as the target.

There are 3 main things to think about when allocating larger RAM amounts for a
VM; allocman virtual pool size, memory overhead, and untyped memory.

Allocman Virtual Pools

In projects/camkes-vm/components/Init/src/main.c there is a define for
ALLOCMAN_VIRTUAL_SIZE at 400000000 (notice this isn’t hex). This pool is used
by VMM to store overhead info on the VM. It was found that this size of
400000000 maxes out at 5.5GB allocated to a VM. This pool should be increased if
the VM needs more than 5.5GB. Reassigning a value to this is more of an art than
a science so guess and check.

Memory Overhead

The VMM and seL4 kernel both have a memory overhead that needs to be taken into
account when allocating memory for a VM. We have found that seL4 needs
350MB. The VMM probably needs the overhead for the ALLOCMAN_VIRTUAL_SIZE and
BRK_VIRTUAL_SIZE, so that is another thing to keep track of.

To get a rough idea of how much memory is left for VM allocation take the total
system memory and subtract 350MB, and the ALLOCMAN_VIRTUAL_SIZE and
BRK_VIRTUAL_SIZE. This result is not exact and will depend on actual overhead
numbers but gives an idea for VM allocation.

Untyped Pools

The untyped pools for each VM in the camkes file is the most tedious guess and
check part about VM RAM allocation. (i.e.vm0.simple_untyped30_pool = 7;) Using
the rough idea of how much memory is left from last sections, start give chunks of
memory to the VM. Start with 30 bit (1GB) chunks then move down if more granularity
is needed. Also giving something like 300 12 bit chunks also may help. It also may be
necessary to over allocate untyped for a VM.

Example: on the Optiplex with 10 GB of RAM is was seemingly not possible to
allocate a VM 8GB. This is probably because of all of the memory overhead. After
installing more RAM so the Optiplex had 16GB of RAM, 8GB of RAM was allocatable
to the VM. The final config was 9 30 bit pools (9 * 1GB) and 300 12 bit pools
(300 * 1KB).

3

Thank you for your suggestion. I tried to increase the size of allocator_mempool and finally solved this problem