diff --git a/xen/arch/arm/gic-v3.c b/xen/arch/arm/gic-v3.c
index c98a163ee7..2952335d05 100644
--- a/xen/arch/arm/gic-v3.c
+++ b/xen/arch/arm/gic-v3.c
@@ -1265,7 +1265,8 @@ static int gicv3_make_hwdom_dt_node(const struct domain *d,
     if ( res )
         return res;
 
-    res = fdt_property_cell(fdt, "#redistributor-regions", gicv3.rdist_count);
+    res = fdt_property_cell(fdt, "#redistributor-regions",
+                            d->arch.vgic.nr_regions);
     if ( res )
         return res;
 
@@ -1274,8 +1275,10 @@ static int gicv3_make_hwdom_dt_node(const struct domain *d,
      * GIC has two memory regions: Distributor + rdist regions
      * CPU interface and virtual cpu interfaces accessesed as System registers
      * So cells are created only for Distributor and rdist regions
+     * The hardware domain may not use all the regions. So only copy
+     * what is necessary.
      */
-    new_len = new_len * (gicv3.rdist_count + 1);
+    new_len = new_len * (d->arch.vgic.nr_regions + 1);
 
     hw_reg = dt_get_property(gic, "reg", &len);
     if ( !hw_reg )
@@ -1503,7 +1506,11 @@ static int gicv3_make_hwdom_madt(const struct domain *d, u32 offset)
 
     /* Add Generic Redistributor */
     size = sizeof(struct acpi_madt_generic_redistributor);
-    for ( i = 0; i < gicv3.rdist_count; i++ )
+    /*
+     * The hardware domain may not used all the regions. So only copy
+     * what is necessary.
+     */
+    for ( i = 0; i < d->arch.vgic.nr_regions; i++ )
     {
         gicr = (struct acpi_madt_generic_redistributor *)(base_ptr + table_len);
         gicr->header.type = ACPI_MADT_TYPE_GENERIC_REDISTRIBUTOR;
diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index df1bab3a35..efe824c6fb 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -1640,7 +1640,11 @@ static int vgic_v3_vcpu_init(struct vcpu *v)
     return 0;
 }
 
-static inline unsigned int vgic_v3_rdist_count(struct domain *d)
+/*
+ * Return the maximum number possible of re-distributor regions for
+ * a given domain.
+ */
+static inline unsigned int vgic_v3_max_rdist_count(struct domain *d)
 {
     /*
      * Normally there is only one GICv3 redistributor region.
@@ -1662,7 +1666,7 @@ static int vgic_v3_real_domain_init(struct domain *d)
     int rdist_count, i, ret;
 
     /* Allocate memory for Re-distributor regions */
-    rdist_count = vgic_v3_rdist_count(d);
+    rdist_count = vgic_v3_max_rdist_count(d);
 
     rdist_regions = xzalloc_array(struct vgic_rdist_region, rdist_count);
     if ( !rdist_regions )
@@ -1695,8 +1699,19 @@ static int vgic_v3_real_domain_init(struct domain *d)
             d->arch.vgic.rdist_regions[i].first_cpu = first_cpu;
 
             first_cpu += size / GICV3_GICR_SIZE;
+
+            if ( first_cpu >= d->max_vcpus )
+                break;
         }
 
+        /*
+         * The hardware domain may not use all the re-distributors
+         * regions (e.g when the number of vCPUs does not match the
+         * number of pCPUs). Update the number of regions to avoid
+         * exposing unused region as they will not get emulated.
+         */
+        d->arch.vgic.nr_regions = i + 1;
+
         d->arch.vgic.intid_bits = vgic_v3_hw.intid_bits;
     }
     else
@@ -1825,7 +1840,7 @@ int vgic_v3_init(struct domain *d, int *mmio_count)
     }
 
     /* GICD region + number of Redistributors */
-    *mmio_count = vgic_v3_rdist_count(d) + 1;
+    *mmio_count = vgic_v3_max_rdist_count(d) + 1;
 
     /* one region per ITS */
     *mmio_count += vgic_v3_its_count(d);