diff --git a/xen/arch/arm/gic-v2.c b/xen/arch/arm/gic-v2.c
index 256988c665..13f106cb61 100644
--- a/xen/arch/arm/gic-v2.c
+++ b/xen/arch/arm/gic-v2.c
@@ -123,6 +123,9 @@ static DEFINE_PER_CPU(u8, gic_cpu_id);
 /* Maximum cpu interface per GIC */
 #define NR_GIC_CPU_IF 8
 
+static void gicv2_irq_enable(struct irq_desc *desc);
+static void gicv2_irq_disable(struct irq_desc *desc);
+
 static inline void writeb_gicd(uint8_t val, unsigned int offset)
 {
     writeb_relaxed(val, gicv2.map_dbase + offset);
@@ -191,6 +194,38 @@ static void gicv2_save_state(struct vcpu *v)
     writel_gich(0, GICH_HCR);
 }
 
+static void gicv2_save_and_mask_hwppi(struct irq_desc *desc,
+                                      struct hwppi_state *s)
+{
+    const uint32_t mask = (1u << desc->irq); /* PPIs are IRQ# 16-31 */
+    const uint32_t pendingr = readl_gicd(GICD_ISPENDR);
+    const uint32_t activer = readl_gicd(GICD_ISACTIVER);
+    const uint32_t enabler = readl_gicd(GICD_ISENABLER);
+    const bool is_edge = !!(desc->arch.type & DT_IRQ_TYPE_EDGE_BOTH);
+
+    s->active = !!(activer & mask);
+    s->enabled = !!(enabler & mask);
+    s->pending = !!(pendingr & mask);
+
+    /* Write a 1 to IC...R to clear the corresponding bit of state */
+    if ( s->active )
+        writel_gicd(mask, GICD_ICACTIVER);
+
+    /*
+     * For an edge interrupt clear the pending state, for a level interrupt
+     * this clears the latch there is no need since saving the peripheral state
+     * (and/or restoring the next VCPU) will cause the correct action.
+     */
+    if ( is_edge && s->pending )
+        writel_gicd(mask, GICD_ICPENDR);
+
+    if ( s->enabled )
+        gicv2_irq_disable(desc);
+
+    ASSERT(!(readl_gicd(GICD_ISACTIVER) & mask));
+    ASSERT(!(readl_gicd(GICD_ISENABLER) & mask));
+}
+
 static void gicv2_restore_state(const struct vcpu *v)
 {
     int i;
@@ -203,6 +238,38 @@ static void gicv2_restore_state(const struct vcpu *v)
     writel_gich(GICH_HCR_EN, GICH_HCR);
 }
 
