diff -r 9dbbf1631193 xen/arch/x86/hvm/vmx/vvmx.c
--- a/xen/arch/x86/hvm/vmx/vvmx.c	Mon Jul 25 14:21:13 2011 +0100
+++ b/xen/arch/x86/hvm/vmx/vvmx.c	Tue Jul 26 15:19:30 2011 +0100
@@ -1070,11 +1070,17 @@ int nvmx_handle_vmresume(struct cpu_user
     int launched;
     struct vcpu *v = current;
 
+    if ( vcpu_nestedhvm(v).nv_vvmcxaddr == VMCX_EADDR )
+    {
+        vmreturn (regs, VMFAIL_INVALID);
+        return X86EMUL_OKAY;        
+    }
+
     launched = __get_vvmcs(vcpu_nestedhvm(v).nv_vvmcx,
                            NVMX_LAUNCH_STATE);
     if ( !launched ) {
        vmreturn (regs, VMFAIL_VALID);
-       return X86EMUL_EXCEPTION;
+       return X86EMUL_OKAY;
     }
     return nvmx_vmresume(v,regs);
 }
@@ -1085,11 +1091,17 @@ int nvmx_handle_vmlaunch(struct cpu_user
     int rc;
     struct vcpu *v = current;
 
+    if ( vcpu_nestedhvm(v).nv_vvmcxaddr == VMCX_EADDR )
+    {
+        vmreturn (regs, VMFAIL_INVALID);
+        return X86EMUL_OKAY;        
+    }
+
     launched = __get_vvmcs(vcpu_nestedhvm(v).nv_vvmcx,
                            NVMX_LAUNCH_STATE);
     if ( launched ) {
        vmreturn (regs, VMFAIL_VALID);
-       rc = X86EMUL_EXCEPTION;
+       return X86EMUL_OKAY;
     }
     else {
         rc = nvmx_vmresume(v,regs);
@@ -1162,6 +1174,7 @@ int nvmx_handle_vmclear(struct cpu_user_
     struct vmx_inst_decoded decode;
     struct nestedvcpu *nvcpu = &vcpu_nestedhvm(v);
     unsigned long gpa = 0;
+    void *vvmcs;
     int rc;
 
     rc = decode_vmx_inst(regs, &decode, &gpa, 0);
@@ -1171,24 +1184,28 @@ int nvmx_handle_vmclear(struct cpu_user_
     if ( gpa & 0xfff )
     {
         vmreturn(regs, VMFAIL_INVALID);
-        goto out;
+        return X86EMUL_OKAY;
+    }
+    
+    if ( gpa == nvcpu->nv_vvmcxaddr ) 
+    {
+        __set_vvmcs(nvcpu->nv_vvmcx, NVMX_LAUNCH_STATE, 0);
+        nvmx_purge_vvmcs(v);
+    }
+    else 
+    {
+        /* Even if this VMCS isn't the current one, we must clear it. */
+        vvmcs = hvm_map_guest_frame_rw(gpa >> PAGE_SHIFT);
+        if ( vvmcs ) 
+            __set_vvmcs(vvmcs, NVMX_LAUNCH_STATE, 0);
+        hvm_unmap_guest_frame(vvmcs);
+
+        if ( nvcpu->nv_vvmcxaddr != VMCX_EADDR )
+            gdprintk(XENLOG_WARNING, "vmclear gpa %lx != %"PRIpaddr"\n",
+                     gpa, nvcpu->nv_vvmcxaddr);
     }
 
-    if ( gpa != nvcpu->nv_vvmcxaddr && nvcpu->nv_vvmcxaddr != VMCX_EADDR )
-    {
-        gdprintk(XENLOG_WARNING, 
-                 "vmclear gpa %lx not the same as current vmcs %"PRIpaddr"\n",
-                 gpa, nvcpu->nv_vvmcxaddr);
-        vmreturn(regs, VMSUCCEED);
-        goto out;
-    }
-    if ( nvcpu->nv_vvmcxaddr != VMCX_EADDR )
-        __set_vvmcs(nvcpu->nv_vvmcx, NVMX_LAUNCH_STATE, 0);
-    nvmx_purge_vvmcs(v);
-
     vmreturn(regs, VMSUCCEED);
-
-out:
     return X86EMUL_OKAY;
 }