I have questions about the vgic maintenance for sel4 tk1 ARM VMM.  When the VM acknowledges an IRQ, an exception is raised and is delivered to the VMM. Could someone explain how seL4 intercepts the VM ack? How is this exception is raised ? I am confused because the VM is supposed to totally control the MMIO of the device and can write any thing to the device. How can seL4 be triggered in this case? Which part of  source code allows seL4 to intercept the VM ack?

Thanks

Peng