gicv3: Use split EOI mode

[kent-mcleod]

Separate priority drop from deactivation so that when the kernel
delegates interrupts to userlevel, they can be left in the active state
until user level performs the ack invocation which deactivates them.
This is more efficient than doing a disable and enable operation
for each handled interrupt as it is core local and doesn't require
sending operations to the GIC distributor.

[kent-mcleod]

I don't plan to add this support to the other GIC versions in this PR as there would be more substantial changes involved:

• GICv2 with SGIs stores the source CPUID in the active IRQ state. This is needed for both priority drop and final deactivation. This feature was removed in the GICv3. The kernel doesn't track this additional state when delegating IRQs to user level and so wouldn't be able to correctly end an SGI interrupt without adding more book-keeping for each IRQ number.
• Some platforms that use the GICv2 code implementation don't actually support split EOI mode (I guess they don't implement gic 2.0 but are more 1.0). The imx6/sabre is an example of this.
• On platforms that do support split-eoi mode, the second register for ending the interrupt (GICC_DIR) is located at address 0x1000, but the kernel has only mapped in a single 4k frame for the device and so can't currently access it.

None of these are show-stoppers, but it'd be a fair amount of code changes and I don't think it's justified at this stage unless there was a cortex-a15 platform that really wanted the change.

[Indanz]

Other than the doRemoteDeactivatePrivateInterrupt typo and the ifdef maze, it looks good.

Would be good to test this cross-core too though, either manually or with sel4test. But sel4test doesn't have the infrastructure to trigger IRQs on demand yet.

[Indanz]

Agreed with not supporting GICv2.

As for cross-core IRQ handling, if we add a way to change the affinity of an existing IRQ handler, I'm fine with disallowing cross-core interrupt acks. That way users will notice if they accidentally configured a system horribly wrong.

[Indanz]

I'm not convinced that RISC-V's invokeIRQHandler_AckIRQ() implementation is correct in case the ack is done on a different core than where the IRQ originated. It should use your new doRemoteDeactivatePrivateInterrupt() too I think, or somehow remember the originating core and use that in plic_complete_claim() instead of plic_get_current_hart_id(). Or ACK it immediately like is done for QEMU.

[kent-mcleod]

One potential issue is with what happens if user-level keeps calling seL4_IRQHandler_Ack for the same interrupt.
Previously, unmasking the interrupt was idempotent, but deactivateInterrupt isn't. The GICv3 specification states:

When ICC_CTLR_EL1.EOImode or ICC_CTLR_EL3.EOIMode_EL3 == 1 but the interrupt is not active in the
Distributor, writes to ICC_DIR_EL1 must be ignored. If supported, an implementation might generate a system
error.

Edit: I think that "writes to ICC_DIR_EL1 must be ignored" means that the hardware has to ignore writes to ICC_DIR_EL1 without an active corresponding interrupt in the distributor. So it's just a question of whether our platforms have implementations that generate system errors in this case.

• add sel4test that multiple acks are allowed by the platform.

[Indanz]

The same document also says:

SPIs can be deactivated by a different PE.

So perhaps IpiRemoteCall_DeactivatePrivateInterrupt() isn't necessary for SPIs.

[Indanz]

If the endif is this close to the if I would drop the comment as it only makes things messy and it's clear enough without it.

[lsf37]

This kind of pattern in generic code will make it impossible for us to switch between GICv2 and GICv3 in verification without making it an entire new architecture. Can this be put behind a generic interface that both GIC versions implement?

[Indanz]

I think the problem is that the current IRQ model doesn't match reality enough and we need to extend maskInterrupt() with something like kernelAckInterrupt() and userAckInterrupt(), with remote equivalent functions.

Then all the ifdeffery is moved to arch code instead of generic code.

[lsf37]

Same here, having ARM config dependent ifdefs in generic code will make generic proofs impossible -- it's fine for those that we're not planning to ever verify, but GICv3 does sound like something we'd want pretty soon.

[lsf37]

We don't do this much in the kernel usually, but would it work to use an actual if instead of conditional compilation/preprocessor here? Then we can follow both paths in the verification and it'll work either way. IIRC, the compiler should optimise out any if (0) cases.