diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index de180d8..c238c8f 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -968,6 +968,12 @@ static int map_device(struct domain *d, struct dt_device_node *dev)
         irq = res;
 
         DPRINT("irq %u = %u\n", i, irq);
+        /*
+         * Checking the return of vgic_reserve_virq is not
+         * necessary. It should not fail except when we try to map
+         * twice the IRQ. This can happen if the IRQ is shared
+         */
+        vgic_reserve_virq(d, irq);
         res = route_irq_to_guest(d, irq, dt_node_name(dev));
         if ( res )
         {
diff --git a/xen/arch/arm/platforms/xgene-storm.c b/xen/arch/arm/platforms/xgene-storm.c
index 0b3492d..416d42c 100644
--- a/xen/arch/arm/platforms/xgene-storm.c
+++ b/xen/arch/arm/platforms/xgene-storm.c
@@ -71,6 +71,10 @@ static int map_one_spi(struct domain *d, const char *what,
 
     printk("Additional IRQ %u (%s)\n", irq, what);
 
+    if ( !vgic_reserve_virq(d, irq) )
+        printk("Failed to reserve the vIRQ %u on dom%d\n",
+               irq, d->domain_id);
+
     ret = route_irq_to_guest(d, irq, what);
     if ( ret )
         printk("Failed to route %s to dom%d\n", what, d->domain_id);
diff --git a/xen/arch/arm/vgic.c b/xen/arch/arm/vgic.c
index 75cb7ff..dbfc259 100644
--- a/xen/arch/arm/vgic.c
+++ b/xen/arch/arm/vgic.c
@@ -87,6 +87,8 @@ int domain_vgic_init(struct domain *d)
         return -ENODEV;
     }
 
+    spin_lock_init(&d->arch.vgic.lock);
+
     d->arch.vgic.shared_irqs =
         xzalloc_array(struct vgic_irq_rank, DOMAIN_NR_RANKS(d));
     if ( d->arch.vgic.shared_irqs == NULL )
@@ -107,6 +109,15 @@ int domain_vgic_init(struct domain *d)
 
     d->arch.vgic.handler->domain_init(d);
 
+    d->arch.vgic.allocated_irqs =
+        xzalloc_array(unsigned long, BITS_TO_LONGS(vgic_num_irqs(d)));
+    if ( !d->arch.vgic.allocated_irqs )
+        return -ENOMEM;
+
+    /* vIRQ0-15 (SGIs) are reserved */
+    for (i = 0; i <= 15; i++)
+        set_bit(i, d->arch.vgic.allocated_irqs);
+
     return 0;
 }
 
@@ -119,6 +130,7 @@ void domain_vgic_free(struct domain *d)
 {
     xfree(d->arch.vgic.shared_irqs);
     xfree(d->arch.vgic.pending_irqs);
+    xfree(d->arch.vgic.allocated_irqs);
 }
 
 int vcpu_vgic_init(struct vcpu *v)
@@ -441,6 +453,70 @@ int vgic_emulate(struct cpu_user_regs *regs, union hsr hsr)
     return v->domain->arch.vgic.handler->emulate_sysreg(regs, hsr);
 }
 
