diff --git a/xen/arch/x86/hvm/svm/vmcb.c b/xen/arch/x86/hvm/svm/vmcb.c
index 4e1f61dbe0..839d3ff91b 100644
--- a/xen/arch/x86/hvm/svm/vmcb.c
+++ b/xen/arch/x86/hvm/svm/vmcb.c
@@ -12,6 +12,8 @@
 #include <xen/mm.h>
 #include <xen/rcupdate.h>
 #include <xen/sched.h>
+#include <xen/softirq.h>
+
 #include <asm/hvm/svm/vmcb.h>
 #include <asm/msr-index.h>
 #include <asm/p2m.h>
@@ -246,6 +248,8 @@ static void cf_check vmcb_dump(unsigned char ch)
             }
             printk("\tVCPU %d\n", v->vcpu_id);
             svm_vmcb_dump("key_handler", v->arch.hvm.svm.vmcb);
+
+            process_pending_softirqs();
         }
     }
 
diff --git a/xen/arch/x86/hvm/vmx/vmcs.c b/xen/arch/x86/hvm/vmx/vmcs.c
index c86f73f6d1..e7fca4bf33 100644
--- a/xen/arch/x86/hvm/vmx/vmcs.c
+++ b/xen/arch/x86/hvm/vmx/vmcs.c
@@ -2165,7 +2165,7 @@ static void cf_check vmcs_dump(unsigned char ch)
 {
     struct domain *d;
     struct vcpu *v;
-    
+
     printk("*********** VMCS Areas **************\n");
 
     rcu_read_lock(&domlist_read_lock);
@@ -2184,6 +2184,8 @@ static void cf_check vmcs_dump(unsigned char ch)
             }
             printk("\tVCPU %d\n", v->vcpu_id);
             vmcs_dump_vcpu(v);
+
+            process_pending_softirqs();
         }
     }