diff --git a/arch/x86_64/include/intel64/irq.h b/arch/x86_64/include/intel64/irq.h
index d27019d457..90e9372a91 100644
--- a/arch/x86_64/include/intel64/irq.h
+++ b/arch/x86_64/include/intel64/irq.h
@@ -530,7 +530,7 @@ static inline void setidt(void *idt, int size)
   asm volatile ("lidt %0"::"m"(idt_ptr):"memory");
 }
 
-static inline uint64_t rdtsc(void)
+static inline uint64_t rdtscp(void)
 {
   uint32_t lo;
   uint32_t hi;
@@ -539,7 +539,7 @@ static inline uint64_t rdtsc(void)
   return (uint64_t)lo | (((uint64_t)hi) << 32);
 }
 
-static inline uint64_t _rdtsc(void)
+static inline uint64_t rdtsc(void)
 {
   uint32_t lo;
   uint32_t hi;
diff --git a/arch/x86_64/src/intel64/intel64_rtc.c b/arch/x86_64/src/intel64/intel64_rtc.c
index 1dc3ce5f34..f96dc8a566 100644
--- a/arch/x86_64/src/intel64/intel64_rtc.c
+++ b/arch/x86_64/src/intel64/intel64_rtc.c
@@ -82,7 +82,7 @@ static unsigned long rtc_last;
 
 static unsigned long rtc_read(void)
 {
-  uint64_t  tmr = rdtsc();
+  uint64_t  tmr = rdtscp();
 
   if (tmr < rtc_last)
     {
diff --git a/arch/x86_64/src/intel64/intel64_tsc_tickless.c b/arch/x86_64/src/intel64/intel64_tsc_tickless.c
index 1ca12523eb..9341770e7e 100644
--- a/arch/x86_64/src/intel64/intel64_tsc_tickless.c
+++ b/arch/x86_64/src/intel64/intel64_tsc_tickless.c
@@ -127,7 +127,7 @@ void up_alarm_expire(void);
 
 void up_timer_initialize(void)
 {
-  g_last_stop_time = g_start_tsc = rdtsc();
+  g_last_stop_time = g_start_tsc = rdtscp();
 
 #ifndef CONFIG_SCHED_TICKLESS_ALARM
   irq_attach(TMR_IRQ, (xcpt_t)up_timer_expire, NULL);
@@ -208,7 +208,7 @@ static inline void up_tmr_sync_down(void)
 
 int up_timer_gettime(struct timespec *ts)
 {
-  uint64_t diff = (rdtsc() - g_start_tsc);
+  uint64_t diff = (rdtscp() - g_start_tsc);
   up_tick2ts(diff, ts);
   return OK;
 }
@@ -256,7 +256,7 @@ int up_timer_cancel(struct timespec *ts)
     {
       if (g_timer_active)
         {
-          up_tick2ts(g_goal_time - rdtsc(), ts);
+          up_tick2ts(g_goal_time - rdtscp(), ts);
         }
       else
         {
@@ -303,7 +303,7 @@ int up_timer_start(const struct timespec *ts)
 
   up_tmr_sync_up();
 
-  ticks = up_ts2tick(ts) + rdtsc();
+  ticks = up_ts2tick(ts) + rdtscp();
 
   g_timer_active = 1;
 
diff --git a/arch/x86_64/src/intel64/intel64_tsc_timerisr.c b/arch/x86_64/src/intel64/intel64_tsc_timerisr.c
index 9fe54174ea..2413345aac 100644
--- a/arch/x86_64/src/intel64/intel64_tsc_timerisr.c
+++ b/arch/x86_64/src/intel64/intel64_tsc_timerisr.c
@@ -73,7 +73,7 @@ void apic_timer_set(unsigned long timeout_ns)
     (unsigned long long)timeout_ns * g_x86_64_timer_freq / NS_PER_SEC;
 
 #ifdef CONFIG_ARCH_INTEL64_TSC_DEADLINE
-    write_msr(MSR_IA32_TSC_DEADLINE, rdtsc() + ticks);
+    write_msr(MSR_IA32_TSC_DEADLINE, rdtscp() + ticks);
 #else
     write_msr(MSR_X2APIC_TMICT, ticks);
 #endif