Hi all!
I'm currently trying to understand something about the use of the virtualization extensions available in the PL-400 interrupt controller in seL4. It all starts with this sentence:
The hypervisor supports virtualization also by using address
translation tables to trap accesses that the virtual machines make to the virtual distributor. The hypervisor determines the effect of these accesses and might typically update the virtual interface control registers as a result.
Source: http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0471b/CHDIHID...
My interpretation of this is that by using the IPA which is available with arm hyp, the hardware can trap accesses to the GIC from the guest and "redirect" those accesses to the physical GIC. From this, I draw the conclusion that the need for a completely virtualized GIC when using these extensions is not necessary. However, in seL4—due to the way in which it manages interrupts by handling the hardware interactions itself and instead invoking an endpoint—the use of these extensions in this way is not possible.
I'm curious if this understanding is correct, and if not, I welcome any clarity y'all can provide!
cheers, dan