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
> [email protected]
> https://sel4.systems/lists/listinfo/devel

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to