diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index 256d9cf..3e75fc5 100644
--- a/xen/arch/arm/gic.c
+++ b/xen/arch/arm/gic.c
@@ -33,6 +33,7 @@
 #include <asm/device.h>
 #include <asm/io.h>
 #include <asm/gic.h>
+#include <asm/vgic.h>
 
 static void gic_restore_pending_irqs(struct vcpu *v);
 
@@ -375,10 +376,13 @@ static void gic_update_one_lr(struct vcpu *v, int i)
         clear_bit(GIC_IRQ_GUEST_ACTIVE, &p->status);
         p->lr = GIC_INVALID_LR;
         if ( test_bit(GIC_IRQ_GUEST_ENABLED, &p->status) &&
-             test_bit(GIC_IRQ_GUEST_QUEUED, &p->status) )
+             test_bit(GIC_IRQ_GUEST_QUEUED, &p->status) &&
+             !test_bit(GIC_IRQ_GUEST_MIGRATING, &p->status) )
             gic_raise_guest_irq(v, irq, p->priority);
-        else
+        else {
             list_del_init(&p->inflight);
+            clear_bit(GIC_IRQ_GUEST_MIGRATING, &p->status);
+        }
     }
 }
 
diff --git a/xen/arch/arm/vgic-v2.c b/xen/arch/arm/vgic-v2.c
index 63d4f65..39d8272 100644
--- a/xen/arch/arm/vgic-v2.c
+++ b/xen/arch/arm/vgic-v2.c
@@ -356,34 +356,60 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info)
         goto write_ignore;
 
     case GICD_ITARGETSR + 8 ... GICD_ITARGETSRN:
+    {
+        /* unsigned long needed for find_next_bit */
+        unsigned long target;
+        int i;
         if ( dabt.size != DABT_BYTE && dabt.size != DABT_WORD ) goto bad_width;
         rank = vgic_rank_offset(v, 8, gicd_reg - GICD_ITARGETSR, DABT_WORD);
         if ( rank == NULL) goto write_ignore;
         /* 8-bit vcpu mask for this domain */
         BUG_ON(v->domain->max_vcpus > 8);
-        tr = (1 << v->domain->max_vcpus) - 1;
+        target = (1 << v->domain->max_vcpus) - 1;
         if ( dabt.size == 2 )
-            tr = tr | (tr << 8) | (tr << 16) | (tr << 24);
+            target = target | (target << 8) | (target << 16) | (target << 24);
         else
-            tr = (tr << (8 * (gicd_reg & 0x3)));
-        tr &= *r;
+            target = (target << (8 * (gicd_reg & 0x3)));
+        target &= *r;
         /* ignore zero writes */
-        if ( !tr )
+        if ( !target )
             goto write_ignore;
         /* For word reads ignore writes where any single byte is zero */
         if ( dabt.size == 2 &&
-            !((tr & 0xff) && (tr & (0xff << 8)) &&
-             (tr & (0xff << 16)) && (tr & (0xff << 24))))
+            !((target & 0xff) && (target & (0xff << 8)) &&
+             (target & (0xff << 16)) && (target & (0xff << 24))))
             goto write_ignore;
         vgic_lock_rank(v, rank);
+        i = 0;
+        while ( (i = find_next_bit(&target, 32, i)) < 32 )
+        {
+            unsigned int irq, new_target, old_target;
+            unsigned long old_target_mask;
+            struct vcpu *v_target, *v_old;
+
+            new_target = i % 8;
+            old_target_mask = vgic_byte_read(rank->itargets[REG_RANK_INDEX(8,
+                                             gicd_reg - GICD_ITARGETSR, DABT_WORD)], 0, i/8);
+            old_target = find_first_bit(&old_target_mask, 8);
+
+            if ( new_target != old_target )
+            {
+                irq = gicd_reg - GICD_ITARGETSR + (i / 8);
+                v_target = v->domain->vcpu[new_target];
+                v_old = v->domain->vcpu[old_target];
+                vgic_migrate_irq(v_old, v_target, irq);
+            }
+            i += 8 - new_target;
+        }
         if ( dabt.size == DABT_WORD )
             rank->itargets[REG_RANK_INDEX(8, gicd_reg - GICD_ITARGETSR,
-                                          DABT_WORD)] = tr;
+                                          DABT_WORD)] = target;
         else
             vgic_byte_write(&rank->itargets[REG_RANK_INDEX(8,
-                       gicd_reg - GICD_ITARGETSR, DABT_WORD)], tr, gicd_reg);
+                       gicd_reg - GICD_ITARGETSR, DABT_WORD)], target, gicd_reg);
         vgic_unlock_rank(v, rank);
         return 1;
