Camkes VMM configuration questions

seL4 kernel
1

Hi, I’ve sent these questions to devel@sel4.systems, but since I haven’t got any answers there, I’ll try here:

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é

1 Like