Hi there.
The scheduler base frequency chosen on ARM kernels, and here the RPI kernel in particular, is 100Hz.
That means we're facing a 10ms scheduling interval.
Such a low setting is ususally recommended for server usage. (My experience: Higher settings won't cause issues on servers either.)
The 100Hz has also been the default and even hardcoded ARM kernel setting for quite some time in the past.
With the new 3.12/3.16 kernels (on the RPI) we can change this CONFIG_HZ setting.
On older and still used kernels like 3.4, kernel sources could easily patched. I did this for my own custom Cubitruck kernel.
Choosing 250 or 300Hz instead of 100Hz will speed up the scheduling interval.
I'd guess most applications on these low-muscle ARM devices will benefit.
Things will get more responsive since latencies get lowered.
What do you guys think about introducing such an easy to accomplish change to the default kernel configurations???
Cheers