diff --git a/xen/arch/arm/gic-v3.c b/xen/arch/arm/gic-v3.c
index 7b33ff7..fdfda0b 100644
--- a/xen/arch/arm/gic-v3.c
+++ b/xen/arch/arm/gic-v3.c
@@ -909,10 +909,10 @@ static int gicv_v3_init(struct domain *d)
 
         for ( i = 0; i < gicv3.rdist_count; i++ )
         {
-            d->arch.vgic.rbase[i] = gicv3.rdist_regions[i].base;
-            d->arch.vgic.rbase_size[i] = gicv3.rdist_regions[i].size;
+            d->arch.vgic.rdist_regions[i].base = gicv3.rdist_regions[i].base;
+            d->arch.vgic.rdist_regions[i].size = gicv3.rdist_regions[i].size;
         }
-        d->arch.vgic.rdist_count = gicv3.rdist_count;
+        d->arch.vgic.nr_regions = gicv3.rdist_count;
     }
     else
     {
@@ -922,13 +922,13 @@ static int gicv_v3_init(struct domain *d)
         /* XXX: Only one Re-distributor region mapped for the guest */
         BUILD_BUG_ON(GUEST_GICV3_RDIST_REGIONS != 1);
 
-        d->arch.vgic.rdist_count = GUEST_GICV3_RDIST_REGIONS;
+        d->arch.vgic.nr_regions = GUEST_GICV3_RDIST_REGIONS;
         d->arch.vgic.rdist_stride = GUEST_GICV3_RDIST_STRIDE;
 
         /* The first redistributor should contain enough space for all CPUs */
         BUILD_BUG_ON((GUEST_GICV3_GICR0_SIZE / GUEST_GICV3_RDIST_STRIDE) < MAX_VIRT_CPUS);
-        d->arch.vgic.rbase[0] = GUEST_GICV3_GICR0_BASE;
-        d->arch.vgic.rbase_size[0] = GUEST_GICV3_GICR0_SIZE;
+        d->arch.vgic.rdist_regions[0].base = GUEST_GICV3_GICR0_BASE;
+        d->arch.vgic.rdist_regions[0].size = GUEST_GICV3_GICR0_SIZE;
     }
 
     return 0;
@@ -1107,7 +1107,7 @@ static int gicv3_make_dt_node(const struct domain *d,
      * CPU interface and virtual cpu interfaces accessesed as System registers
      * So cells are created only for Distributor and rdist regions
      */
-    len = len * (d->arch.vgic.rdist_count + 1);
+    len = len * (d->arch.vgic.nr_regions + 1);
     new_cells = xzalloc_bytes(len);
     if ( new_cells == NULL )
         return -FDT_ERR_XEN(ENOMEM);
@@ -1116,9 +1116,9 @@ static int gicv3_make_dt_node(const struct domain *d,
 
     dt_set_range(&tmp, node, d->arch.vgic.dbase, d->arch.vgic.dbase_size);
 
-    for ( i = 0; i < d->arch.vgic.rdist_count; i++ )
-        dt_set_range(&tmp, node, d->arch.vgic.rbase[i],
-                     d->arch.vgic.rbase_size[i]);
+    for ( i = 0; i < d->arch.vgic.nr_regions; i++ )
+        dt_set_range(&tmp, node, d->arch.vgic.rdist_regions[i].base,
+                     d->arch.vgic.rdist_regions[i].size);
 
     res = fdt_property(fdt, "reg", new_cells, len);
     xfree(new_cells);
diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index db6b514..13481ac 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -1112,13 +1112,14 @@ static int vgic_v3_domain_init(struct domain *d)
                           d->arch.vgic.dbase_size);
 
     /*
-     * Register mmio handler per redistributor region but not for
-     * every sgi rdist region which is per core.
-     * The redistributor region encompasses per core sgi region.
+     * Register mmio handler per contiguous region occupied by the
+     * redistributors. The handler will take care to choose which
+     * redistributor is targeted.
      */
-    for ( i = 0; i < d->arch.vgic.rdist_count; i++ )
+    for ( i = 0; i < d->arch.vgic.nr_regions; i++ )
         register_mmio_handler(d, &vgic_rdistr_mmio_handler,
-            d->arch.vgic.rbase[i], d->arch.vgic.rbase_size[i]);
+            d->arch.vgic.rdist_regions[i].base,
+            d->arch.vgic.rdist_regions[i].size);
 
     d->arch.vgic.ctlr = VGICD_CTLR_DEFAULT;
 
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index 9018c6a..3eaa7f0 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -102,10 +102,13 @@ struct arch_domain
 #ifdef CONFIG_ARM_64
         /* GIC V3 addressing */
         paddr_t dbase_size; /* Distributor base size */
-        paddr_t rbase[MAX_RDIST_COUNT];      /* Re-Distributor base address */
-        paddr_t rbase_size[MAX_RDIST_COUNT]; /* Re-Distributor size */
-        uint32_t rdist_stride;               /* Re-Distributor stride */
-        int rdist_count;                     /* No. of Re-Distributors */
+        /* List of contiguous occupied by the redistributors */
+        struct vgic_rdist_region {
+            paddr_t base;                   /* Base address */
+            paddr_t size;                   /* Size */
+        } rdist_regions[MAX_RDIST_COUNT];
+        int nr_regions;                     /* Number of rdist regions */
+        uint32_t rdist_stride;              /* Re-Distributor stride */
 #endif
     } vgic;
 
