Looking some more at the kernel code (tsc.c), it appears that it would
only trust the arch frequency if the cpu 'tsc_known_freq' flag is set
(which none of the machines I have access to has, although for some
the dpdk's get_tsc_freq_arch() does return a value), otherwise it
would calibrate it (hence the "Refined" in dmesg). Perhaps we should
do the same.
/*
* When TSC frequency is known (retrieved via MSR or CPUID), we skip
* the refined calibration and directly register it as a clocksource.
*/
if (boot_cpu_has(X86_FEATURE_TSC_KNOWN_FREQ)) {
