QEMU Virt build fails when allocating >512 MiB of contiguous memory

[rsmith-ssc]

Good afternoon,

Just started testing around with SEL4, so this could likely be user error rather than an issue with Microkit (ver 2.0.1). I am currently able to build a system using the simple example in LIBVMM as a base with my custom Linux kernel and initrd images with a few tweaks to dts and system files. However, if I try to define a memory region > 512 MiB in the system configuration I get the following error:

ERROR: failed to allocate objects for 'Page(2 MiB): MR=guest_ram #0' of object type 'SEL4_LARGE_PAGE_OBJECT'
ERROR: allocation size (768 MiB) is greater than current maximum size for a single allocation (512 MiB)

I get the same error when attempting to create two 512 MiB memory regions that are contiguous. Is this a bug or is there any configuration to enable memory regions > 512 MiB? The research I've done points toward potential solutions in CAmkES, but I would very much prefer to stick with Microkit.

See following configs to make sure I am not missing something obvious. I am updating these and also the VMM.c GUEST_RAM_SIZE definition to match total ram size:

dts.overlay:

/*
 * Copyright 2024, UNSW
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */
/ {
    /* Need to specify how much RAM the guest will have */
    memory@40000000 {
        device_type = "memory";
        reg = <0x00 0x40000000 0x00 0x30000000>;
    };

    flash@0 {
        status = "disabled";
    };

    chosen {
        stdout-path = "/pl011@9000000";
        bootargs = "earlycon=pl011,0x9000000 earlyprintk=serial debug loglevel=8 root=/dev/vda";
        linux,stdout-path = "/pl011@9000000";
        linux,initrd-start = <0x4f000830>;
        linux,initrd-end = <0x60000000>;
    };
};

system file:

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <memory_region name="guest_ram" size="0x30_000_000" page_size="0x1000" />
    <memory_region name="serial" size="0x1_000" phys_addr="0x9000000" />
    <memory_region name="gic_vcpu" size="0x1_000" phys_addr="0x8040000" />
    <protection_domain name="VMM" priority="254">
        <program_image path="vmm.elf" />
        <map mr="guest_ram" vaddr="0x40000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
        <virtual_machine name="linux" >
            <vcpu id="0" />
            <map mr="guest_ram" vaddr="0x40000000" perms="rwx" />
            <map mr="serial" vaddr="0x9000000" perms="rw" cached="false" />
            <map mr="gic_vcpu" vaddr="0x8010000" perms="rw" cached="false" />
        </virtual_machine>
        <irq irq="33" id="1" />
    </protection_domain>
</system>

run command:

make MICROKIT_BOARD=qemu_virt_aarch64 MICROKIT_SDK=~/microkit-sdk-2.0.1/ LINUX=kernel.bin  INITRD=rootfs.cpio.gz qemu

[Ivan-Velickovic]

Hi @rsmith-ssc, this is a bug (or more accurately, a limitation) with the way the Microkit tool allocates memory from seL4 untyped memory regions. The issue is that the current strategy Microkit uses is that it will try to allocate all the kernel objects necessary (in this case 2MiB pages) from a single untyped. This is fine until you start to allocate large memory regions that use more memory than the biggest untyped (in this case 512MiB). This fails, even though there is enough memory available, it's just spread over multiple untypeds.

Sorry about this, for now it means that your Linux virtual machine is limited to 512MiB of RAM on QEMU. I will try get this fixed this week.

[rsmith-ssc]

Understood, appreciate the quick response. I'll check again next week and see if I can assist with testing on the issue branch.

[Ivan-Velickovic]

Hi @rsmith-ssc, apologies for the long delay.

This should now be fixed as of PR #337 being merged.

If you go to https://github.com/seL4/microkit/actions/runs/18930185432, at the bottom you will see a pre-release build of the SDK. If you download that and then unzip and then untar (GitHub always zips artifacts...) you'll have an SDK that should fix your issue. Building from source will also work if you want to do that instead.

Just note that to your SDF you'll have to apply one change:

-<protection_domain name="VMM" priority="254">
+<protection_domain name="VMM" priority="253">

Let us know if that fixes it for you.

[Ivan-Velickovic]

Hi @rsmith-ssc I'm going to close this for now since I believe we've fixed the issue. If you run into anything else or still have issues with using more memory on QEMU let us know.