diff -r 58ef1439ca98 xen/arch/x86/domain.c
--- a/xen/arch/x86/domain.c	Tue Sep 15 10:08:12 2009 +0100
+++ b/xen/arch/x86/domain.c	Mon Sep 21 18:52:26 2009 +0100
@@ -1324,6 +1324,13 @@
         p->arch.ctxt_switch_from(p);
     }
 
+    if ( p->domain != n->domain )
+        cpu_set(cpu, n->domain->domain_dirty_cpumask);
+    cpu_set(cpu, n->vcpu_dirty_cpumask);
+
+    /* Run arch.ctxt_switch_to() afrter domain_dirty_cpumask
+     * to make sure arch-dependent things (like ept flushing)
+     * happens at-least-once without locks */
     if ( !is_idle_vcpu(n) )
     {
         memcpy(stack_regs,
@@ -1332,10 +1339,6 @@
         n->arch.ctxt_switch_to(n);
     }
 
-    if ( p->domain != n->domain )
-        cpu_set(cpu, n->domain->domain_dirty_cpumask);
-    cpu_set(cpu, n->vcpu_dirty_cpumask);
-
     gdt = !is_pv_32on64_vcpu(n) ? per_cpu(gdt_table, cpu) :
                                   per_cpu(compat_gdt_table, cpu);
     if ( need_full_gdt(n) )
diff -r 58ef1439ca98 xen/arch/x86/hvm/vmx/vmx.c
--- a/xen/arch/x86/hvm/vmx/vmx.c	Tue Sep 15 10:08:12 2009 +0100
+++ b/xen/arch/x86/hvm/vmx/vmx.c	Mon Sep 21 18:52:26 2009 +0100
@@ -666,10 +666,17 @@
 
 static void vmx_ctxt_switch_to(struct vcpu *v)
 {
+    struct domain *d = v->domain;
+
     /* HOST_CR4 in VMCS is always mmu_cr4_features. Sync CR4 now. */
     if ( unlikely(read_cr4() != mmu_cr4_features) )
         write_cr4(mmu_cr4_features);
 
+    if ( d->arch.hvm_domain.hap_enabled
+         && cpu_test_and_clear(smp_processor_id(),
+                               d->arch.hvm_domain.vmx.ept_needs_flush)) 
+        __invept(1, d->arch.hvm_domain.vmx.ept_control.eptp, 0);
+
     vmx_restore_guest_msrs(v);
     vmx_restore_dr(v);
     vpmu_load(v);
@@ -1219,7 +1226,11 @@
     if ( d->arch.hvm_domain.hap_enabled && d->vcpu && d->vcpu[0] )
     {
         ASSERT(local_irq_is_enabled());
-        on_each_cpu(__ept_sync_domain, d, 1);
+        /* Mark cpus that may need flushing on next schedule */
+        cpus_complement(d->arch.hvm_domain.vmx.ept_needs_flush,
+                        d->domain_dirty_cpumask);
+        /* And flush on actively-running processors */
+        on_selected_cpus(&d->domain_dirty_cpumask, __ept_sync_domain, d, 1);
     }
 }
 
diff -r 58ef1439ca98 xen/include/asm-x86/hvm/vmx/vmcs.h
--- a/xen/include/asm-x86/hvm/vmx/vmcs.h	Tue Sep 15 10:08:12 2009 +0100
+++ b/xen/include/asm-x86/hvm/vmx/vmcs.h	Mon Sep 21 18:52:26 2009 +0100
@@ -67,6 +67,7 @@
         };
         u64 eptp;
     } ept_control;
+    cpumask_t ept_needs_flush;
 };
 
 struct arch_vmx_struct {