Indan Zupancic

> No, it's different here because currently seL4 bounds interrupt inter-arrival time by how often the receiving thread can acknowledge it. Yes, the worst case is much worse, but higher...

> This is less worse than in the unicore case, where all threads would be blocked from making any progress, but it is still not ideal. On unicore only threads...

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. I also think the old...

> Again, GICv3 can support up to 16 LRs while GICv2 can support up to 64 LRs. Thats why 64-bit wide register to be generic. What is the actual hardware...

> > 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...

Although many device regions are chunks of 64k, only very few actually need more than the first 4k. That said, 64k pages are good to have for other reasons. Anything...

The problem I have with this solution is that conceptually it doesn't make sense: `ksCurThread` should always be running on the current core. This fix relies on `SCHED_ENQUEUE_CURRENT_TCB`/`SCHED_APPEND_CURRENT_TCB` being called...

> I agree that it is weird conceptually that a thread on a remote core is enqueued on the remote core during a call to schedule() on the current core,...

`ackInterrupt()` is called with the irq retrieved by `getActiveIRQ()`, which basically returns `active_irq`. I don't see `active_irq` being overwritten anywhere though.

>> Separation of Priority-drop from Deactivation (Feature supported by GICv2/3/4). > > Yes, I've been trying to find time to set up some benchmarks to measure the impact of this...