diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index 4d2a92d..c7dda9b 100644
--- a/xen/arch/arm/gic.c
+++ b/xen/arch/arm/gic.c
@@ -683,10 +683,32 @@ 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);
+            /* 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 1e1c244..7924629 100644
--- a/xen/arch/arm/vgic.c
+++ b/xen/arch/arm/vgic.c
@@ -409,6 +409,35 @@ 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 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 */
+    } else if ( !list_empty(&p->inflight) )
+        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;
@@ -546,6 +575,8 @@ static int vgic_distr_mmio_write(struct vcpu *v, mmio_info_t *info)
     int offset = (int)(info->gpa - v->domain->arch.vgic.dbase);
     int gicd_reg = REG(offset);
     uint32_t tr;
+    unsigned long trl;
+    int i;
 
     switch ( gicd_reg )
     {
@@ -630,25 +661,45 @@ static int vgic_distr_mmio_write(struct vcpu *v, mmio_info_t *info)
         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;
+        trl = (1 << v->domain->max_vcpus) - 1;
         if ( dabt.size == 2 )
-            tr = tr | (tr << 8) | (tr << 16) | (tr << 24);
+            trl = trl | (trl << 8) | (trl << 16) | (trl << 24);
         else
-            tr = (tr << (8 * (offset & 0x3)));
-        tr &= *r;
+            trl = (trl << (8 * (offset & 0x3)));
+        trl &= *r;
         /* ignore zero writes */
-        if ( !tr )
+        if ( !trl )
             goto write_ignore;
         if ( dabt.size == 2 &&
-            !((tr & 0xff) && (tr & (0xff << 8)) &&
-             (tr & (0xff << 16)) && (tr & (0xff << 24))))
+            !((trl & 0xff) && (trl & (0xff << 8)) &&
+             (trl & (0xff << 16)) && (trl & (0xff << 24))))
             goto write_ignore;
         vgic_lock_rank(v, rank);
+        i = 0;
+        while ( (i = find_next_bit(&trl, 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 = 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)] = trl;
         else
             byte_write(&rank->itargets[REG_RANK_INDEX(8, gicd_reg - GICD_ITARGETSR)],
-                       tr, offset);
+                       trl, offset);
         vgic_unlock_rank(v, rank);
         return 1;
 
@@ -786,9 +837,14 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
 
     spin_lock_irqsave(&v->arch.vgic.lock, flags);
 
+    set_bit(GIC_IRQ_GUEST_QUEUED, &n->status);
+    /* update QUEUED before MIGRATING */
+    smp_wmb();
+    if ( test_bit(GIC_IRQ_GUEST_MIGRATING, &n->status) )
+        goto out;
+
     if ( !list_empty(&n->inflight) )
     {
-        set_bit(GIC_IRQ_GUEST_QUEUED, &n->status);
         gic_raise_inflight_irq(v, irq);
         goto out;
     }
@@ -796,6 +852,7 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
     /* vcpu offline */
     if ( test_bit(_VPF_down, &v->pause_flags) )
     {
+        clear_bit(GIC_IRQ_GUEST_QUEUED, &n->status);
         spin_unlock_irqrestore(&v->arch.vgic.lock, flags);
         return;
     }
@@ -803,7 +860,6 @@ void vgic_vcpu_inject_irq(struct vcpu *v, unsigned int irq)
     priority = byte_read(rank->ipriority[REG_RANK_INDEX(8, idx)], 0, byte);
 
     n->irq = irq;
-    set_bit(GIC_IRQ_GUEST_QUEUED, &n->status);
     n->priority = priority;
 
     /* the irq is enabled */
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index 2cb6837..12b2a1d 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -55,11 +55,15 @@ 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.
+     *
      */
 #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;
