Hi Dan, Roughly, GIC-v2 has per-core CPU interfaces and a shared distributor (GICD). The GIC-v2 virtualisation extension provides hardware support for the per-core CPU interface, but the shared GICD needs to be emulated for a virtual machine. The hypervisor still has control over the physical GICD so that it can control physical interrupts. Guest accesses to the emulated GICD are trapped so that the hypervisor can determine if a virtual interrupt is enabled or disabled by inspecting the state of the emulated GICD. For instance, if a physical interrupt is active and the VM enables the corresponding virtual interrupt, the hypervisor will inject the virtual interrupt to the VM through the virtual CPU interface control registers. If the guest accesses were redirected to the physical GICD, the guest would have control over physical interrupts. Regards, Yanyan On 10/5/19, 5:35 am, "Devel on behalf of dan pittman" wrote: 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