I noticed that my sched_clock() was slow on a number of machine, so I
started looking at cpufreq.

The below seems to fix the problem for me.
Signed-off-by: NIngo Molnar <mingo@elte.hu>