vmm_scale_tsc
const uint64_t htsc_scaled = vmm_scale_tsc(base_host_tsc, mult);
return (vmm_scale_tsc(host_tsc, mult) + offset);
const uint64_t guest_ticks = vmm_scale_tsc(host_ticks,
