diff --git a/xen/arch/x86/domain.c b/xen/arch/x86/domain.c
index 8d30d0837c..0d7a40cc73 100644
--- a/xen/arch/x86/domain.c
+++ b/xen/arch/x86/domain.c
@@ -2093,6 +2093,9 @@ void arch_dump_domain_info(struct domain *d)
 void arch_dump_vcpu_info(struct vcpu *v)
 {
     paging_dump_vcpu_info(v);
+
+    if ( is_hvm_vcpu(v) )
+        vpmu_dump(v);
 }
 
 void domain_cpuid(
diff --git a/xen/arch/x86/hvm/vmx/vpmu_core2.c b/xen/arch/x86/hvm/vmx/vpmu_core2.c
index f14fbee76e..2313e39f62 100644
--- a/xen/arch/x86/hvm/vmx/vpmu_core2.c
+++ b/xen/arch/x86/hvm/vmx/vpmu_core2.c
@@ -133,6 +133,16 @@ static const u32 core2_fix_counters_msr[] = {
     MSR_CORE_PERF_FIXED_CTR2
 };
 
+/*
+ * MSR_CORE_PERF_FIXED_CTR_CTRL contains the configuration of all fixed
+ * counters. 4 bits for every counter.
+ */
+#define FIXED_CTR_CTRL_BITS 4
+#define FIXED_CTR_CTRL_MASK ((1 << FIXED_CTR_CTRL_BITS) - 1)
+
+/* The index into the core2_ctrls_msr[] of this MSR used in core2_vpmu_dump() */
+#define MSR_CORE_PERF_FIXED_CTR_CTRL_IDX 0
+
 /* Core 2 Non-architectual Performance Control MSRs. */
 static const u32 core2_ctrls_msr[] = {
     MSR_CORE_PERF_FIXED_CTR_CTRL,
@@ -508,7 +518,7 @@ static int core2_vpmu_do_wrmsr(unsigned int msr, uint64_t msr_content)
         {
             core2_vpmu_cxt->pmu_enable->fixed_ctr_enable[i] =
                 (global_ctrl & 1) & ((non_global_ctrl & 0x3)? 1: 0);
-            non_global_ctrl >>= 4;
+            non_global_ctrl >>= FIXED_CTR_CTRL_BITS;
             global_ctrl >>= 1;
         }
         break;
@@ -565,7 +575,7 @@ static int core2_vpmu_do_wrmsr(unsigned int msr, uint64_t msr_content)
             if  ( msr == MSR_IA32_DS_AREA )
                 break;
             /* 4 bits per counter, currently 3 fixed counters implemented. */
-            mask = ~((1ull << (3 * 4)) - 1);
+            mask = ~((1ull << (VPMU_CORE2_NUM_FIXED * FIXED_CTR_CTRL_BITS)) - 1);
             if (msr_content & mask)
                 inject_gp = 1;
             break;
@@ -645,6 +655,52 @@ static void core2_vpmu_do_cpuid(unsigned int input,
     }
 }
 
+/* Dump vpmu info on console, called in the context of keyhandler 'q'. */
+static void core2_vpmu_dump(struct vcpu *v)
+{
+    struct vpmu_struct *vpmu = vcpu_vpmu(v);
+    int i, num;
+    struct core2_vpmu_context *core2_vpmu_cxt = NULL;
+    u64 val;
+
+    if ( !vpmu_is_set(vpmu, VPMU_CONTEXT_ALLOCATED) )
+         return;
+
+    if ( !vpmu_is_set(vpmu, VPMU_RUNNING) )
+    {
+        if ( vpmu_set(vpmu, VPMU_CONTEXT_LOADED) )
+            printk("    vPMU loaded\n");
+        else
+            printk("    vPMU allocated\n");
+        return;
+    }
+
+    printk("    vPMU running\n");
+    core2_vpmu_cxt = vpmu->context;
+    num = core2_get_pmc_count();
+    /* Print the contents of the counter and its configuration msr. */
+    for ( i = 0; i < num; i++ )
+    {
+        struct arch_msr_pair* msr_pair = core2_vpmu_cxt->arch_msr_pair;
+        if ( core2_vpmu_cxt->pmu_enable->arch_pmc_enable[i] )
+            printk("      general_%d: 0x%016lx ctrl: 0x%016lx\n",
+                             i, msr_pair[i].counter, msr_pair[i].control);
+    }
+    /*
+     * The configuration of the fixed counter is 4 bits each in the
+     * MSR_CORE_PERF_FIXED_CTR_CTRL.
+     */
+    val = core2_vpmu_cxt->ctrls[MSR_CORE_PERF_FIXED_CTR_CTRL_IDX];
+    for ( i = 0; i < core2_fix_counters.num; i++ )
+    {
+        if ( core2_vpmu_cxt->pmu_enable->fixed_ctr_enable[i] )
+            printk("      fixed_%d:   0x%016lx ctrl: 0x%lx\n",
+                             i, core2_vpmu_cxt->fix_counters[i],
+                             val & FIXED_CTR_CTRL_MASK);
+        val >>= FIXED_CTR_CTRL_BITS;
+    }
+}
+
 static int core2_vpmu_do_interrupt(struct cpu_user_regs *regs)
 {
     struct vcpu *v = current;
@@ -758,7 +814,8 @@ struct arch_vpmu_ops core2_vpmu_ops = {
     .do_cpuid = core2_vpmu_do_cpuid,
     .arch_vpmu_destroy = core2_vpmu_destroy,
     .arch_vpmu_save = core2_vpmu_save,
-    .arch_vpmu_load = core2_vpmu_load
+    .arch_vpmu_load = core2_vpmu_load,
+    .arch_vpmu_dump = core2_vpmu_dump
 };
 
 static void core2_no_vpmu_do_cpuid(unsigned int input,
diff --git a/xen/arch/x86/hvm/vpmu.c b/xen/arch/x86/hvm/vpmu.c
index 0b843c15e5..3b6958081e 100644
--- a/xen/arch/x86/hvm/vpmu.c
+++ b/xen/arch/x86/hvm/vpmu.c
@@ -154,3 +154,12 @@ void vpmu_destroy(struct vcpu *v)
         vpmu->arch_vpmu_ops->arch_vpmu_destroy(v);
 }
 
+/* Dump some vpmu informations on console. Used in keyhandler dump_domains(). */
+void vpmu_dump(struct vcpu *v)
+{
+    struct vpmu_struct *vpmu = vcpu_vpmu(v);
+
+    if ( vpmu->arch_vpmu_ops && vpmu->arch_vpmu_ops->arch_vpmu_dump )
+        vpmu->arch_vpmu_ops->arch_vpmu_dump(v);
+}
+
diff --git a/xen/include/asm-x86/hvm/vpmu.h b/xen/include/asm-x86/hvm/vpmu.h
index 84e4c42ee7..cd31f5eb0b 100644
--- a/xen/include/asm-x86/hvm/vpmu.h
+++ b/xen/include/asm-x86/hvm/vpmu.h
@@ -54,6 +54,7 @@ struct arch_vpmu_ops {
     void (*arch_vpmu_destroy)(struct vcpu *v);
     void (*arch_vpmu_save)(struct vcpu *v);
     void (*arch_vpmu_load)(struct vcpu *v);
+    void (*arch_vpmu_dump)(struct vcpu *v);
 };
 
 int vmx_vpmu_initialise(struct vcpu *, unsigned int flags);
@@ -87,6 +88,7 @@ void vpmu_initialise(struct vcpu *v);
 void vpmu_destroy(struct vcpu *v);
 void vpmu_save(struct vcpu *v);
 void vpmu_load(struct vcpu *v);
+void vpmu_dump(struct vcpu *v);
 
 extern int acquire_pmu_ownership(int pmu_ownership);
 extern void release_pmu_ownership(int pmu_ownership);