seL4_projects_libs
seL4_projects_libs copied to clipboard
libsel4vm, vgic: generate dist and cpu values
This commit adds an "fdt_ori" and "gic_node" parameter to the vm struct, which allows the library to find the GIC_DIST and GIC_CPU register addresses required for emulating the vgic.
This isn't perfect, and requires a change in camkes-vm to set the path and pointers. It could also use a check to handle address-cells and size-cells properly. I just wanted to put it out for review and discussion, and to show its possible to grab the values from the device tree. I'm open to other and better ways to do this.
Test with: https://github.com/seL4/camkes-vm/pull/52
This commit adds an "fdt_ori" and "gic_node" parameter to the vm struct,
This isn't an insignificant design change to the vm_t struct. If this is something that we should add, then it probably needs to be properly integrated into the rest of the library with proper initialization functions. If it's just an initial way to prototype associating a device tree with a guest for virtual devices to more easily find configuration information it should probably still have a proper way of installing it. (This would also allow the camkes-vm layer to more explicitly generate the fdt and then install it into the guest for the rest of the guest devices to use). Also, how is this expected to work with guests that don't use an FDT but want to use virtual devices that do use an fdt?
One more comment, if this isn't something that we want to tackle now, then maybe a smaller-impact change would be choosing to have device specific interfaces for vm_install_vgic() that could take the configuration arguments needed, allowing the caller (camkes-vm) to do the device tree parsing and pass in the address ranges via the newer vm_install_vgic() interface.
Thanks for the comments, Kent. This was something that I just put together based on the comments on using the GIC path to find the phandle. Basically, its more of a proof of concept. If you want to separate this commit out into a draft, so we can figure out the best way to do this properly while merging in the gic phandle, I'm okay with that approach.
Also, how is this expected to work with guests that don't use an FDT but want to use virtual devices that do use an fdt?
Doesn't the kernel pass an FDT to each VMM regardless of whether the guest needs to use the FDT? So I guess there's a disconnect between the guest's device tree, and the FDT used to describe the hardware resources of the system.
Would it be possible to just use the ps_io_ops interface to get the FDT? Then search for the node with the arm,gic-400 string?
Doesn't the kernel pass an FDT to each VMM regardless of whether the guest needs to use the FDT? So I guess there's a disconnect between the guest's device tree, and the FDT used to describe the hardware resources of the system.
In CAmkES, the DTB is given to the component if it has the dtb property set in its configuration, so it's not always expected to be present. It would be reasonable for a VM component to load a file from the fileserver component and not need the system DTB given to the component at all.
I think one question that needs to be decided is whether device trees are a concept that libsel4vm should know about and have a mechanism for managing a device tree and installing it into the guest. It seems to me that this is better suited for libsel4vmmplatsupport?
Thanks for the comments, Kent. This was something that I just put together based on the comments on using the GIC path to find the phandle
Yea, I'm not trying to say you shouldn't have proposed the changes, just pointing out that adding a way for vm devices to query a device tree associated with the guest is something that would be quite useful to many more devices than just the vgic, so we should consider the wider implications. EG, should this device tree be the system device tree, or the one that the guest sees? Are devices allowed to mutate it? If it's using a libfdt compatible object, then we could allow devices to install nodes in during their own initialization and have an explicit finalization step which is what Qemu does.
I'm going to mark this as a draft, since like Kent mentioned, in order to do this, you need access to the FDT in the libraries, which is a bigger design choice than just this PR. I think this would still be useful as a reference for getting the GIC information out of the device tree once the FDT is available.