IRQ Model Refactoring / Fidelity

[midnightveil]

https://github.com/seL4/seL4/pull/1183#discussion_r1479773059

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. — @Indanz

^ That is the long and short of this. We have both ARM-GICv3 and RISC-V which doesn't match the "mask" and "ack" model that the generic code assumes.

Also like to mention that at one point we had Arch_finaliseInterrupt. (https://github.com/seL4/l4v/pull/370).

Some follow up tasks from https://github.com/seL4/seL4/issues/1399#issuecomment-2669926970_ that could be done or would be invalidated by these changes.

• [ ] when writing to icenablern, why we don't use wait_for_rwp. The only reason why this code even exists (outside of boot) is probably because we still use maskInterrupt in a bunch of places on arm w/gicv3 (in 'exceptional' cases)
• [ ] some form of spurious IRQ tracking in the benchmark utilisation config?

[Indanz]

Once we fix VPPI virtual timer interrupt not to use maskInterrupt, it's safe to resurrect and merge #1399. The only reason not to merge it before was because of the performance impact, which is irrelevant once it's not used for generic IRQ handling any more.

Spurious IRQ tracking would be good, but you need a proper workload that generates a lot of interrupts, both peripheral ones as VCPU ones. Neither sel4test nor sel4bench do that. Such tracking strikes me more like a debug feature than a benchmark feature though and is tricky to get right. The easy case is handled by the printf we already have, but the tricky case of double interrupts is much harder to detect reliably.