diff --git a/xen/arch/arm/domain.c b/xen/arch/arm/domain.c
index 9ca44ea..ebd94d3 100644
--- a/xen/arch/arm/domain.c
+++ b/xen/arch/arm/domain.c
@@ -481,6 +481,10 @@ int arch_domain_create(struct domain *d, unsigned int domcr_flags)
     d->arch.vpidr = boot_cpu_data.midr.bits;
     d->arch.vmpidr = boot_cpu_data.mpidr.bits;
 
+    /* TODO: retrieve the evtchn IRQ from the guest DTS */
+    if ( d->domain_id )
+        d->arch.evtchn_irq = dom0->arch.evtchn_irq;
+
     clear_page(d->shared_info);
     share_xen_page_with_guest(
         virt_to_page(d->shared_info), d, XENSHARE_writable);
@@ -636,6 +640,8 @@ void arch_dump_domain_info(struct domain *d)
 {
     struct vcpu *v;
 
+    printk("Event channel IRQ: %u\n", d->arch.evtchn_irq);
+
     for_each_vcpu ( d, v )
     {
         gic_dump_info(v);
@@ -672,7 +678,7 @@ void vcpu_mark_events_pending(struct vcpu *v)
     if ( already_pending )
         return;
 
-    vgic_vcpu_inject_irq(v, VGIC_IRQ_EVTCHN_CALLBACK, 1);
+    vgic_vcpu_inject_irq(v, v->domain->arch.evtchn_irq, 1);
 }
 
 /*
diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index b92c64b..f857e40 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -258,7 +258,9 @@ static int fdt_next_dom0_node(const void *fdt, int node,
     return node;
 }
 
-static void make_hypervisor_node(void *fdt, int addrcells, int sizecells)
+static void make_hypervisor_node(struct domain *d,
+                                 void *fdt, int addrcells,
+                                 int sizecells)
 {
     const char compat[] =
         "xen,xen-"__stringify(XEN_VERSION)"."__stringify(XEN_SUBVERSION)"\0"
@@ -291,9 +293,12 @@ static void make_hypervisor_node(void *fdt, int addrcells, int sizecells)
      * interrupts is evtchn upcall  <1 15 0xf08>
      * See linux Documentation/devicetree/bindings/arm/gic.txt
      */
+    BUG_ON(!irq_is_ppi(d->arch.evtchn_irq));
     intr[0] = cpu_to_fdt32(1); /* is a PPI */
-    intr[1] = cpu_to_fdt32(VGIC_IRQ_EVTCHN_CALLBACK - 16); /* PPIs start at 16 */
-    intr[2] = cpu_to_fdt32(0xf08); /* Active-low level-sensitive */
+    intr[1] = cpu_to_fdt32(d->arch.evtchn_irq - FIRST_PPI_IRQ);
+    /* PPI attached for each CPU and active-low level-sensitive */
+    intr[2] = cpu_to_fdt32(((0xf) << DT_IRQ_TYPE_CPU_MASK_SHIFT) |
+                           DT_IRQ_TYPE_LEVEL_LOW);
 
     fdt_property(fdt, "interrupts", intr, sizeof(intr[0]) * 3);
 
@@ -348,14 +353,15 @@ static int write_nodes(struct domain *d, struct kernel_info *kinfo,
     while ( last_depth-- >= 1 )
         fdt_end_node(kinfo->fdt);
 
-    make_hypervisor_node(kinfo->fdt, address_cells[0], size_cells[0]);
+    make_hypervisor_node(d, kinfo->fdt, address_cells[0], size_cells[0]);
 
     fdt_end_node(kinfo->fdt);
     return 0;
 }
 
 /* Map the device in the domain */
-static int map_device(struct domain *d, const struct dt_device_node *dev)
+static int map_device(struct domain *d, const struct dt_device_node *dev,
+                      bool_t ppis[])
 {
     unsigned int nirq;
     unsigned int naddr;
@@ -403,6 +409,9 @@ static int map_device(struct domain *d, const struct dt_device_node *dev)
         DPRINT("irq %u = %u type = 0x%x\n", i, irq.irq, irq.type);
         /* Don't check return because the IRQ can be use by multiple device */
         gic_route_irq_to_guest(d, &irq, dt_node_name(dev));
+
+        if (irq_is_ppi(irq.irq))
+            ppis[irq.irq - FIRST_PPI_IRQ] = 1;
     }
 
     /* Map the address ranges */
@@ -434,7 +443,8 @@ static int map_device(struct domain *d, const struct dt_device_node *dev)
     return 0;
 }
 