+static void gicv2_restore_hwppi(struct irq_desc *desc,
+                                const struct hwppi_state *s)
+{
+    const uint32_t mask = (1u << desc->irq); /* PPIs are IRQ# 16-31 */
+    const bool is_edge = !!(desc->arch.type & DT_IRQ_TYPE_EDGE_BOTH);
+
+    /*
+     * The IRQ must always have been set inactive and masked etc by
+     * the saving of the previous state via save_and_mask_hwppi.
+     */
+    ASSERT(!(readl_gicd(GICD_ISACTIVER) & mask));
+    ASSERT(!(readl_gicd(GICD_ISENABLER) & mask));
+
+    if ( s->active )
+        writel_gicd(mask, GICD_ICACTIVER);
+
+    /*
+     * Restore pending state for edge triggered interrupts only. For
+     * level triggered interrupts the level will be restored as
+     * necessary by restoring the state of the relevant peripheral.
+     *
+     * For a level triggered interrupt ISPENDR acts as a *latch* which
+     * is only cleared by ICPENDR (i.e. the input level is no longer
+     * relevant). We certainly do not want that here.
+     */
+    if ( is_edge && s->pending )
+        writel_gicd(mask, GICD_ISPENDR);
+
+    if ( s->enabled )
+        gicv2_irq_enable(desc);
+}
+
 static void gicv2_dump_state(const struct vcpu *v)
 {
     int i;
@@ -1335,7 +1402,9 @@ const static struct gic_hw_operations gicv2_ops = {
     .init                = gicv2_init,
     .secondary_init      = gicv2_secondary_cpu_init,
     .save_state          = gicv2_save_state,
+    .save_and_mask_hwppi = gicv2_save_and_mask_hwppi,
     .restore_state       = gicv2_restore_state,
+    .restore_hwppi       = gicv2_restore_hwppi,
     .dump_state          = gicv2_dump_state,
     .gic_host_irq_type   = &gicv2_host_irq_type,
     .gic_guest_irq_type  = &gicv2_guest_irq_type,
diff --git a/xen/arch/arm/gic-v3.c b/xen/arch/arm/gic-v3.c
index 0f6cbf6224..be5ea61ab5 100644
--- a/xen/arch/arm/gic-v3.c
+++ b/xen/arch/arm/gic-v3.c
@@ -63,6 +63,9 @@ static DEFINE_PER_CPU(void __iomem*, rbase);
 #define GICD_RDIST_BASE        (this_cpu(rbase))
 #define GICD_RDIST_SGI_BASE    (GICD_RDIST_BASE + SZ_64K)
 
+static void gicv3_irq_enable(struct irq_desc *desc);
+static void gicv3_irq_disable(struct irq_desc *desc);
+
 /*
  * Saves all 16(Max) LR registers. Though number of LRs implemented
  * is implementation specific.
@@ -375,6 +378,38 @@ static void gicv3_save_state(struct vcpu *v)
     v->arch.gic.v3.sre_el1 = READ_SYSREG32(ICC_SRE_EL1);
 }
 
+static void gicv3_save_and_mask_hwppi(struct irq_desc *desc,
+                                      struct hwppi_state *s)
+{
+    const uint32_t mask = (1u << desc->irq); /* PPIs are IRQ# 16-31 */
+    const uint32_t pendingr = readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISPENDR0);
+    const uint32_t activer = readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISACTIVER0);
+    const uint32_t enabler = readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISENABLER0);
+    const bool is_edge = !!(desc->arch.type & DT_IRQ_TYPE_EDGE_BOTH);
+
+    s->active = !!(activer & mask);
+    s->enabled = !!(enabler & mask);
+    s->pending = !!(pendingr & mask);
+
+    /* Write a 1 to IC...R to clear the corresponding bit of state */
+    if ( s->active )
+        writel_relaxed(mask, GICD_RDIST_SGI_BASE + GICR_ICACTIVER0);
+
+    /*
+     * For an edge interrupt clear the pending state, for a level interrupt
+     * this clears the latch there is no need since saving the peripheral state
+     * (and/or restoring the next VCPU) will cause the correct action.
+     */
+    if ( is_edge && s->pending )
+        writel_relaxed(mask, GICD_RDIST_SGI_BASE + GICR_ICPENDR0);
+
+    if ( s->enabled )
+        gicv3_irq_disable(desc);
+
+    ASSERT(!(readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISACTIVER0) & mask));
+    ASSERT(!(readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISENABLER0) & mask));
+}
+
 static void gicv3_restore_state(const struct vcpu *v)
 {
     uint32_t val;
@@ -410,6 +445,38 @@ static void gicv3_restore_state(const struct vcpu *v)
     dsb(sy);
 }
 
