diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index e1e27b35..b5269d4 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);
 
@@ -372,10 +373,33 @@ 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 {
+            int m, q;
             list_del_init(&p->inflight);
+
+            m = test_and_clear_bit(GIC_IRQ_GUEST_MIGRATING, &p->status);
+            p->vcpu_migrate_from = NULL;
+            /* check MIGRATING before QUEUED */
+            smp_rmb();
+            q = test_bit(GIC_IRQ_GUEST_QUEUED, &p->status);
+            if ( m && q )
+            {
+                struct vcpu *v_target;
+
+                /* It is safe to temporarily drop the lock because we
+                 * are finished dealing with this LR. We'll take the
+                 * lock before reading the next. */
+                spin_unlock(&v->arch.vgic.lock);
+                /* vgic_get_target_vcpu takes the rank lock, ensuring
+                 * consistency with other itarget changes. */
+                v_target = vgic_get_target_vcpu(v, irq);
+                vgic_vcpu_inject_irq(v_target, irq);
+                spin_lock(&v->arch.vgic.lock);
+            }
+        }
     }
 }
 
diff --git a/xen/arch/arm/vgic.c b/xen/arch/arm/vgic.c
index e928879..8827a77 100644
--- a/xen/arch/arm/vgic.c
+++ b/xen/arch/arm/vgic.c
@@ -382,6 +382,46 @@ struct vcpu *vgic_get_target_vcpu(struct vcpu *v, unsigned int irq)
     return v_target;
 }
 
+static 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) )
+    {
+        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) )
+    {
+        p->vcpu_migrate_from = old;
+        set_bit(GIC_IRQ_GUEST_MIGRATING, &p->status);
+    }
+
+    spin_unlock_irqrestore(&old->arch.vgic.lock, flags);
+}
+
 static void vgic_disable_irqs(struct vcpu *v, uint32_t r, int n)
 {
     const unsigned long mask = r;
@@ -598,35 +638,60 @@ static int vgic_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 != 0 && dabt.size != 2 ) goto bad_width;
         rank = vgic_rank_offset(v, 8, gicd_reg - GICD_ITARGETSR);
         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 * (offset & 0x3)));
-        tr &= *r;
+            target = (target << (8 * (offset & 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, target, old_target;
+            unsigned long old_target_mask;
+            struct vcpu *v_target, *v_old;
+
+            target = i % 8;
+            old_target_mask = vgic_byte_read(rank->itargets[REG_RANK_INDEX(8, gicd_reg - GICD_ITARGETSR)], 0, i/8);
+            old_target = find_first_bit(&old_target_mask, 8);
+
+            if ( target != old_target )
+            {
+                irq = offset + (i / 8);
+                v_target = v->domain->vcpu[target];
+                v_old = v->domain->vcpu[old_target];
+                vgic_migrate_irq(v_old, v_target, irq);
+            }
+            i += 8 - target;
+        }
         if ( dabt.size == 2 )
-            rank->itargets[REG_RANK_INDEX(8, gicd_reg - GICD_ITARGETSR)] = tr;
+            rank->itargets[REG_RANK_INDEX(8, gicd_reg - GICD_ITARGETSR)] = target;
         else
         {
             int ri = REG_RANK_INDEX(8, gicd_reg - GICD_ITARGETSR);
-            vgic_byte_write(&rank->itargets[ri], tr, offset);
+            vgic_byte_write(&rank->itargets[ri], target, offset);
         }
         vgic_unlock_rank(v, rank);
         return 1;
+    }
 
     case GICD_IPRIORITYR ... GICD_IPRIORITYRN:
         if ( dabt.size != 0 && dabt.size != 2 ) goto bad_width;
@@ -747,6 +812,7 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
     struct pending_irq *iter, *n = irq_to_pending(v, irq);
     unsigned long flags;
     bool_t running;
+    struct vcpu *vcpu_migrate_from;
 
     spin_lock_irqsave(&v->arch.vgic.lock, flags);
 
@@ -758,6 +824,21 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
     }
 
     set_bit(GIC_IRQ_GUEST_QUEUED, &n->status);
+    vcpu_migrate_from = n->vcpu_migrate_from;
+    /* update QUEUED before MIGRATING */
+    smp_wmb();
+    if ( test_bit(GIC_IRQ_GUEST_MIGRATING, &n->status) )
+    {
+        spin_unlock_irqrestore(&v->arch.vgic.lock, flags);
+
+        /* The old vcpu must have EOIed the SGI but not cleared the LR.
+         * Give it a kick. */
+        running = n->vcpu_migrate_from->is_running;
+        vcpu_unblock(n->vcpu_migrate_from);
+        if ( running )
+            smp_send_event_check_mask(cpumask_of(n->vcpu_migrate_from->processor));
+        return;
+    }
 
     if ( !list_empty(&n->inflight) )
     {
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index 077ac1e..70c1215 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -48,17 +48,24 @@ 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;
 #define GIC_INVALID_LR         ~(uint8_t)0
     uint8_t lr;
     uint8_t priority;
+    /* keeps track of the vcpu this irq is currently migrating from */
+    struct vcpu *vcpu_migrate_from;
     /* inflight is used to append instances of pending_irq to
      * vgic.inflight_irqs */
     struct list_head inflight;
