ARM Example: best use of VGIC in virtual machines.

Could you please route me to an ARM code example on the usage of VGIC in the context of virtualized system? The examples provided in DS-5 illustrate the usage of GIC  in a physical (not virtualized environment).

I have taken a rapid look at Xen and KVM VGIC code but not sure whether the implementation does not provide strict isolation of VMs. For instance, information about a particular VM interrupts can still be leaked to another VM ...