Index: trunk/kernel/devices/dev_pic.h
===================================================================
--- trunk/kernel/devices/dev_pic.h	(revision 205)
+++ trunk/kernel/devices/dev_pic.h	(revision 279)
@@ -34,11 +34,12 @@
  * to route a given IRQ to a given core, in a given cluster, and to help the interrupt
  * handler to select  and execute the relevant ISR (Interrupt Service Routine).
- * It handles the following type of interrupts:
- * - External IRQs generated by the external (shared) peripherals.
- * - Internal IRQs generated by the internal (replicated) peripherals.
- * - Timer IRQs generated by the timers (one timer per core).
- * - Inter Processor IRQs (IPI) generated by software.
- *
- * In most supported manycores architectures, the PIC device contains two types 
+ * It handles the four following types of interrupts:
+ *
+ * 1) EXT_IRQ (External IRQ) generated by the external (shared) peripherals.
+ * 2) INT_IRQ (Internal IRQ) generated by the internal (replicated) peripherals.
+ * 3) TIM_IRQ (Timer IRQ) generated by the timers (one timer per core).
+ * 4) IPI_IRQ (Inter Processor IRQ) generated by software (one IPI per core).
+ *
+ * In supported manycores architectures, the PIC device contains two types 
  * of hardware components: 
  * - the IOPIC is an external component, handling all external peripherals IRQs.
@@ -54,5 +55,5 @@
  * at kernel initialization.
  *
- * The PIC device defines 4 generic commands that can be used by each kernel instance,
+ * The PIC device defines generic commands that can be used by each kernel instance,
  * - to create in local cluster the PIC implementation specific interupt vector(s),
  * - to bind a given IRQ (internal or external IRQ to a given core in the local cluster,
@@ -64,5 +65,5 @@
  * cluster manager or to the core descriptors to register the interrupt vectors
  * used by the kernel to select the relevant ISR when an interrupt is received 
- * by a given core in agiven cluster.
+ * by a given core in a given cluster.
  
  * This PIC device does not execute itself I/O operations. It is just acting as a 
@@ -87,4 +88,5 @@
 typedef void   (disable_irq_t)  ( lid_t lid , xptr_t src_chdev_xp );   
 typedef void   (enable_timer_t) ( uint32_t period );   
+typedef void   (enable_ipi_t)   ( );   
 typedef void   (send_ipi_t)     ( cxy_t cxy , lid_t lid ); 
 typedef void   (extend_init_t)  ( uint32_t * lapic_base ); 
@@ -96,4 +98,5 @@
     disable_irq_t   * disable_irq;   /*! pointer on the driver "disable_irq" function   */ 
     enable_timer_t  * enable_timer;  /*! pointer on the driver "enable_timer" function  */
+    enable_timer_t  * enable_ipi;    /*! pointer on the driver "enable_ipi" function    */
     send_ipi_t      * send_ipi;      /*! pointer on the driver "send_ipi" function      */
     extend_init_t   * extend_init;   /*! pointer on the driver "init_extend" function   */
@@ -186,5 +189,5 @@
 
 /*****************************************************************************************
- * This function enables remote IRQ generated by a remote chdev, defined by the 
+ * This function enables the IRQ generated by a remote chdev, defined by the 
  * <src_chdev_xp> argument. It can be called by any thread running in any cluster,
  * and can be used for both internal & external IRQs.
@@ -199,5 +202,5 @@
  * This function disables remote IRQ generated by a remote chdev, defined by the 
  * <src_chdev_xp> argument. It can be called by any thread running in any cluster,
- * and can be used for both internal & external IRQs.
+ * and can be used for both INT_IRq & EXT_IRQ.
  *****************************************************************************************
  * @ lid           : target core local index (in cluster containing the source chdev).
@@ -208,10 +211,15 @@
 
 /*****************************************************************************************
- * This function activates the TICK timer for the calling core.
- * The <period> argument define the number of cycles between IRQs.
+ * This function activates the TIM_IRQ for the calling core.
+ * The <period> argument define the number of cycles between twoo successive IRQs.
  *****************************************************************************************
  * @ period      : number of cycles between IRQs.
  ****************************************************************************************/
 void dev_pic_enable_timer( uint32_t period );
+
+/*****************************************************************************************
+ * This function activates the IPI_IRQ for the calling core.
+ ****************************************************************************************/
+void dev_pic_enable_ipi();
 
 /*****************************************************************************************
