:: commit aad4f66fec0af2d3521d5503eb6716ffc6a89e78

diff --git a/common/sys/cpu.h b/common/sys/cpu.h
index 1d445b83..41c7576b 100644
--- a/common/sys/cpu.h
+++ b/common/sys/cpu.h
@@ -407,7 +407,11 @@ void calibrate_tsc(void);
 
 static inline uint64_t rdtsc_usec(void) {
     uint64_t exec_ticks = rdtsc();
-    return tsc_freq != 0 ? 1000000ULL * exec_ticks / tsc_freq : 0;
+    if (tsc_freq == 0) {
+        return 0;
+    }
+    return exec_ticks / tsc_freq * 1000000
+         + exec_ticks % tsc_freq * 1000000 / tsc_freq;
 }
 
 static inline void stall(uint64_t us) {