+bool_t vgic_reserve_virq(struct domain *d, unsigned int virq)
+{
+    bool_t reserved;
+
+    if ( virq >= vgic_num_irqs(d) )
+        return 0;
+
+    spin_lock(&d->arch.vgic.lock);
+    reserved = !test_and_set_bit(virq, d->arch.vgic.allocated_irqs);
+    spin_unlock(&d->arch.vgic.lock);
+
+    return reserved;
+}
+
+int vgic_allocate_virq(struct domain *d, bool_t spi)
+{
+    int ret = -1;
+    unsigned int virq;
+
+    spin_lock(&d->arch.vgic.lock);
+    if ( !spi )
+    {
+        virq = find_first_zero_bit(d->arch.vgic.allocated_irqs, 32);
+        if ( virq >= 32 )
+            goto unlock;
+    }
+    else
+    {
+        virq = find_next_zero_bit(d->arch.vgic.allocated_irqs,
+                                  32, vgic_num_irqs(d));
+        if ( virq >= vgic_num_irqs(d) )
+            goto unlock;
+    }
+
+    set_bit(virq, d->arch.vgic.allocated_irqs);
+    ret = virq;
+
+unlock:
+    spin_unlock(&d->arch.vgic.lock);
+
+    return ret;
+}
+
+void vgic_free_virq(struct domain *d, unsigned int virq)
+{
+    unsigned int spi;
+
+    if ( is_hardware_domain(d) )
+        return;
+
+    if ( virq < 32 && virq >= vgic_num_irqs(d) )
+        return;
+
+    spi = virq - 32;
+
+    /* Taking the vGIC domain lock is not necessary. We don't care if
+     * the bit is cleared a bit later. What only matters is bit to 1.
+     *
+     * With this solution vgic_allocate may fail to find an vIRQ if the
+     * allocated_irqs is fully. But we don't care.
+     */
+    clear_bit(spi, d->arch.vgic.allocated_irqs);
+}
+
 /*
  * Local variables:
  * mode: C
diff --git a/xen/arch/arm/vtimer.c b/xen/arch/arm/vtimer.c
index 2e95ceb..de660bb 100644
--- a/xen/arch/arm/vtimer.c
+++ b/xen/arch/arm/vtimer.c
@@ -49,6 +49,21 @@ int domain_vtimer_init(struct domain *d)
 {
     d->arch.phys_timer_base.offset = NOW();
     d->arch.virt_timer_base.offset = READ_SYSREG64(CNTPCT_EL0);
+
+    /* At this stage vgic_reserve_virq can't fail */
+    if ( is_hardware_domain(d) )
+    {
+        BUG_ON(!vgic_reserve_virq(d, timer_get_irq(TIMER_PHYS_SECURE_PPI)));
+        BUG_ON(!vgic_reserve_virq(d, timer_get_irq(TIMER_PHYS_NONSECURE_PPI)));
+        BUG_ON(!vgic_reserve_virq(d, timer_get_irq(TIMER_VIRT_PPI)));
+    }
+    else
+    {
+        BUG_ON(!vgic_reserve_virq(d, GUEST_TIMER_PHYS_S_PPI));
+        BUG_ON(!vgic_reserve_virq(d, GUEST_TIMER_PHYS_NS_PPI));
+        BUG_ON(!vgic_reserve_virq(d, GUEST_TIMER_VIRT_PPI));
+    }
+
     return 0;
 }
 
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index 8b7dd85..d302fc9 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -90,6 +90,7 @@ struct arch_domain
         spinlock_t lock;
         int ctlr;
         int nr_spis; /* Number of SPIs */
+        unsigned long *allocated_irqs; /* bitmap of IRQs allocated */
         struct vgic_irq_rank *shared_irqs;
         /*
          * SPIs are domain global, SGIs and PPIs are per-VCPU and stored in
diff --git a/xen/include/asm-arm/vgic.h b/xen/include/asm-arm/vgic.h
index 74d5a4e..9e167fa 100644
--- a/xen/include/asm-arm/vgic.h
+++ b/xen/include/asm-arm/vgic.h
@@ -199,6 +199,19 @@ 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);
+
+/* Reserve a specific guest vIRQ */
+extern bool_t vgic_reserve_virq(struct domain *d, unsigned int virq);
+
+/*
+ * Allocate a guest VIRQ
+ *  - spi == 0 => allocate a PPI. It will be the same on every vCPU
+ *  - spi == 0 => allocate an SGI
+ */
+extern int vgic_allocate_virq(struct domain *d, bool_t spi);
+
+extern void vgic_free_virq(struct domain *d, unsigned int irq);
+
 #endif /* __ASM_ARM_VGIC_H__ */
 
 /*
