diff -r 5094980f9e16 xen/arch/x86/hvm/vmx/vmx.c
--- a/xen/arch/x86/hvm/vmx/vmx.c	Tue Sep 22 09:18:25 2009 +0100
+++ b/xen/arch/x86/hvm/vmx/vmx.c	Tue Sep 22 12:32:48 2009 +0100
@@ -1233,6 +1233,7 @@
         return;
 
     ASSERT(local_irq_is_enabled());
+    ASSERT(p2m_locked_by_me(d->arch.p2m));
 
     /*
      * Flush active cpus synchronously. Flush others the next time this domain