diff --git a/xen/common/trace.c b/xen/common/trace.c
index 9746b75102..da359b5908 100644
--- a/xen/common/trace.c
+++ b/xen/common/trace.c
@@ -260,7 +260,7 @@ void trace(u32 event, unsigned long d1, unsigned long d2,
     }
 
     rec = &t_recs[smp_processor_id()][buf->prod % nr_recs];
-    rdtscll(rec->cycles);
+    rec->cycles  = (u64)get_cycles();
     rec->event   = event;
     rec->data[0] = d1;
     rec->data[1] = d2;
diff --git a/xen/include/asm-x86/time.h b/xen/include/asm-x86/time.h
index ba5b23139a..b192f55c82 100644
--- a/xen/include/asm-x86/time.h
+++ b/xen/include/asm-x86/time.h
@@ -2,6 +2,8 @@
 #ifndef __X86_TIME_H__
 #define __X86_TIME_H__
 
+#include <asm/msr.h>
+
 extern int timer_ack;
 
 extern void calibrate_tsc_bp(void);
@@ -10,4 +12,13 @@ extern void calibrate_tsc_ap(void);
 struct domain;
 extern void init_domain_time(struct domain *d);
 
+typedef u64 cycles_t;
+
+static inline cycles_t get_cycles(void)
+{
+    cycles_t c;
+    rdtscll(c);
+    return c;
+}
+
 #endif /* __X86_TIME_H__ */