Camkes VMM configuration
Hello. I've been playing around with the camkes Arm VMM. However, the meaning of some of the configuration fields is not completely clear to me. For example: - what is the difference between "linux_ram_base" and "linux_ram_paddr_base" in the linux_address_config attribute? Are these supposed to define the virtual and physical addresses of the guest's ram region base, respectively? If so, can we have non-identity mappings by setting them to different values? From my experiments having different addresses on those does not always work (even if both are aligned to a 2M superpage boundary) . - what is the difference between the untyped_mmios and mmios attributes? They seem to serve pretty similar purposes. For example, in different vm-examples they are both used for assigning the virtual gic cpu interface to the guest. I probably have a few other questions. I couldn't find it, but I was hoping there was more thorough documentation for the vm configuration detailing the meaning of these fields (and others)? Best regards, José
I see this topic wasn’t answered yet. Let me give more traction to it since I also have the same questions since when I started playing with CAmKES VMM. Please, help/correct me if I’m wrong. See inline. From: Jose Martins <josemartins90@gmail.com> Date: Tuesday, 2 November 2021 at 10:12 PM To: devel@sel4.systems <devel@sel4.systems> Subject: [seL4] Camkes VMM configuration Hello. I've been playing around with the camkes Arm VMM. However, the meaning of some of the configuration fields is not completely clear to me. For example: - what is the difference between "linux_ram_base" and "linux_ram_paddr_base" in the linux_address_config attribute? Are these supposed to define the virtual and physical addresses of the guest's ram region base, respectively? If so, can we have non-identity mappings by setting them to different values? From my experiments having different addresses on those does not always work (even if both are aligned to a 2M superpage boundary) . JP: Indeed, I think the idea was originally to provide a way to configure VMs with a 2nd stage mapping that is not 1:1. But I also think this is still work in progress today. Is it correct? JP: Looks like linux_ram_base would be the guest-physical baseaddr while linux_ram_paddr_base the machine-physical. - what is the difference between the untyped_mmios and mmios attributes? They seem to serve pretty similar purposes. For example, in different vm-examples they are both used for assigning the virtual gic cpu interface to the guest. JP: I think mmios is used for memory maps with dev attributes, The mmio of virtual gic cpu interface is one of the mappings where you want to have dev attributes in the 2nd stage MMU. Untyped_mmios looks like it is used only for normal memory attributes. For instance, guest ram. Is it correct? I probably have a few other questions. I couldn't find it, but I was hoping there was more thorough documentation for the vm configuration detailing the meaning of these fields (and others)? JP: I don’t know about documentation, but if the community could give us a pointer, that would be much appreciated. Best regards, José _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
participants (2)
-
Jorge Pereira -
Jose Martins