+static void gicv3_restore_hwppi(struct irq_desc *desc,
+                                const struct hwppi_state *s)
+{
+    const uint32_t mask = (1u << desc->irq); /* PPIs are IRQ# 16-31 */
+    const bool is_edge = !!(desc->arch.type & DT_IRQ_TYPE_EDGE_BOTH);
+
+    /*
+     * The IRQ must always have been set inactive and masked etc by
+     * the saving of the previous state via save_and_mask_hwppi.
+     */
+    ASSERT(!(readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISACTIVER0) & mask));
+    ASSERT(!(readl_relaxed(GICD_RDIST_SGI_BASE + GICR_ISENABLER0) & mask));
+
+    if ( s->active )
+        writel_relaxed(mask, GICD_RDIST_SGI_BASE + GICR_ICACTIVER0);
+
+    /*
+     * Restore pending state for edge triggered interrupts only. For
+     * level triggered interrupts the level will be restored as
+     * necessary by restoring the state of the relevant peripheral.
+     *
+     * For a level triggered interrupt ISPENDR acts as a *latch* which
+     * is only cleared by ICPENDR (i.e. the input level is no longer
+     * relevant). We certainly do not want that here.
+     */
+    if ( is_edge && s->pending )
+        writel_relaxed(mask, GICD_RDIST_SGI_BASE + GICR_ISPENDR0);
+
+    if ( s->enabled )
+        gicv3_irq_enable(desc);
+}
+
 static void gicv3_dump_state(const struct vcpu *v)
 {
     int i;
@@ -1835,7 +1902,9 @@ static const struct gic_hw_operations gicv3_ops = {
     .info                = &gicv3_info,
     .init                = gicv3_init,
     .save_state          = gicv3_save_state,
+    .save_and_mask_hwppi = gicv3_save_and_mask_hwppi,
     .restore_state       = gicv3_restore_state,
+    .restore_hwppi       = gicv3_restore_hwppi,
     .dump_state          = gicv3_dump_state,
     .gic_host_irq_type   = &gicv3_host_irq_type,
     .gic_guest_irq_type  = &gicv3_guest_irq_type,
diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index 113655a789..75921724dd 100644
--- a/xen/arch/arm/gic.c
+++ b/xen/arch/arm/gic.c
@@ -64,6 +64,17 @@ unsigned int gic_number_lines(void)
     return gic_hw_ops->info->nr_lines;
 }
 
+void gic_hwppi_state_init(struct hwppi_state *s, unsigned irq)
+{
+    memset(s, 0, sizeof(*s));
+    s->irq = irq;
+}
+
+void gic_hwppi_set_pending(struct hwppi_state *s)
+{
+    s->pending = true;
+}
+
 void gic_save_state(struct vcpu *v)
 {
     ASSERT(!local_irq_is_enabled());
@@ -78,6 +89,25 @@ void gic_save_state(struct vcpu *v)
     isb();
 }
 
+void gic_save_and_mask_hwppi(struct vcpu *v, const unsigned virq,
+                             struct hwppi_state *s)
+{
+    struct pending_irq *p = irq_to_pending(v, virq);
+    struct irq_desc *desc = p->desc;
+
+    spin_lock(&desc->lock);
+
+    ASSERT(virq >= 16 && virq < 32);
+    ASSERT(desc->irq >= 16 && desc->irq < 32);
+    ASSERT(!is_idle_vcpu(v));
+
+    s->inprogress = test_and_clear_bit(_IRQ_INPROGRESS, &desc->status);
+
+    gic_hw_ops->save_and_mask_hwppi(desc, s);
+
+    spin_unlock(&desc->lock);
+}
+
 void gic_restore_state(struct vcpu *v)
 {
     ASSERT(!local_irq_is_enabled());
@@ -89,6 +119,30 @@ void gic_restore_state(struct vcpu *v)
     isb();
 }
 
+void gic_restore_hwppi(struct vcpu *v,
+                       const unsigned virq,
+                       const struct hwppi_state *s)
+{
+    struct pending_irq *p = irq_to_pending(v, virq);
+    struct irq_desc *desc = irq_to_desc(s->irq);
+
+    spin_lock(&desc->lock);
+
+    ASSERT(virq >= 16 && virq < 32);
+    ASSERT(!is_idle_vcpu(v));
+
+    p->desc = desc; /* Migrate to new physical processor */
+
+    irq_set_virq(desc, virq);
+
+    gic_hw_ops->restore_hwppi(desc, s);
+
+    if ( s->inprogress )
+        set_bit(_IRQ_INPROGRESS, &desc->status);
+
+    spin_unlock(&desc->lock);
+}
+
 /* desc->irq needs to be disabled before calling this function */
 void gic_set_irq_type(struct irq_desc *desc, unsigned int type)
 {
diff --git a/xen/arch/arm/irq.c b/xen/arch/arm/irq.c
index c80782026f..1a8e599c2e 100644
--- a/xen/arch/arm/irq.c
+++ b/xen/arch/arm/irq.c
@@ -150,6 +150,13 @@ static inline struct irq_guest *irq_get_guest_info(struct irq_desc *desc)
     return desc->action->dev_id;
 }
 
+void irq_set_virq(struct irq_desc *desc, unsigned virq)
+{
+    struct irq_guest *info = irq_get_guest_info(desc);
+    ASSERT(test_bit(_IRQ_PER_CPU, &desc->status));
+    info->virq = virq;
+}
+
 static inline struct domain *irq_get_domain(struct irq_desc *desc)
 {
     return irq_get_guest_info(desc)->d;
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index f3f3fb7d7f..c3f4cd5069 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -34,6 +34,17 @@ enum domain_type {
 /* The hardware domain has always its memory direct mapped. */
 #define is_domain_direct_mapped(d) ((d) == hardware_domain)
 
+struct hwppi_state {
+    /* h/w state */
+    unsigned irq;
+    unsigned long enabled:1;
+    unsigned long pending:1;
+    unsigned long active:1;
+
+    /* Xen s/w state */
+    unsigned long inprogress:1;
+};
+
 struct vtimer {
     struct vcpu *v;
     int irq;
diff --git a/xen/include/asm-arm/gic.h b/xen/include/asm-arm/gic.h
index 793d324b33..1164e0c7a6 100644
--- a/xen/include/asm-arm/gic.h
+++ b/xen/include/asm-arm/gic.h
@@ -275,6 +275,26 @@ extern int gicv_setup(struct domain *d);
 extern void gic_save_state(struct vcpu *v);
 extern void gic_restore_state(struct vcpu *v);
 
+/*
+ * Save/restore the state of a single PPI which must be routed to
+ * <current-vcpu> (that is, is defined to be injected to the current
+ * vcpu).
+ *
+ * We expect the device which use this PPI to be quiet while we
+ * save/restore.
+ *
+ * For instance we want to disable the timer before saving the state.
+ * Otherwise we will mess up the state.
+ */
+struct hwppi_state;
+extern void gic_hwppi_state_init(struct hwppi_state *s, unsigned irq);
+extern void gic_hwppi_set_pending(struct hwppi_state *s);
+extern void gic_save_and_mask_hwppi(struct vcpu *v, unsigned irq,
+                                    struct hwppi_state *s);
+extern void gic_restore_hwppi(struct vcpu *v,
+                              const unsigned virq,
+                              const struct hwppi_state *s);
+
 /* SGI (AKA IPIs) */
 enum gic_sgi {
     GIC_SGI_EVENT_CHECK = 0,
@@ -325,8 +345,10 @@ struct gic_hw_operations {
     int (*init)(void);
     /* Save GIC registers */
     void (*save_state)(struct vcpu *);
+    void (*save_and_mask_hwppi)(struct irq_desc *desc, struct hwppi_state *s);
     /* Restore GIC registers */
     void (*restore_state)(const struct vcpu *);
+    void (*restore_hwppi)(struct irq_desc *desc, const struct hwppi_state *s);
     /* Dump GIC LR register information */
     void (*dump_state)(const struct vcpu *);
 
diff --git a/xen/include/asm-arm/irq.h b/xen/include/asm-arm/irq.h
index e14001b5c6..3b37a21c06 100644
--- a/xen/include/asm-arm/irq.h
+++ b/xen/include/asm-arm/irq.h
@@ -96,6 +96,8 @@ void irq_set_affinity(struct irq_desc *desc, const cpumask_t *cpu_mask);
  */
 bool irq_type_set_by_domain(const struct domain *d);
 
+void irq_set_virq(struct irq_desc *desc, unsigned virq);
+
 #endif /* _ASM_HW_IRQ_H */
 /*
  * Local variables:
