On the one hand, the Linux kernel task scheduler is critical to all
application performance. On the other hand, it is widely agreed that its
code complexity is spiraling out of control, and only a tiny handful of
kernel developers understand it. We are exploring the opportunities and
challenges in applying formal verification to Linux kernel task-scheduler
code. Building on a previous work focusing on the evolution of the
function {\tt should_we_balance}, we here consider a version of the key
task-placement function {\tt select_idle_core} and the evolution of the
iterators on which it relies.