So far, I've not been able to turn up any benchmarks on linux kernels compiled for different cpus. There's stuff on kernel.org showing that years ago someone had plans for documenting such benchmarks, but that's the best that I've turned up so far.
That leaves me with only conjecture and superstition (mine is that these speed differences aren't measurable for normal applications -- otherwise someone would have documented them). However, conjecture and superstition aren't a suitable basis for a technical committee decision. Does *anyone* have any relevant, solid data that they can point us at? If there's no hard data -- neither positive nor negative -- I think we should adopt a wait&see attitude, expecting that [any day now] such benchmark results will turn up, or that we'll soon have the resources to conduct such benchmarks ourselves. -- Raul

