Gerwin Klein

> By my interpretation of the RFC conditions, this shouldn't require an RFC. Extended bootinfo types is intended for extensions like this as the `seL4_BootInfoID` enum is intended to be...

Happy to leave the details to the people who know them, but as high-level input: Optimising only for the non-FPU case so that non-FPU micro benchmarks look good does not...

> note: how hard would this to be verify, anyway? Funding aside, I would naively think that having a precondition of any machine code that the FPU is enabled and...

I think there are two viable options (from the verification perspective): 1. the current form of https://github.com/seL4/seL4/pull/1539 (enable when notification is bound, disable when IRQHandler disappears or when explicitly unbound)...

If there is no interrupt, how are we getting into the `checkInterrupt` function at all? `handleInvocation` should be returning `EXCEPTION_NONE` if no preemption/interrupts happened. Do we really get this for...

Hm, just reading the test log above, I can't see anything in SCHED0007 that would have a preemptable call in it. Does sel4test tear down of test CSpaces etc after...

Good point. I can see that they do happen immediately for MCS runs during the initial allocation phase, which is preemptable. So at least that does seem to be right....

Yes, it looks fine. And AFAIR we do have a test for preemption that also works with MCS. But then I am really out of leads -- the function *is*...

But that also looks harmless, unless `getCurrentTime` messes with interrupts

Actually, MCS preemption checking (`preemptionPoint()`) is exactly where the problem is. It is not messing with interrupts, but it does not fulfil the expectations of the preemptionPoint handling code: ```...