The seL4 microkernel, written in C, has formal proofs of the maximum clock cycles for all of its syscalls. That's one way they manage to not need in-kernel preemption.