On Sat, Dec 18, 2021 at 7:57 AM Richard Clark <[email protected]> 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 -- [email protected]
> To unsubscribe send an email to [email protected]
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]

Reply via email to