Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

libsel4vm: add entries to vm structure #81

Merged
merged 1 commit into from
Mar 7, 2023
Merged

libsel4vm: add entries to vm structure #81

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions libsel4vm/include/sel4vm/guest_vm.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,8 @@ struct vm_ram_region {
* @param {vm_memory_reservation_cookie_t *} Initialised instance of vm memory interface
* @param {unhandled_mem_fault_callback_fn} unhandled_mem_fault_handler Registered callback for unhandled memory faults
* @param {void *} unhandled_mem_fault_cookie User data passed onto unhandled mem fault callback
* @param {int} clean_cache Flag to clean cache when loading images
* @param {int} map_one_to_one Flag to tell VMM to map memory 1:1
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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;

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

*/
struct vm_mem {
/* Guest vm vspace management */
Expand All @@ -94,6 +96,8 @@ struct vm_mem {
vm_memory_reservation_cookie_t *reservation_cookie;
unhandled_mem_fault_callback_fn unhandled_mem_fault_handler;
void *unhandled_mem_fault_cookie;
int clean_cache;
int map_one_to_one;
};

/***
Expand Down Expand Up @@ -177,6 +181,7 @@ struct vm_cspace {
* @param {vka_t *} vka Handle to virtual kernel allocator for seL4 kernel object allocation
* @param {ps_io_ops_t *} io_ops Handle to platforms io ops
* @param {simple_t *} simple Handle to hosts simple environment
* @param {seL4_Word} entry Entry address for the loaded kernel
* @param {char *} vm_name String used to describe VM. Useful for debugging
* @param {unsigned int} vm_id Identifier for VM. Useful for debugging
* @param {bool} vm_initialised Boolean flagging whether VM is intialised or not
Expand All @@ -199,6 +204,10 @@ struct vm {
vka_t *vka;
ps_io_ops_t *io_ops;
simple_t *simple;

/* vm entry address */
seL4_Word entry;

/* Debugging & Identification */
char *vm_name;
unsigned int vm_id;
Expand Down
10 changes: 2 additions & 8 deletions libsel4vmmplatsupport/src/arch/arm/guest_image.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ static int guest_write_address(vm_t *vm, uintptr_t paddr, void *vaddr, size_t si
return -1;
}

if (config_set(CONFIG_PLAT_TX1) || config_set(CONFIG_PLAT_TX2)) {
if (vm->mem.clean_cache) {
seL4_CPtr cap = vspace_get_cap(&vm->mem.vmm_vspace, vaddr);
if (cap == seL4_CapNull) {
/* Not sure how we would get here, something has gone pretty wrong */
Expand Down Expand Up @@ -202,13 +202,7 @@ static void *load_guest_kernel_image(vm_t *vm, const char *kernel_image_name, ui
/* Determine the load address */
switch (ret_file_type) {
case IMG_BIN:
if (config_set(CONFIG_PLAT_TX1) || config_set(CONFIG_PLAT_TX2) || config_set(CONFIG_PLAT_QEMU_ARM_VIRT)
|| config_set(CONFIG_PLAT_ODROIDC2) || config_set(CONFIG_PLAT_ZYNQMP)) {
/* This is likely an aarch64/aarch32 linux difference */
load_addr = load_base_addr + 0x80000;
} else {
load_addr = load_base_addr + 0x8000;
}
load_addr = vm->entry;
break;
case IMG_ZIMAGE:
load_addr = zImage_get_load_address(&header, load_base_addr);
Expand Down