diff --git a/xen/arch/arm/vgic/vgic-mmio-v2.c b/xen/arch/arm/vgic/vgic-mmio-v2.c
new file mode 100644
index 0000000000..ee685a5a07
--- /dev/null
+++ b/xen/arch/arm/vgic/vgic-mmio-v2.c
@@ -0,0 +1,83 @@
+/*
+ * VGICv2 MMIO handling functions
+ * Imported from Linux ("new" KVM VGIC) and heavily adapted to Xen.
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License version 2 as
+ * published by the Free Software Foundation.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ */
+
+#include <xen/bitops.h>
+#include <xen/sched.h>
+#include <xen/sizes.h>
+#include <asm/arm_vgic.h>
+
+#include "vgic.h"
+#include "vgic-mmio.h"
+
+static const struct vgic_register_region vgic_v2_dist_registers[] = {
+    REGISTER_DESC_WITH_LENGTH(GICD_CTLR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, 12,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_IGROUPR,
+        vgic_mmio_read_rao, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ISENABLER,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ICENABLER,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ISPENDR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ICPENDR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ISACTIVER,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ICACTIVER,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 1,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_IPRIORITYR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 8,
+        VGIC_ACCESS_32bit | VGIC_ACCESS_8bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ITARGETSR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 8,
+        VGIC_ACCESS_32bit | VGIC_ACCESS_8bit),
+    REGISTER_DESC_WITH_BITS_PER_IRQ(GICD_ICFGR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, NULL, NULL, 2,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_LENGTH(GICD_SGIR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, 4,
+        VGIC_ACCESS_32bit),
+    REGISTER_DESC_WITH_LENGTH(GICD_CPENDSGIR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, 16,
+        VGIC_ACCESS_32bit | VGIC_ACCESS_8bit),
+    REGISTER_DESC_WITH_LENGTH(GICD_SPENDSGIR,
+        vgic_mmio_read_raz, vgic_mmio_write_wi, 16,
+        VGIC_ACCESS_32bit | VGIC_ACCESS_8bit),
+};
+
+unsigned int vgic_v2_init_dist_iodev(struct vgic_io_device *dev)
+{
+    dev->regions = vgic_v2_dist_registers;
+    dev->nr_regions = ARRAY_SIZE(vgic_v2_dist_registers);
+
+    return SZ_4K;
+}
+
+/*
+ * Local variables:
+ * mode: C
+ * c-file-style: "BSD"
+ * c-basic-offset: 4
+ * indent-tabs-mode: nil
+ * End:
+ */
diff --git a/xen/arch/arm/vgic/vgic-mmio.c b/xen/arch/arm/vgic/vgic-mmio.c
index 3c70945466..59703a6909 100644
--- a/xen/arch/arm/vgic/vgic-mmio.c
+++ b/xen/arch/arm/vgic/vgic-mmio.c
@@ -182,6 +182,32 @@ struct mmio_handler_ops xen_io_gic_ops = {
     .write = dispatch_mmio_write,
 };
 
+int vgic_register_dist_iodev(struct domain *d, paddr_t dist_base_address,
+                 enum vgic_type type)
+{
+    struct vgic_io_device *io_device = &d->arch.vgic.dist_iodev;
+    int ret = 0;
+    unsigned int len;
+
+    switch (type)
+    {
+    case VGIC_V2:
+        len = vgic_v2_init_dist_iodev(io_device);
+        break;
+    default:
+        BUG_ON(1);
+    }
+
+    io_device->base_addr = dist_base_address;
+    io_device->iodev_type = IODEV_DIST;
+    io_device->redist_vcpu = NULL;
+
+    register_mmio_handler(d, &xen_io_gic_ops, dist_base_address, len,
+                  io_device);
+
+    return ret;
+}
+
 /*
  * Local variables:
  * mode: C
diff --git a/xen/arch/arm/vgic/vgic-mmio.h b/xen/arch/arm/vgic/vgic-mmio.h
index 375b70561d..10ac682296 100644
--- a/xen/arch/arm/vgic/vgic-mmio.h
+++ b/xen/arch/arm/vgic/vgic-mmio.h
@@ -137,6 +137,8 @@ unsigned long vgic_mmio_read_rao(struct vcpu *vcpu,
 void vgic_mmio_write_wi(struct vcpu *vcpu, paddr_t addr,
                         unsigned int len, unsigned long val);
 
+unsigned int vgic_v2_init_dist_iodev(struct vgic_io_device *dev);
+
 /* Find the proper register handler entry given a certain address offset */
 const struct vgic_register_region *
 vgic_find_mmio_region(const struct vgic_register_region *regions,
diff --git a/xen/arch/arm/vgic/vgic.h b/xen/arch/arm/vgic/vgic.h
index 426b34d0ce..7747d3f3e0 100644
--- a/xen/arch/arm/vgic/vgic.h
+++ b/xen/arch/arm/vgic/vgic.h
@@ -49,6 +49,8 @@ void vgic_v2_fold_lr_state(struct vcpu *vcpu);
 void vgic_v2_populate_lr(struct vcpu *vcpu, struct vgic_irq *irq, int lr);
 void vgic_v2_clear_lr(struct vcpu *vcpu, int lr);
 void vgic_v2_set_underflow(struct vcpu *vcpu);
+int vgic_register_dist_iodev(struct domain *d, paddr_t dist_base_address,
+                 enum vgic_type);
 
 void vgic_v2_save_state(struct vcpu *vcpu);
 void vgic_v2_restore_state(struct vcpu *vcpu);
