use_scaling      1799 arch/x86/kvm/x86.c 	int use_scaling = 0;
use_scaling      1824 arch/x86/kvm/x86.c 		use_scaling = 1;
use_scaling      1826 arch/x86/kvm/x86.c 	return set_tsc_khz(vcpu, user_tsc_khz, use_scaling);