#include <linux/i8253.h>
 
-#define GET_TIME(x)    do { if (cpu_has_tsc) rdtscl(x); else x = get_time_pit(); } while (0)
+#define GET_TIME(x)    do { if (cpu_has_tsc) x = (unsigned int)native_read_tsc(); else x = get_time_pit(); } while (0)
 #define DELTA(x,y)     (cpu_has_tsc ? ((y) - (x)) : ((x) - (y) + ((x) < (y) ? PIT_TICK_RATE / HZ : 0)))
 #define TIME_NAME      (cpu_has_tsc?"TSC":"PIT")
 static unsigned int get_time_pit(void)
         return count;
 }
 #elif defined(__x86_64__)
-#define GET_TIME(x)    rdtscl(x)
+#define GET_TIME(x)    do { x = (unsigned int)native_read_tsc(); } while (0)
 #define DELTA(x,y)     ((y)-(x))
 #define TIME_NAME      "TSC"
 #elif defined(__alpha__) || defined(CONFIG_MN10300) || defined(CONFIG_ARM) || defined(CONFIG_ARM64) || defined(CONFIG_TILE)