Hi Peng, ARM provides hardware support for virtual interrupts. When the VM writes to the acknowledge register of the virtual interrupt controller, an IRQ exception is triggered and delivered to PL2 (hypervisor mode). - Alex Kroh On Sun, 2017-01-08 at 17:22 -0500, PX wrote:

Hi, all 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

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel