libsel4vm: add entries to vm structure

[chrisguikema]

This commit adds three entries to the vm structure. The first is the entry address of the loaded kernel. The second is a flag to determine whether the cache should be cleaned when loading images to the guest's address space. The third flag is whether the VM should map memory 1:1.

These flags are necessary to differentiate VMs in a multiple VM setup. For example, if two VMs have kernels with different entry points, only one VM would run, and the other would fault.

Test with: seL4/camkes-vm-examples#31
Test with: seL4/camkes-vm#48

[wom-bat]

This look sliek a worthwhile improvement. Please rebase to current and retest, then we can merge in the new year.

[chrisguikema]

@wom-bat What needs to happen for these PRs to be merged? I don't want them to sit for too long and get stale.

[axel-h]

This one looks ok to merge, seem this is mostly blocked in the other two PRs now.

[axel-h]

How does map_one_to_one relate to ram_paddr_base and ram_base now? The explanation should be a bit more verbose about the impact and why this is not redundant.

[axel-h]

Sorry, my comment is a bit misplaced here. There seems no place where the CAmkES VM attributes are described, is there?

[chrisguikema]

map_one_to_one is used in the init_ram module. If true, the ram_ut_alloc_iterator function is used to map guest memory, which retypes untyped objects to create the guest memory mappings. The untypes are added in the VMM here:

        if (utType == ALLOCMAN_UT_DEV &&
            paddr >= ram_paddr_base && paddr <= (ram_paddr_base + (ram_size - 1))) {
            utType = ALLOCMAN_UT_DEV_MEM;
        }

When untypes are declared like simple_size24_pool in the .camkes files, generic untyped objects are added to the CSpace of the VMM and are mapped in the camkes_make_simple function:

                simple_data.untyped[0] = (camkes_untyped_t) {.cptr = 19, .paddr = make_frame_get_paddr(19), .size_bits = 24, .device = false};

This means the physical address of the untyped don't matter. However, you can also give a VMM untyped objects by using the untyped_mmio entry, which adds the untyped with a specific paddr:

            simple_data.untyped[12] = (camkes_untyped_t){.cptr = 31, .paddr = 134479872, .size_bits = 12, .device = true};
        
            simple_data.untyped[13] = (camkes_untyped_t){.cptr = 32, .paddr = 1073741824, .size_bits = 29, .device = true};

So the ram_paddr_base is a check that allows the user to specify the physical memory region that backs the guest memory map, instead of being backed by "random" memory regions. Benefits of this approach are that you can guarantee a guest is mapped 1:1, which allows for DMA transactions to work without an SMMU, but it would also allow the user to have fine-grained control over where guests end up in memory.

So for example:

#define VM_RAM_BASE 0x10000000
#define VM_RAM_SIZE 0x20000000
#define VM_PADDR_RAM_BASE 0x10000000

        vm0.vm_image_config = {
            "map_one_to_one" : true,
        };

You would need to provide the untyped object to 0x1000_0000 -> 0x3000_0000, something like this:

     vm0.untyped_mmios = ["0x10000000:29"];

But lets say you wanted the guest to be backed by the memory at 0x40000000 (full clarity i've never tried this), you'd provide the following:

#define VM_PADDR_RAM_BASE 0x40000000

     vm0.untyped_mmios = ["0x40000000:29"];

And if you didn't care about the backed memory, you'd do:

        vm0.vm_image_config = {
            "map_one_to_one" : false,
        };

        vm0.simple_untyped24_pool = 33;

[axel-h]

Thanks, that fits to my understanding. It would be good if we have this verbose explanation somewhere for the VMM settings somewhere. I don't want to make this a blocker for the merge, as it's a general thing actually.