Gerwin Klein

> If we run out of schedcontext time then we wouldn't have an interrupt? Yup you found the same issue :-)

> Surely we have already set the timer interrupt to the earliest of these conditions That's probably where I'm wrong..

Ok, but that also means that @Indanz way of just existing the kernel is actually wrong, it would miss all that `mcsPreemptionPoint` cleanup that it needs to do because it...

For the next domain, I agree that we should have a deadline IRQ set already. But are we also guaranteed that we already have set something for when the current...

Is there a litmus test we can write that would tell us if preemption works correctly time-wise when we only check for IRQ? (like in the non-MCS code) What would...

As a "quicker", more current-behaviour-preserving fix, we could return EXCEPTION_TIME instead of EXCEPTION_PREEMPTED, and call `checkInterrupt` only for actual EXCEPTION_PREEMPTED. That would at least not change the current behaviour and...

Hm, yes, this is suspiciously simple. I'll see if I can find something in the earlier commit history that suggests why we did not do this in the first place.

*Insert rant about useless commit messages here.* I can find a set of commits in C/Haskell/proofs that introduce the split into deleting/deleted from 2008, but I can't find anything as...

> With this change the new invariant could be something like: "IRQs are disabled if no corresponding IRQ handler cap exists and enabled when there is a notification registered". And...

First results of tracing where that invariant is used (still incomplete, there are over 150 occurrences in just the invariant proofs): For acknowledging an interrupt, we currently require that `interrupt_states...