Modern concurrency logics are sound only with respect to the interleaving semantics, which assumes scheduling is implemented correctly. This cannot be taken for granted in preemptive OS kernels, where the correctness of the scheduler is interdependent with the correctness of the code it schedules. Come to the talk to learn about how we can do things for real! This is joint work with Hongseok Yang.