My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark
On Sat, Dec 18, 2021 at 7:57 AM Richard Clark <richard@trustedst.com> wrote:
My VM's can't seem to be untied from actual physical memory....
I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But
On platforms that don't have an IOMMU, memory would be mapped with physical addresses equal to virtual addresses so that pass-through devices that use DMA would still work.
I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand?
Trying to answer this for seL4 version 8... Is your question for Arm or x86? Are you using CAmkES? x86 VMs already have mappings that have the same virtual but different physical addresses for required mappings in the low 1MiB of each guest's physical address space and this is supported by the kernel. You would need to make sure that the vmm doesn't think it's trying to create direct mappings for DMA and it should fall back to using arbitrary physical addresses for a configured virtual address range for ram. You would need to follow the implementation of main.c in the Init component in the camkes-vm repository (assuming you're using camkes) to see how it decides to handle Ram device setup. From my recollection and a quick look through the code it supports either direct mapping or mapping using arbitrary physical frames. seL4 version 8.0 didn't support multiple Arm VMs as far as I can recall.
For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time:
map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2];
reservation_t res; int err;
/* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; }
/* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; }
vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]);
printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; }
printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; }
err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12);
vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; }
printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; }
Help is greatly appreciated!
Richard H. Clark _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
participants (2)
-
Kent Mcleod -
Richard Clark