diff -r 3e1b6559f67d xen/arch/x86/genapic/x2apic.c
--- a/xen/arch/x86/genapic/x2apic.c	Fri Jun 11 13:58:40 2010 +0100
+++ b/xen/arch/x86/genapic/x2apic.c	Fri Jun 11 15:13:26 2010 +0200
@@ -90,6 +90,7 @@ void send_IPI_mask_x2apic_phys(const cpu
 {
     unsigned int cpu, cfg;
     unsigned long flags;
+    uint64_t msr_content;
 
     /*
      * Ensure that any synchronisation data written in program order by this
@@ -107,8 +108,10 @@ void send_IPI_mask_x2apic_phys(const cpu
 
     cfg = APIC_DM_FIXED | 0 /* no shorthand */ | APIC_DEST_PHYSICAL | vector;
     for_each_cpu_mask ( cpu, *cpumask )
-        if ( cpu != smp_processor_id() )
-            apic_wrmsr(APIC_ICR, cfg, cpu_physical_id(cpu));
+        if ( cpu != smp_processor_id() ) {
+            msr_content = cfg | ((uint64_t)cpu_physical_id(cpu) << 32);
+            apic_wrmsr(APIC_ICR, msr_content);
+        }
 
     local_irq_restore(flags);
 }
@@ -117,6 +120,7 @@ void send_IPI_mask_x2apic_cluster(const 
 {
     unsigned int cpu, cfg;
     unsigned long flags;
+    uint64_t msr_content;
 
     mb(); /* see the comment in send_IPI_mask_x2apic_phys() */
 
@@ -124,8 +128,10 @@ void send_IPI_mask_x2apic_cluster(const 
 
     cfg = APIC_DM_FIXED | 0 /* no shorthand */ | APIC_DEST_LOGICAL | vector;
     for_each_cpu_mask ( cpu, *cpumask )
-        if ( cpu != smp_processor_id() )
-            apic_wrmsr(APIC_ICR, cfg, cpu_2_logical_apicid[cpu]);
+        if ( cpu != smp_processor_id() ) {
+            msr_content = cfg | ((uint64_t)cpu_2_logical_apicid[cpu] << 32);
+            apic_wrmsr(APIC_ICR, msr_content);
+        }
 
     local_irq_restore(flags);
 }
diff -r 3e1b6559f67d xen/include/asm-x86/apic.h
--- a/xen/include/asm-x86/apic.h	Fri Jun 11 13:58:40 2010 +0100
+++ b/xen/include/asm-x86/apic.h	Fri Jun 11 15:13:26 2010 +0200
@@ -4,7 +4,7 @@
 #include <xen/config.h>
 #include <asm/apicdef.h>
 #include <asm/fixmap.h>
-#include <asm/system.h>
+#include <asm/msr.h>
 
 #define Dprintk(x...)
 
@@ -76,34 +76,31 @@ static __inline u32 apic_mem_read(unsign
  * access the 64-bit ICR register.
  */
 
-static __inline void apic_wrmsr(unsigned long reg, u32 low, u32 high)
+static __inline void apic_wrmsr(unsigned long reg, uint64_t msr_content)
 {
     if (reg == APIC_DFR || reg == APIC_ID || reg == APIC_LDR ||
         reg == APIC_LVR)
         return;
 
-    __asm__ __volatile__("wrmsr"
-            : /* no outputs */
-            : "c" (APIC_MSR_BASE + (reg >> 4)), "a" (low), "d" (high));
+    wrmsrl(APIC_MSR_BASE + (reg >> 4), msr_content);
 }
 
-static __inline void apic_rdmsr(unsigned long reg, u32 *low, u32 *high)
+static __inline uint64_t apic_rdmsr(unsigned long reg)
 {
+    uint64_t msr_content;
+
     if (reg == APIC_DFR)
-    {
-        *low = *high = -1u;
-        return;
-    }
-    __asm__ __volatile__("rdmsr"
-            : "=a" (*low), "=d" (*high)
-            : "c" (APIC_MSR_BASE + (reg >> 4)));
+        return -1u;
+
+    rdmsrl(APIC_MSR_BASE + (reg >> 4), msr_content);
+    return msr_content;
 }
 
 static __inline void apic_write(unsigned long reg, u32 v)
 {
 
     if ( x2apic_enabled )
-        apic_wrmsr(reg, v, 0);
+        apic_wrmsr(reg, v);
     else
         apic_mem_write(reg, v);
 }
@@ -111,20 +108,17 @@ static __inline void apic_write(unsigned
 static __inline void apic_write_atomic(unsigned long reg, u32 v)
 {
     if ( x2apic_enabled )
-        apic_wrmsr(reg, v, 0);
+        apic_wrmsr(reg, v);
     else
         apic_mem_write_atomic(reg, v);
 }
 
 static __inline u32 apic_read(unsigned long reg)
 {
-    u32 lo, hi;
-
     if ( x2apic_enabled )
-        apic_rdmsr(reg, &lo, &hi);
+        return apic_rdmsr(reg);
     else
-        lo = apic_mem_read(reg);
-    return lo;
+        return apic_mem_read(reg);
 }
 
 static __inline u64 apic_icr_read(void)
@@ -132,7 +126,7 @@ static __inline u64 apic_icr_read(void)
     u32 lo, hi;
 
     if ( x2apic_enabled )
-        apic_rdmsr(APIC_ICR, &lo, &hi);
+        return apic_rdmsr(APIC_ICR);
     else
     {
         lo = apic_mem_read(APIC_ICR);
@@ -145,7 +139,7 @@ static __inline u64 apic_icr_read(void)
 static __inline void apic_icr_write(u32 low, u32 dest)
 {
     if ( x2apic_enabled )
-        apic_wrmsr(APIC_ICR, low, dest);
+        apic_wrmsr(APIC_ICR, low | ((uint64_t)dest << 32));
     else
     {
         apic_mem_write(APIC_ICR2, dest << 24);
diff -r 3e1b6559f67d xen/include/asm-x86/msr.h
--- a/xen/include/asm-x86/msr.h	Fri Jun 11 13:58:40 2010 +0100
+++ b/xen/include/asm-x86/msr.h	Fri Jun 11 15:13:26 2010 +0200
@@ -5,7 +5,6 @@
 
 #ifndef __ASSEMBLY__
 
-#include <xen/smp.h>
 #include <xen/types.h>
 #include <xen/percpu.h>
 #include <xen/errno.h>
@@ -104,29 +103,22 @@ static inline int wrmsr_safe(unsigned in
 
 DECLARE_PER_CPU(u64, efer);
 
-static inline u64 read_efer(void)
-{
-    return this_cpu(efer);
-}
+#define read_efer() this_cpu(efer)
 
-static inline void write_efer(u64 val)
-{
-    this_cpu(efer) = val;
-    wrmsrl(MSR_EFER, val);
-}
+#define write_efer(val) do { \
+    this_cpu(efer) = val; \
+    wrmsrl(MSR_EFER, val); \
+} while(0)
 
 DECLARE_PER_CPU(u32, ler_msr);
 
-static inline void ler_enable(void)
-{
-    u64 debugctl;
-    
-    if ( !this_cpu(ler_msr) )
-        return;
-
-    rdmsrl(MSR_IA32_DEBUGCTLMSR, debugctl);
-    wrmsrl(MSR_IA32_DEBUGCTLMSR, debugctl | 1);
-}
+#define ler_enable() do { \
+    u64 debugctl; \
+    if ( !this_cpu(ler_msr) ) \
+        return; \
+    rdmsrl(MSR_IA32_DEBUGCTLMSR, debugctl); \
+    wrmsrl(MSR_IA32_DEBUGCTLMSR, debugctl | 1); \
+} while(0)
 
 #endif /* !__ASSEMBLY__ */
 
diff -r 3e1b6559f67d xen/include/xen/cpuidle.h
--- a/xen/include/xen/cpuidle.h	Fri Jun 11 13:58:40 2010 +0100
+++ b/xen/include/xen/cpuidle.h	Fri Jun 11 15:13:26 2010 +0200
@@ -27,6 +27,8 @@
 #ifndef _XEN_CPUIDLE_H
 #define _XEN_CPUIDLE_H
 
+#include <xen/smp.h>
+
 #define ACPI_PROCESSOR_MAX_POWER        8
 #define CPUIDLE_NAME_LEN                16