Jorge Pereira

> I think the fault size increase is unnecessary. `ICH_EISR_EL2` is only defined for 16 bits currently, while there are 60 bits available in the structure. 16 bits are good...

> Thanks for this change @JorgeMVP! If I understand correctly, this is processing and forwarding all updated LRs on each VGIC maintenance interrupt instead of one-at-a-time. Are you able to...

> What is the actual hardware number of LRs supported by GICv2 hardware currently supported by seL4? I'm pretty sure it's no where near 64. This is implementation defined. As...

> * vgic maintenance interrupts are PPIs, > I'm not sure I follow this use case, as it seems to me that this wouldn't trigger more than one LR updated...

Please, lets focus in the technical side, we avoid wasting our time. I'm okay if the feature is not accepted, we all know there are tradeoffs, especially with verification which...

> > Partially agreed :), if the guest uses EOIMode set to 1, then the instruction that deactivates the vIRQ can be executed by any vCPU/pCPU, which is ICV_DIR_EL1. >...

> I'm now also unclear as to how a host is supposed to handle a guest that is using SplitEOI mode and has more active IRQs than there are available...

> masks away the CPUID bits ``` static inline irq_t getActiveIRQ(void) { irq_t irq; if (!IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) { active_irq[CURRENT_CPU_INDEX()] = gic_cpuiface->int_ack; } if (IS_IRQ_VALID(active_irq[CURRENT_CPU_INDEX()])) { irq = CORE_IRQ_TO_IRQT(CURRENT_CPU_INDEX(), active_irq[CURRENT_CPU_INDEX()] & IRQ_MASK);...

> > This one is masked but fortunately seems not to be used on ackInterrupt. > > And if we were to migrate this to use split-eoi, priority drop is...

> Wow, you must be psychic because I'd been thinking about making this issue earlier today also. > > > Separation of Priority-drop from Deactivation (Feature supported by GICv2/3/4). >...