+    }
 
     case GICD_IPRIORITYR ... GICD_IPRIORITYRN:
         if ( dabt.size != DABT_BYTE && dabt.size != DABT_WORD ) goto bad_width;
diff --git a/xen/arch/arm/vgic.c b/xen/arch/arm/vgic.c
index 9947e8c..e0dcaf6 100644
--- a/xen/arch/arm/vgic.c
+++ b/xen/arch/arm/vgic.c
@@ -165,6 +165,44 @@ struct vcpu *vgic_get_target_vcpu(struct vcpu *v, unsigned int irq)
     return v_target;
 }
 
+void vgic_migrate_irq(struct vcpu *old, struct vcpu *new, unsigned int irq)
+{
+    unsigned long flags;
+    struct pending_irq *p = irq_to_pending(old, irq);
+
+    /* nothing to do for virtual interrupts */
+    if ( p->desc == NULL )
+        return;
+
+    /* migration already in progress, no need to do anything */
+    if ( test_bit(GIC_IRQ_GUEST_MIGRATING, &p->status) )
+        return;
+
+    spin_lock_irqsave(&old->arch.vgic.lock, flags);
+
+    if ( list_empty(&p->inflight) )
+    {
+        spin_unlock_irqrestore(&old->arch.vgic.lock, flags);
+        return;
+    }
+    /* If the IRQ is still lr_pending, re-inject it to the new vcpu */
+    if ( !list_empty(&p->lr_queue) )
+    {
+        clear_bit(GIC_IRQ_GUEST_QUEUED, &p->status);
+        list_del_init(&p->lr_queue);
+        list_del_init(&p->inflight);
+        spin_unlock_irqrestore(&old->arch.vgic.lock, flags);
+        vgic_vcpu_inject_irq(new, irq);
+        return;
+    }
+    /* if the IRQ is in a GICH_LR register, set GIC_IRQ_GUEST_MIGRATING
+     * and wait for the EOI */
+    if ( !list_empty(&p->inflight) )
+        set_bit(GIC_IRQ_GUEST_MIGRATING, &p->status);
+
+    spin_unlock_irqrestore(&old->arch.vgic.lock, flags);
+}
+
 void vgic_disable_irqs(struct vcpu *v, uint32_t r, int n)
 {
     struct domain *d = v->domain;
diff --git a/xen/include/asm-arm/vgic.h b/xen/include/asm-arm/vgic.h
index 81a3eef..434a625 100644
--- a/xen/include/asm-arm/vgic.h
+++ b/xen/include/asm-arm/vgic.h
@@ -55,11 +55,16 @@ struct pending_irq
      * GIC_IRQ_GUEST_ENABLED: the guest IRQ is enabled at the VGICD
      * level (GICD_ICENABLER/GICD_ISENABLER).
      *
+     * GIC_IRQ_GUEST_MIGRATING: the irq is being migrated to a different
+     * vcpu while it is still inflight and on an GICH_LR register on the
+     * old vcpu.
+     *
      */
 #define GIC_IRQ_GUEST_QUEUED   0
 #define GIC_IRQ_GUEST_ACTIVE   1
 #define GIC_IRQ_GUEST_VISIBLE  2
 #define GIC_IRQ_GUEST_ENABLED  3
+#define GIC_IRQ_GUEST_MIGRATING   4
     unsigned long status;
     struct irq_desc *desc; /* only set it the irq corresponds to a physical irq */
     int irq;
@@ -169,6 +174,7 @@ extern int vcpu_vgic_free(struct vcpu *v);
 extern int vgic_to_sgi(struct vcpu *v, register_t sgir,
                        enum gic_sgi_mode irqmode, int virq,
                        unsigned long vcpu_mask);
+extern void vgic_migrate_irq(struct vcpu *old, struct vcpu *new, unsigned int irq);
 #endif /* __ASM_ARM_VGIC_H__ */
 
 /*
