First impression: There is something funny going on with imx8mq and the speedup isn't big enough to justify a fast path. I would try optimising the normal IRQ path first.

Have you tested with SMP too?

I agree that something is wrong with the slowpath for the imx8mq - most of the speedup in that case is from using the fastpath version of switchToThread.

I have done some SMP testing. seL4Test passes with the SMP tests enabled.

Do we know how much slower the slow path becomes with this patch? The additional checks are probably not much, but it would be nice to quantify.

If there is a chance to improve the slow path speed to get to similar results, that would be great of course. @danshea00 can you comment on which bits in here you think brought the highest payoff in performance improvement?

Most of the speedup is from the simplified scheduling logic. Here is a rough breakdown of where time is going on the imx8mm (update timestamp also includes budget checking/charging):

I just measured the worst case slowpath overhead (from the start of the fastpath to after the final slowpath_irq) to be 120 (8) cycles on the imx8mm. I can add numbers for other boards if that would be useful.

Nice graph, how did you collect those numbers?

In your new test, the while loop in high_prio_fn should be a while (i < N_RUNS), otherwise there is no bound on how far into results[] will be written. I also don't see how high_prio_fn is stopped currently, other than crashing. On non-MCS, I'm not sure how you can distinguish between kernel timer ticks and user space IRQs.

I used tracepoints to record each section of the slowpath and fastpath. I just ran this with the two benchmarks, so each 'split' is the mean of 110 runs.

Thanks for the feedback on the new benchmark. At the moment the test ends with high_prio_fn waiting on the notification when low_prio_fn exits it's loop and sends on the done_ep. I'll clean things up if I end up making a PR to seL4Bench.