-static int handle_node(struct domain *d, const struct dt_device_node *np)
+static int handle_node(struct domain *d, const struct dt_device_node *np,
+                       bool_t ppis[])
 {
     const struct dt_device_node *child;
     int res;
@@ -449,7 +459,7 @@ static int handle_node(struct domain *d, const struct dt_device_node *np)
 
     if ( dt_device_used_by(np) != DOMID_XEN )
     {
-        res = map_device(d, np);
+        res = map_device(d, np, ppis);
 
         if ( res )
             return res;
@@ -457,7 +467,7 @@ static int handle_node(struct domain *d, const struct dt_device_node *np)
 
     for ( child = np->child; child != NULL; child = child->sibling )
     {
-        res = handle_node(d, child);
+        res = handle_node(d, child, ppis);
         if ( res )
             return res;
     }
@@ -467,9 +477,41 @@ static int handle_node(struct domain *d, const struct dt_device_node *np)
 
 static int map_devices_from_device_tree(struct domain *d)
 {
+    bool_t ppis[NR_PPI_IRQS] = {0};
+    int res;
+    unsigned int i;
+
     ASSERT(dt_host && (dt_host->sibling == NULL));
 
-    return handle_node(d, dt_host);
+    res = handle_node(d, dt_host, ppis);
+
+    /*
+     * Fill by hand timer IRQS ppis as we don't map it in Dom0
+     * We assume the host IRQs and the dom0 IRQs are the same for the timer.
+     */
+    for ( i = TIMER_PHYS_SECURE_PPI; i < MAX_TIMER_PPI; i++ )
+    {
+        const struct dt_irq *irq = timer_dt_irq(i);
+
+        if ( irq_is_ppi(irq->irq) )
+            ppis[irq->irq - FIRST_PPI_IRQ] = 1;
+    }
+
+    /* Start from the last PPIs and decrease to find a free PPI */
+    for ( i = NR_PPI_IRQS; i != 0; i-- )
+    {
+        if ( !ppis[i - 1] )
+            break;
+    }
+
+    if ( i == 0 )
+        panic("Can't find a free PPI for the event channel IRQ\n");
+
+    d->arch.evtchn_irq = (i - 1) + FIRST_PPI_IRQ;
+
+    printk(XENLOG_INFO "DOM0 Event channel IRQ: %u\n", d->arch.evtchn_irq);
+
+    return res;
 }
 
 static int prepare_dtb(struct domain *d, struct kernel_info *kinfo)
@@ -546,16 +588,16 @@ int construct_dom0(struct domain *d)
 
     d->max_pages = ~0U;
 
-    rc = prepare_dtb(d, &kinfo);
+    map_devices_from_device_tree(d);
+    rc = platform_specific_mapping(d);
     if ( rc < 0 )
         return rc;
 
-    rc = kernel_prepare(&kinfo);
+    rc = prepare_dtb(d, &kinfo);
     if ( rc < 0 )
         return rc;
 
-    map_devices_from_device_tree(d);
-    rc = platform_specific_mapping(d);
+    rc = kernel_prepare(&kinfo);
     if ( rc < 0 )
         return rc;
 
diff --git a/xen/arch/arm/gic.c b/xen/arch/arm/gic.c
index 30bf8d1..aa2710c 100644
--- a/xen/arch/arm/gic.c
+++ b/xen/arch/arm/gic.c
@@ -682,7 +682,7 @@ int gic_events_need_delivery(void)
 void gic_inject(void)
 {
     if ( vcpu_info(current, evtchn_upcall_pending) )
-        vgic_vcpu_inject_irq(current, VGIC_IRQ_EVTCHN_CALLBACK, 1);
+        vgic_vcpu_inject_irq(current, current->domain->arch.evtchn_irq, 1);
 
     gic_restore_pending_irqs(current);
     if (!gic_events_need_delivery())
diff --git a/xen/include/asm-arm/domain.h b/xen/include/asm-arm/domain.h
index cb251cc..6fc3ddd 100644
--- a/xen/include/asm-arm/domain.h
+++ b/xen/include/asm-arm/domain.h
@@ -76,6 +76,8 @@ struct arch_domain
         uint64_t offset;
     } virt_timer_base;
 
+    unsigned int evtchn_irq; /* Event Channel IRQ */
+
     struct {
         /*
          * Covers access to other members of this struct _except_ for
diff --git a/xen/include/asm-arm/event.h b/xen/include/asm-arm/event.h
index ed05901..f8e8297 100644
--- a/xen/include/asm-arm/event.h
+++ b/xen/include/asm-arm/event.h
@@ -9,7 +9,9 @@ void vcpu_mark_events_pending(struct vcpu *v);
 
 static inline int local_events_need_delivery_nomask(void)
 {
-    struct pending_irq *p = irq_to_pending(current, VGIC_IRQ_EVTCHN_CALLBACK);
+    struct pending_irq *p;
+
+    p = irq_to_pending(current, current->domain->arch.evtchn_irq);
 
     /* XXX: if the first interrupt has already been delivered, we should
      * check whether any other interrupts with priority higher than the
diff --git a/xen/include/asm-arm/gic.h b/xen/include/asm-arm/gic.h
index 513c1fc..fc18c9e 100644
--- a/xen/include/asm-arm/gic.h
+++ b/xen/include/asm-arm/gic.h
@@ -129,9 +129,6 @@
 #define GICH_LR_CPUID_SHIFT     9
 #define GICH_VTR_NRLRGS         0x3f
 
-/* XXX: write this into the DT */
-#define VGIC_IRQ_EVTCHN_CALLBACK 31
-
 #ifndef __ASSEMBLY__
 #include <xen/device_tree.h>
 
diff --git a/xen/include/asm-arm/irq.h b/xen/include/asm-arm/irq.h
index 80ff68d..eeddd82 100644
--- a/xen/include/asm-arm/irq.h
+++ b/xen/include/asm-arm/irq.h
@@ -46,6 +46,14 @@ int __init request_dt_irq(const struct dt_irq *irq,
                           void *dev_id);
 int __init setup_dt_irq(const struct dt_irq *irq, struct irqaction *new);
 
+#define FIRST_PPI_IRQ   16
+#define NR_PPI_IRQS     16
+
+static inline bool_t irq_is_ppi(unsigned int irq)
+{
+    return ((irq >= FIRST_PPI_IRQ) && (irq < (FIRST_PPI_IRQ + NR_PPI_IRQS)));
+}
+
 #endif /* _ASM_HW_IRQ_H */
 /*
  * Local variables:
diff --git a/xen/include/xen/device_tree.h b/xen/include/xen/device_tree.h
index 5a2a5c6..f51f451 100644
--- a/xen/include/xen/device_tree.h
+++ b/xen/include/xen/device_tree.h
@@ -114,6 +114,9 @@ struct dt_device_node {
     (DT_IRQ_TYPE_LEVEL_LOW | DT_IRQ_TYPE_LEVEL_HIGH)
 #define DT_IRQ_TYPE_SENSE_MASK     0x0000000f
 
+/* Cpu mask shift to the interrupt specifier (GIC specific) */
+#define DT_IRQ_TYPE_CPU_MASK_SHIFT      8
+
 /**
  * dt_irq - describe an IRQ in the device tree
  * @irq: IRQ number
