diff --git a/xen/arch/x86/acpi/cpu_idle.c b/xen/arch/x86/acpi/cpu_idle.c
index 14b02789c5..654de24f40 100644
--- a/xen/arch/x86/acpi/cpu_idle.c
+++ b/xen/arch/x86/acpi/cpu_idle.c
@@ -401,15 +401,16 @@ void mwait_idle_with_hints(unsigned int eax, unsigned int ecx)
 {
     unsigned int cpu = smp_processor_id();
     s_time_t expires = per_cpu(timer_deadline, cpu);
+    const void *monitor_addr = &mwait_wakeup(cpu);
 
     if ( boot_cpu_has(X86_FEATURE_CLFLUSH_MONITOR) )
     {
         mb();
-        clflush((void *)&mwait_wakeup(cpu));
+        clflush(monitor_addr);
         mb();
     }
 
-    __monitor((void *)&mwait_wakeup(cpu), 0, 0);
+    __monitor(monitor_addr, 0, 0);
     smp_mb();
 
     /*
diff --git a/xen/include/asm-x86/system.h b/xen/include/asm-x86/system.h
index c665499e36..3246797bec 100644
--- a/xen/include/asm-x86/system.h
+++ b/xen/include/asm-x86/system.h
@@ -11,11 +11,15 @@
     __sel;                                                      \
 })
 
-#define wbinvd() \
-    asm volatile ( "wbinvd" : : : "memory" )
+static inline void wbinvd(void)
+{
+    asm volatile ( "wbinvd" ::: "memory" );
+}
 
-#define clflush(a) \
-    asm volatile ( "clflush (%0)" : : "r"(a) )
+static inline void clflush(const void *p)
+{
+    asm volatile ( "clflush %0" :: "m" (*(const char *)p) );
+}
 
 #define xchg(ptr,v) \
     ((__typeof__(*(ptr)))__xchg((unsigned long)(v),(ptr),sizeof(*(ptr))))