Index: /soft/giet_vm/giet_kernel/ctx_handler.c
===================================================================
--- /soft/giet_vm/giet_kernel/ctx_handler.c	(revision 527)
+++ /soft/giet_vm/giet_kernel/ctx_handler.c	(revision 528)
@@ -8,10 +8,49 @@
 #include <ctx_handler.h>
 #include <giet_config.h>
+#include <hard_config.h>
 #include <utils.h>
 #include <tty0.h>
 #include <xcu_driver.h>
 
-////////// defined in giet_kernel/switch.s file /////////
+/////////////////////////////////////////////////////////////////////////////////
+//     Extern variables and functions
+/////////////////////////////////////////////////////////////////////////////////
+
+// defined in giet_kernel/switch.s file
 extern void _task_switch(unsigned int *, unsigned int *);
+
+// allocated in boot.c or kernel_init.c files
+extern static_scheduler_t* _schedulers[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+
+//////////////////////////////////
+void _ctx_display( unsigned int x,
+                   unsigned int y,
+                   unsigned int p,
+                   unsigned int ltid,
+                   char*        string )
+{
+    static_scheduler_t* psched = _schedulers[x][y][p];
+    _printf("\n########## task[%d,%d,%d,%d] context\n"
+            " - CTX_EPC   = %x\n"
+            " - CTX_PTAB  = %x\n"
+            " - CTX_PTPR  = %x\n"
+            " - CTX_VSID  = %x\n"
+            " - CTX_SR    = %x\n"
+            " - CTX_RA    = %x\n"
+            " - CTX_SP    = %x\n"
+            " - CTX_RUN   = %x\n"
+            "########## %s\n",
+            x , y , p , ltid ,
+            psched->context[ltid][CTX_EPC_ID], 
+            psched->context[ltid][CTX_PTAB_ID], 
+            psched->context[ltid][CTX_PTPR_ID], 
+            psched->context[ltid][CTX_VSID_ID], 
+            psched->context[ltid][CTX_SR_ID], 
+            psched->context[ltid][CTX_RA_ID], 
+            psched->context[ltid][CTX_SP_ID], 
+            psched->context[ltid][CTX_RUN_ID],
+            string );
+}  // _ctx_display()
+
 
 //////////////////
@@ -48,14 +87,10 @@
 
     // launch "idle" task if no runable task
-    if (found == 0) 
-    {
-        next_task_id = IDLE_TASK_INDEX;
-    }
+    if (found == 0) next_task_id = IDLE_TASK_INDEX;
 
 #if GIET_DEBUG_SWITCH
 unsigned int x = cluster_xy >> Y_WIDTH;
 unsigned int y = cluster_xy & ((1<<Y_WIDTH)-1);
-
-_printf("\n[TASK SWITCH] (%d) -> (%d) on processor[%d,%d,%d] at cycle %d\n",
+_printf("\n[DEBUG SWITCH] (%d) -> (%d) on processor[%d,%d,%d] at cycle %d\n",
         curr_task_id, next_task_id, x, y , lpid, _get_proctime() );
 #endif
@@ -66,13 +101,6 @@
         unsigned int* next_ctx_vaddr = &(psched->context[next_task_id][0]);
 
-        // reset timer counter. 
-        // In all clusters, the first NB_PROCS_MAX
-        // timers are system timers (TICK)
-
-#if USE_XCU
+        // reset TICK timer counter. 
         _xcu_timer_reset_cpt( cluster_xy, lpid );
-#else
-        _timer_reset_cpt( cluster_xy, lpid); 
-#endif
 
         // set current task index 
@@ -80,7 +108,9 @@
 
         // makes context switch
-        _task_switch(curr_ctx_vaddr, next_ctx_vaddr);
+        _task_switch( curr_ctx_vaddr , next_ctx_vaddr );
+
     }
 } //end _ctx_switch()
+
 
 /////////////////
@@ -110,13 +140,6 @@
 
         // warning message
-        _puts("\n[GIET WARNING] Processor[");
-        _putd( x );
-        _puts(",");
-        _putd( y );
-        _puts(",");
-        _putd( p );
-        _puts("] still idle at cycle ");
-        _putd( _get_proctime() );
-        _puts("\n");
+        _printf("\n[GIET WARNING] Processor[%d,%d,%d] still idle at cycle %d",
+                x , y , p , _get_proctime() );
     }
 } // end ctx_idle()
Index: /soft/giet_vm/giet_kernel/ctx_handler.h
===================================================================
--- /soft/giet_vm/giet_kernel/ctx_handler.h	(revision 527)
+++ /soft/giet_vm/giet_kernel/ctx_handler.h	(revision 528)
@@ -1,8 +1,8 @@
-/////////////////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////////////////////////////////////////////////////
 // File     : ctx_handler.h
 // Date     : 01/04/2012
 // Authors  : alain greiner & joel porquet
 // Copyright (c) UPMC-LIP6
-/////////////////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////////////////////////////////////////////////////
 // The ctx_handler.h and ctx_handler.c files are part of the GIET-VM nano-kernel.
 // This code is used to support context switch when several tasks are executing
@@ -13,10 +13,10 @@
 // The task context [13] is reserved for the "idle" task that does nothing, and
 // is launched by the scheduler when there is no other runable task.
-/////////////////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////////////////////////////////////////////////////
 // A task context is an array of 64 words = 256 bytes. 
 // It contains copies of processor registers (when the task is preempted)
 // and some general informations associated to a task, such as the peripherals
-// allocated to the task (private peripheral channel for multi-channels peripherals).
-/////////////////////////////////////////////////////////////////////////////////////////
+// allocated to the task (private peripheral channel)
+/////////////////////////////////////////////////////////////////////////////////
 // ctx[0] <- ***   |ctx[8] <- $8     |ctx[16]<- $16   |ctx[24]<- $24
 // ctx[1] <- $1    |ctx[9] <- $9     |ctx[17]<- $17   |ctx[25]<- $25
@@ -36,5 +36,5 @@
 // ctx[38]<- VSID  |ctx[46]<- TIM    |ctx[54]<- ***   |ctx[62]<- ***
 // ctx[39]<- PTPR  |ctx[47]<- HBA    |ctx[55]<- ***   |ctx[63]<- ***
-/////////////////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////////////////////////////////////////////////////
 
 #ifndef _CTX_HANDLER_H
@@ -94,10 +94,5 @@
 
 /////////////////////////////////////////////////////////////////////////////////
-//                 Schedulers array
-/////////////////////////////////////////////////////////////////////////////////
-extern static_scheduler_t _scheduler[];
-
-/////////////////////////////////////////////////////////////////////////////////
-//               External Functions
+//               Extern Functions
 /////////////////////////////////////////////////////////////////////////////////
 
@@ -126,4 +121,14 @@
 extern void _idle_task();
 
+/////////////////////////////////////////////////////////////////////////////////
+// This function displays the context of a task identified by the processor
+// coordinates (x,y,p), and by the local task index ltid.
+// The string argument can be used for debug.
+/////////////////////////////////////////////////////////////////////////////////
+extern void _ctx_display( unsigned int x,
+                          unsigned int y,
+                          unsigned int p,
+                          unsigned int ltid,
+                          char*        string );
 
 #endif
Index: /soft/giet_vm/giet_kernel/exc_handler.c
===================================================================
--- /soft/giet_vm/giet_kernel/exc_handler.c	(revision 527)
+++ /soft/giet_vm/giet_kernel/exc_handler.c	(revision 528)
@@ -76,4 +76,5 @@
     unsigned int task       = _get_context_slot(CTX_LTID_ID);
 
+
     _printf("\n[GIET] Exception for task %d on processor[%d,%d,%d] at cycle %d\n"
             " - type      : %s\n"
@@ -87,7 +88,10 @@
     _set_context_slot(CTX_RUN_ID, 0);
 
-    // deschedule
+    // deschedule (suicide)
+    unsigned int save_sr;  // unused 
+    _it_disable( &save_sr );
     _ctx_switch();
-}
+
+}  // end display_cause()
 
 static void _cause_ukn()  { _display_cause(0); }
Index: /soft/giet_vm/giet_kernel/irq_handler.c
===================================================================
--- /soft/giet_vm/giet_kernel/irq_handler.c	(revision 527)
+++ /soft/giet_vm/giet_kernel/irq_handler.c	(revision 528)
@@ -1,8 +1,8 @@
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
 // File     : irq_handler.c
 // Date     : 01/04/2012
 // Author   : alain greiner 
 // Copyright (c) UPMC-LIP6
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
 
 #include <giet_config.h>
@@ -12,4 +12,5 @@
 #include <tim_driver.h>
 #include <xcu_driver.h>
+#include <pic_driver.h>
 #include <tty_driver.h>
 #include <nic_driver.h>
@@ -19,11 +20,30 @@
 #include <dma_driver.h>
 #include <spi_driver.h>
+#include <mwr_driver.h>
 #include <mapping_info.h>
 #include <utils.h>
 #include <tty0.h>
 
-#if NB_TIM_CHANNELS
-extern volatile unsigned char _user_timer_event[NB_TIM_CHANNELS] ;
-#endif
+/////////////////////////////////////////////////////////////////////////
+//       Global variables 
+/////////////////////////////////////////////////////////////////////////
+
+// array of external IRQ indexes for each (isr/channel) couple 
+__attribute__((section(".kdata")))
+unsigned char _ext_irq_index[GIET_ISR_TYPE_MAX][GIET_ISR_CHANNEL_MAX];
+
+// WTI mailbox allocators for external IRQ routing (3 allocators per proc)
+__attribute__((section(".kdata")))
+unsigned char _wti_alloc_one[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+__attribute__((section(".kdata")))
+unsigned char _wti_alloc_two[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+__attribute__((section(".kdata")))
+unsigned char _wti_alloc_ter[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+
+/////////////////////////////////////////////////////////////////////////
+// this array is allocated in the boot.c or kernel_init.c
+/////////////////////////////////////////////////////////////////////////
+
+extern static_scheduler_t* _schedulers[X_SIZE][Y_SIZE][NB_PROCS_MAX]; 
 
 /////////////////////////////////////////////////////////////////////////
@@ -45,5 +65,169 @@
                            "DMA"    ,
                            "SPI"    ,
-                           "MWR"    };
+                           "MWR"    ,
+                           "HBA"    };
+
+////////////////////
+void _ext_irq_init()
+{
+    mapping_header_t*    header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
+    mapping_cluster_t*   cluster = _get_cluster_base(header);
+    mapping_periph_t*    periph  = _get_periph_base(header);
+    mapping_irq_t*       irq     = _get_irq_base(header);
+    unsigned int         periph_id;   // peripheral index in mapping_info
+    unsigned int         irq_id;      // irq index in mapping_info
+
+    // get cluster_io index in mapping
+    unsigned int         x_io       = header->x_io;  
+    unsigned int         y_io       = header->y_io;  
+    unsigned int         cluster_io = (x_io * Y_SIZE) + y_io; 
+    mapping_periph_t*    pic        = NULL;
+
+    // scan external peripherals to find XCU
+    unsigned int min = cluster[cluster_io].periph_offset ;
+    unsigned int max = min + cluster[cluster_io].periphs ;
+    
+    for ( periph_id = min ; periph_id < max ; periph_id++ )
+    {
+        if ( periph[periph_id].type == PERIPH_TYPE_PIC ) 
+        {
+            pic = &periph[periph_id];
+            break;
+        }
+    }  
+
+    if ( pic == NULL )
+    {
+        _printf("\n[GIET ERROR] in _ext_irq_init() : No PIC component found\n");
+        _exit();
+    }
+
+    // scan PIC IRQS defined in mapping
+    for ( irq_id = pic->irq_offset ;
+          irq_id < pic->irq_offset + pic->irqs ;
+          irq_id++ )
+    {
+        unsigned int type    = irq[irq_id].srctype;
+        unsigned int srcid   = irq[irq_id].srcid;
+        unsigned int isr     = irq[irq_id].isr;
+        unsigned int channel = irq[irq_id].channel;
+
+        if ( (type != IRQ_TYPE_HWI)            || 
+             (srcid > 31)                      || 
+             (isr >= GIET_ISR_TYPE_MAX)        ||
+             (channel >= GIET_ISR_CHANNEL_MAX) )
+        {
+            _printf("\n[GIET ERROR] in _ext_irq_init() : Bad PIC IRQ\n"
+                    "  type = %d / srcid = %d / isr = %d / channel = %d\n",
+                    type , srcid , isr , channel );
+            _exit();
+        }
+        _ext_irq_index[isr][channel] = srcid;
+    }
+}  // end _ext_irq_init()
+
+////////////////////////////////////////////
+void _ext_irq_alloc( unsigned int   isr_type,
+                     unsigned int   isr_channel,
+                     unsigned int*  wti_index )
+{
+    unsigned int wti_id;        // allocated WTI mailbox index in XCU
+    unsigned int irq_id;        // external IRQ index in PIC (input)
+    unsigned int wti_addr;      // WTI mailbox physical address (32 lsb bits)
+
+    // check arguments
+    if ( isr_type >= GIET_ISR_TYPE_MAX )
+    {
+        _printf("\n[GIET ERROR] in _ext_irq_alloc() : illegal ISR type\n");
+        _exit();
+    }
+    if ( isr_channel >= GIET_ISR_CHANNEL_MAX )
+    {
+        _printf("\n[GIET ERROR] in _ext_irq_alloc() : illegal ISR channel\n");
+        _exit();
+    }
+
+    // get processor coordinates [x,y,p]
+    unsigned int gpid           = _get_procid();
+    unsigned int cluster_xy     = gpid >> P_WIDTH;
+    unsigned int x              = cluster_xy >> Y_WIDTH;
+    unsigned int y              = cluster_xy & ((1<<Y_WIDTH)-1);
+    unsigned int p              = gpid & ((1<<P_WIDTH)-1);
+
+    // allocate a WTI mailbox to proc[x,y,p] (blocking until success)
+    while ( 1 )
+    {
+        if ( _wti_alloc_one[x][y][p] == 0 )
+        {
+            _wti_alloc_one[x][y][p] = 1;
+            wti_id = p + NB_PROCS_MAX;
+            break;
+        }
+        if ( _wti_alloc_two[x][y][p] == 0 )
+        {
+            _wti_alloc_two[x][y][p] = 1;
+            wti_id = p + 2*NB_PROCS_MAX;
+            break;
+        }
+        if ( _wti_alloc_ter[x][y][p] == 0 )
+        {
+            _wti_alloc_ter[x][y][p] = 1;
+            wti_id = p + 3*NB_PROCS_MAX;
+            break;
+        }
+    }    
+    *wti_index = wti_id;
+
+    // register the mailbox physical address in IOPIC
+    irq_id   = _ext_irq_index[isr_type][isr_channel];
+    _xcu_get_wti_address( wti_id , &wti_addr );
+    _pic_init( irq_id , wti_addr, cluster_xy );
+    
+    // initializes the WTI interrupt vector entry for XCU
+    _schedulers[x][y][p]->wti_vector[wti_id] = isr_channel<<16 | isr_type;
+
+}  // end ext_irq_alloc()
+
+////////////////////////////////////////////
+void _ext_irq_release( unsigned int isr_type,
+                       unsigned int isr_channel,
+                       unsigned int wti_index )
+{
+    unsigned int irq_id;        // external IRQ index in PIC (input)
+
+    // get processor coordinates [x,y,p]
+    unsigned int gpid           = _get_procid();
+    unsigned int cluster_xy     = gpid >> P_WIDTH;
+    unsigned int x              = cluster_xy >> Y_WIDTH;
+    unsigned int y              = cluster_xy & ((1<<Y_WIDTH)-1);
+    unsigned int p              = gpid & ((1<<P_WIDTH)-1);
+
+    // check arguments
+    if ( isr_type >= GIET_ISR_TYPE_MAX )
+    {
+        _printf("\n[GIET ERROR] in _ext_irq_release() illegal ISR type\n");
+        _exit();
+    }
+    if ( isr_channel >= GIET_ISR_CHANNEL_MAX )
+    {
+        _printf("\n[GIET ERROR] in _ext_irq_release() : illegal ISR channel\n");
+        _exit();
+    }
+
+    // desactivates dynamically allocated PIC entry
+    irq_id = _ext_irq_index[isr_type][isr_channel];
+    _pic_set_register( irq_id , IOPIC_MASK , 0 );
+
+    // releases dynamically allocated WTI mailbox
+    if      ( wti_index == p +   NB_PROCS_MAX ) _wti_alloc_one[x][y][p] = 0;
+    else if ( wti_index == p + 2*NB_PROCS_MAX ) _wti_alloc_two[x][y][p] = 0;
+    else if ( wti_index == p + 3*NB_PROCS_MAX ) _wti_alloc_ter[x][y][p] = 0;
+    else
+    {
+        _printf("\n[GIET ERROR] in _ext_irq_release() : illegal WTI index\n");
+        _exit();
+    }
+}  // end ext_irq_release()
+
 /////////////////
 void _irq_demux() 
@@ -156,20 +340,16 @@
     unsigned int x          = cluster_xy >> Y_WIDTH;
     unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
-    unsigned int lpid       = gpid & ((1<<P_WIDTH)-1);
-
-    unsigned int task       = _get_current_task_id();
-    unsigned int value;
+    unsigned int p          = gpid & ((1<<P_WIDTH)-1);
+
+    unsigned int value;     // WTI mailbox value
+    unsigned int save_sr;   // save SR value in pre-empted task stack
+
+    unsigned int ltid       = _get_current_task_id();
 
     if ( irq_type != IRQ_TYPE_WTI )
     {
-        _puts("[GIET ERROR] _isr_wakup() not called by a WTI on processor[");
-        _putd( x );
-        _puts(",");
-        _putd( y );
-        _puts(",");
-        _putd( lpid );
-        _puts("] at cycle ");
-        _putd( _get_proctime() );
-        _puts("\n");
+        _printf("[GIET ERROR] P[%d,%d,%d] enters _isr_wakup() at cycle %d\n"
+                " but not called by a WTI interrupt\n",
+                x , y , p , _get_proctime() );
         _exit();
     }
@@ -178,22 +358,18 @@
     _xcu_get_wti_value( cluster_xy, irq_id, &value );
 
-#if GIET_DEBUG_IRQS // we don't take the TTY lock to avoid deadlocks
-_puts("\n[IRQS DEBUG] Processor[");
-_putd( x );
-_puts(",");
-_putd( y );
-_puts(",");
-_putd( lpid );
-_puts("] enters _isr_wakup() at cycle ");
-_putd( _get_proctime() );
-_puts("\n  WTI / mailbox data = ");
-_putx( value );
-_puts(" / current task index = ");
-_putd( task );
-_puts("\n  ");
+#if GIET_DEBUG_SWITCH
+_printf("\n[DEBUG SWITCH] P[%d,%d,%d] enters _isr_wakup() at cycle %d\n"
+        "  WTI index = %d / current ltid = %d / mailbox value = %x\n",
+        x , y , p , _get_proctime() , irq_id , ltid , value );
 #endif
 
-    // context swich if required
-    if ( (task == IDLE_TASK_INDEX) || (value != 0) ) _ctx_switch();
+    // enter critical section and swich context (if required)
+    if ( (ltid == IDLE_TASK_INDEX) || (value != 0) )
+    {
+        _it_disable( &save_sr );
+        _ctx_switch();
+        _it_restore( &save_sr );
+    }
+
 } // end _isr_wakup
 
@@ -207,17 +383,13 @@
     unsigned int x          = cluster_xy >> Y_WIDTH;
     unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
-    unsigned int lpid       = gpid & ((1<<P_WIDTH)-1);
+    unsigned int p          = gpid & ((1<<P_WIDTH)-1);
+
+    unsigned int save_sr;   // save SR value in pre-empted task stack
 
     if ( irq_type != IRQ_TYPE_PTI )
     {
-        _puts("[GIET ERROR] _isr_tick() not called by a PTI on processor[");
-        _putd( x );
-        _puts(",");
-        _putd( y );
-        _puts(",");
-        _putd( lpid );
-        _puts("] at cycle ");
-        _putd( _get_proctime() );
-        _puts("\n");
+        _printf("[GIET ERROR] P[%d,%d,%d] enters _isr_tick() at cycle %d\n"
+                " but not called by a PTI interrupt\n",
+                x , y , p , _get_proctime() );
         _exit();
     }
@@ -226,18 +398,16 @@
     _xcu_timer_reset_irq( cluster_xy, irq_id );
 
-#if GIET_DEBUG_IRQS  // we don't take the TTY lock to avoid deadlock
-_puts("\n[IRQS DEBUG] Processor[");
-_putd( x );
-_puts(",");
-_putd( y );
-_puts(",");
-_putd( lpid );
-_puts("] enters _isr_tick() at cycle ");
-_putd( _get_proctime() );
-_puts("\n  ");
+#if GIET_DEBUG_SWITCH
+unsigned int ltid  = _get_current_task_id();
+_printf("\n[DEBUG SWITCH] P[%d,%d,%d] enters _isr_tick() at cycle %d\n"
+        "  WTI index = %d / current ltid = %d\n",
+        x , y , p , _get_proctime() , irq_id , ltid );
 #endif
 
-    // context switch
+    // enter critical section and switch context 
+    _it_disable( &save_sr );
     _ctx_switch();
+    _it_restore( &save_sr );
+
 }  // end _isr_tick
 
Index: /soft/giet_vm/giet_kernel/irq_handler.h
===================================================================
--- /soft/giet_vm/giet_kernel/irq_handler.h	(revision 527)
+++ /soft/giet_vm/giet_kernel/irq_handler.h	(revision 528)
@@ -1,21 +1,19 @@
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
 // File     : irq_handler.h
 // Date     : 01/04/2012
 // Author   : alain greiner 
 // Copyright (c) UPMC-LIP6
-///////////////////////////////////////////////////////////////////////////////////
-// The irq_handler.c and irq_handler.h files are part of the GIET-VM nano-kernel.
-// They contain the code of the _irq_demux() function that access the XICU or
-// ICU component (Interupt Controler Unit), and the various ISRs (Interrupt
-// Service Routine) associated to the various ISR types.
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
+// The irq_handler.c and irq_handler.h files are part of the GIET-VM.
+// They contain the code of used to handlle HWI, WTI, PTI interrupts.
+///////////////////////////////////////////////////////////////////////////
 
 #ifndef _IRQ_HANDLER_H
 #define _IRQ_HANDLER_H
 
-////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
 // This enum must consistent with the values defined in 
-// xml_driver.c / irq_handler.c / mapping.py 
-///////////////////////////////////////////////////////////////////////////////
+// xml_driver.c / xml_parser.c / irq_handler.c / mapping.py 
+///////////////////////////////////////////////////////////////////////////
 
 enum isr_type_t
@@ -35,40 +33,95 @@
     ISR_SPI     = 12,
     ISR_MWR     = 13,
+    ISR_HBA     = 14,
 };
 
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
+//    Global variables allocated in irq_handler.c     
+///////////////////////////////////////////////////////////////////////////
+
+// array of external IRQ indexes for each (isr/channel) couple 
+extern unsigned char _ext_irq_index[GIET_ISR_TYPE_MAX][GIET_ISR_CHANNEL_MAX];
+
+// WTI mailbox allocators for external IRQ routing (3 allocators per proc)
+extern unsigned char _wti_alloc_one[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+extern unsigned char _wti_alloc_two[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+extern unsigned char _wti_alloc_ter[X_SIZE][Y_SIZE][NB_PROCS_MAX];
+
+///////////////////////////////////////////////////////////////////////////
 //    irq_handler functions
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
 
-///////////////////////////////////////////////////////////////////////////////////
-// This function access the ICU or XICU component (Interrupt Controler Unit)
-// to get the interrupt vector entry. There is one ICU or XICU component per
+///////////////////////////////////////////////////////////////////////////
+// This function is only used when the architecture contains an external
+// IOPIC component. It initializes the _ext_irq_index[isr][channel] array,
+// defining the IRQ index associated to (isr_type/isr_channel) couple.
+// This array is used by the kernel for dynamic routing of an external IRQ
+// signaling completion to  the processor that launched the I/O operation.
+///////////////////////////////////////////////////////////////////////////
+
+extern void _ext_irq_init();
+
+///////////////////////////////////////////////////////////////////////////
+// This function is only used when the architecture contains an external
+// IOPIC component. It dynamically routes an external IRQ signaling 
+// completion of an I/O operation to the processor P[x,y,p] running
+// the calling task.
+// 1) it allocates a WTI mailbox in the XCU of cluster[x,y] : Each processor
+//    has 3  mailboxes, with index in [4*p+1, 4*p+2, 4*p+3].
+// 2) it initialises the IOPIC_ADDRESS and IOPIC_MASK registers associated
+//    to the (isr_type/isr_channel) couple.
+// 3) it initializes the proper entry in the WTI interrupt vector associated 
+//    to processor P[x,y,p].
+///////////////////////////////////////////////////////////////////////////
+
+extern void _ext_irq_alloc( unsigned int   isr_type,
+                            unsigned int   isr_channel,
+                            unsigned int*  wti_index );
+                             
+///////////////////////////////////////////////////////////////////////////
+// This function is only used when the architecture contains an external
+// IOPIC component. It desallocates all ressources allocated by the 
+// previous _ext_irq_alloc() function to the calling processor.
+// 1)  it desactivates the PIC entry associated to (isr_type/isr_channel).
+// 2) it releases the WTI mailbox in the XCU of cluster[x,y].
+///////////////////////////////////////////////////////////////////////////
+
+extern void _ext_irq_release( unsigned int isr_type,
+                              unsigned int isr_channel,
+                              unsigned int wti_index );
+
+///////////////////////////////////////////////////////////////////////////
+// This function access the XICU component (Interrupt Controler Unit)
+// to get the interrupt vector entry. There is one XICU component per
 // cluster, and this component can support up to NB_PROCS_MAX output IRQs.
 // It returns the highest priority active interrupt index (smaller
 // indexes have the highest priority).
-// Any value larger than 31 means "no active interrupt", and no ISR is executed.
+// Any value larger than 31 means "no active interrupt".
 //
 // There is three interrupt vectors per processor (stored in the processor's
 // scheduler) for the three HWI, PTI, and WTI interrupts types.
-// Each interrupt vector entry contains three bits fields:
-// - isr_id     bits[15:0]  : defines the type of ISR to be executed.
-// - channel_id bits[30:16] : defines the channel for multi-channels peripherals.
-// - valid      bit 31      : valid interrupt vector entry
+// Each interrupt vector entry contains two fields:
+// - isr_type     bits[15:0]  : defines the type of ISR to be executed.
+// - isr_channel  bits[31:16] : defines the channel index 
 // If the peripheral is replicated in clusters, the channel_id is 
 // a global index : channel_id = cluster_id * NB_CHANNELS_MAX + loc_id   
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
+
 extern void _irq_demux();
 
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
 // This default ISR is called  when the interrupt handler is called, 
-// and there is no active IRQ. It simply displays a warning message on TTY[0].
-///////////////////////////////////////////////////////////////////////////////////
+// and there is no active IRQ. It displays a warning message on TTY[0].
+///////////////////////////////////////////////////////////////////////////
+
 extern void _isr_default();
 
-///////////////////////////////////////////////////////////////////////////////////
-// This ISR can only be executed after a WTI (IPI) to force a context switch
-// on a remote processor. The context switch is only executed if the current task
-// is the IDLE_TASK, or if the value written in the mailbox is non zero.
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////
+// This ISR can only be executed after a WTI to force a context switch
+// on a remote processor. The context switch is only executed if the 
+// current task is the IDLE_TASK, or if the value written in the mailbox 
+// is non zero.
+///////////////////////////////////////////////////////////////////////////
+
 extern void _isr_wakup( unsigned int irq_type,
                         unsigned int irq_id,
Index: /soft/giet_vm/giet_kernel/kernel_init.c
===================================================================
--- /soft/giet_vm/giet_kernel/kernel_init.c	(revision 527)
+++ /soft/giet_vm/giet_kernel/kernel_init.c	(revision 528)
@@ -11,4 +11,5 @@
 #include <hard_config.h>
 #include <utils.h>
+#include <vmem.h>
 #include <tty0.h>
 #include <kernel_malloc.h>
@@ -52,4 +53,8 @@
 #endif
 
+#if !defined(USE_PIC) 
+# error: You must define USE_PIC in the hard_config.h file
+#endif
+
 #if !defined(IDLE_TASK_INDEX) 
 # error: You must define IDLE_TASK_INDEX in the ctx_handler.h file
@@ -72,25 +77,32 @@
 #endif
 
-
-
-// Distributed kernel heap descriptors array
-// __attribute__((section(".kdata")))
-// kernel_heap_t  kernel_heap[X_SIZE][Y_SIZE];
+#if !defined(GIET_ISR_TYPE_MAX)
+# error: You must define GIET_ISR_TYPE_MAX in the giet_config.h file
+#endif
+
+#if !defined(GIET_ISR_CHANNEL_MAX)
+# error: You must define GIET_ISR_CHANNEL_MAX in the giet_config.h file
+#endif
+
+
+////////////////////////////////////////////////////////////////////////////////
+//       Global variables
+////////////////////////////////////////////////////////////////////////////////
 
 // FAT internal representation for kernel code
 __attribute__((section(".kdata")))
-fat32_fs_t     fat      __attribute__((aligned(512)));
+fat32_fs_t     _fat      __attribute__((aligned(512)));
 
 // array of page tables virtual addresses
 __attribute__((section(".kdata")))
-volatile unsigned int _ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
+volatile unsigned int _ptabs_vaddr[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE]; 
 
 // array of page tables PTPR values (physical addresses >> 13)
 __attribute__((section(".kdata")))
-volatile unsigned int _ptabs_ptprs[GIET_NB_VSPACE_MAX]; 
+volatile unsigned int _ptabs_ptprs[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE]; 
 
 // Array of pointers on the schedulers
 __attribute__((section(".kdata")))
-volatile static_scheduler_t*    _schedulers[X_SIZE][Y_SIZE][NB_PROCS_MAX]; 
+volatile static_scheduler_t* _schedulers[X_SIZE][Y_SIZE][NB_PROCS_MAX]; 
 
 // Synchonisation before entering parallel execution
@@ -102,31 +114,29 @@
 unsigned int   _tty0_boot_mode = 0;
 
-// Distributed synchronisation barrier for parallel init by all processors      
+// synchronisation barrier for parallel init by all processors      
 __attribute__((section(".kdata")))
 sqt_barrier_t  _all_procs_barrier  __attribute__((aligned(64)));
 
-
+////////////////////////////////////////////////////////////////////////////////
+//      Extern variables
+////////////////////////////////////////////////////////////////////////////////
 
 // this variable is defined in tty0.c file
 extern sqt_lock_t _tty0_sqt_lock;
 
-
-
-///////////////////////////////////////////////////////////////////////////////////
-// This kernel_init() function completes the kernel initialisation in 7 steps.
-// Step 0 is done by processor[0,0,0]. Steps 1 to 6 are executed in parallel
-// by all procesors.
-// - step 0 : P[0,0,0] Initialise fat, heap descriptors, barrier and TTY0 lock.
+////////////////////////////////////////////////////////////////////////////////
+// This kernel_init() function completes the kernel initialisation in 6 steps:
+// Step 0 is done by processor[0,0,0]. Steps 1 to 4 are executed in parallel
+// by all processors.
+// - step 0 : P[0,0,0] Initialise various global variables.
 // - step 1 : Each processor initialises scheduler pointers array.
 // - step 2 : Each processor initialises PTAB pointers arrays.
-// - step 3 : Each processor initialises its private XCU masks.
-// - step 4 : Each processor starts its private TICK timer.
-// - step 5 : Each processor initialises its private idle task context.
-// - step 6 : Each processor set sp, sr, ptpr, epc registers values. 
-///////////////////////////////////////////////////////////////////////////////////
+// - step 3 : Each processor initialise idle task and starts TICK timer.
+// - step 4 : Each processor set sp, sr, ptpr, epc registers values. 
+////////////////////////////////////////////////////////////////////////////////
 __attribute__((section (".kinit"))) void kernel_init() 
 {
     // gpid  : hardware processor index (fixed format: X_WIDTH|Y_WIDTH|P_WIDTH)
-    // x,y,p : processor coordinates ( x<X_SIZE / y<Y_SIZE / p<NB_PROCS_MAX )
+    // x,y,p : proc coordinates ( x < X_SIZE / y < Y_SIZE / p < NB_PROCS_MAX )
 
     unsigned int gpid       = _get_procid();
@@ -137,19 +147,15 @@
 
     ////////////////////////////////////////////////////////////////////////////
-    // Step 0 : P[0,0,0] initialises various structures
+    // Step 0 : P[0,0,0] initialises various global vaiables
+    ////////////////////////////////////////////////////////////////////////////
 
     if ( gpid == 0 )
     {
-        // distributed kernel heaps
+        // distributed kernel heap initialisation
         _heap_init();
         
 #if GIET_DEBUG_INIT
-_nolock_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] completes kernel HEAP init\n", x, y, p );
-#endif
-        // kernel FAT 
-        _fat_init( IOC_BOOT_MODE ); 
-
-#if GIET_DEBUG_INIT
-_nolock_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] completes kernel FAT init\n", x, y, p );
+_nolock_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] completes kernel HEAP init\n",
+               x, y, p );
 #endif
         // distributed lock for TTY0
@@ -167,4 +173,20 @@
                x , y , p );
 #endif
+
+#if USE_PIC
+
+        // _ext_irq_index[isr][channel] initialisation
+        _ext_irq_init();
+
+        // routing HBA IRQ to proc[0,0,0] EXT_IRQ_ONE
+        unsigned int unused = 0;
+        if ( USE_IOC_HBA ) _ext_irq_alloc( ISR_HBA , 0 , &unused );
+
+#if GIET_DEBUG_INIT
+_nolock_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] completes ext_irq init\n", 
+               x , y , p );
+#endif
+
+#endif // USE_PIC
 
         // release other processors
@@ -176,8 +198,9 @@
     }
 
-    ///////////////////////////////////////////////////////////////////
+    ///////////////////////////////////////////////////////////////////////////
     // Step 1 : each processor get its scheduler vaddr from CP0_SCHED, 
     //          contributes to _schedulers[] array initialisation,
     //          and wait completion of array initialisation.
+    ///////////////////////////////////////////////////////////////////////////
 
     static_scheduler_t* psched     = (static_scheduler_t*)_get_sched();
@@ -193,14 +216,18 @@
 #endif
 
+    /////////////////////////////////////////
     _sqt_barrier_wait( &_all_procs_barrier );    
+    /////////////////////////////////////////
 
     ////////////////////////////////////////////////////////////////////////////
     // step 2 : each processor that is allocated at least one task loops 
-    //          on all allocated tasks: 
-    //          - contributes to _ptabs_vaddr[] & _ptabs_ptprs[] initialisation.
+    //          on its allocated tasks: 
+    //          - contributes to _ptabs_vaddr[][][] & _ptabs_ptprs[][][]
+    //            initialisation, from values stored in the tasks contexts.
     //          - set CTX_RA slot  with the kernel _ctx_eret() virtual address.
     //          - set CTX_EPC slot that must contain the task entry point, 
-    //            and contain only at this point the virtual address of the memory 
-    //            location containing this entry point. 
+    //            and contain only at this point the virtual address of the 
+    //            memory slot containing this entry point. 
+    ////////////////////////////////////////////////////////////////////////////
 
     unsigned int ltid;
@@ -213,16 +240,9 @@
 
         // initialize PTABS arrays
-        _ptabs_vaddr[vsid] = ptab;
-        _ptabs_ptprs[vsid] = ptpr;
-
-#if GIET_DEBUG_INIT
-_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] initialises PTABS arrays\n"
-        " - ptabs_vaddr[%d] = %x / ptpr_paddr[%d] = %l\n",
-        x, y, p,  
-        vsid, ptab, vsid, ((unsigned long long)ptpr)<<13 );
-#endif
-
-        // set the ptpr to use the task page table
-        asm volatile( "mtc2    %0,   $0   \n"
+        _ptabs_vaddr[vsid][x][y] = ptab;
+        _ptabs_ptprs[vsid][x][y] = ptpr;
+
+        // set the ptpr to use the local page table
+        asm volatile( "mtc2    %0,   $0"
                       : : "r" (ptpr) );
 
@@ -232,12 +252,17 @@
 
         // compute ctx_epc
-        unsigned int* ptr = (unsigned int*)_get_task_slot( x, y, p, ltid, CTX_EPC_ID );
-        _set_task_slot( x, y, p, ltid, CTX_EPC_ID, *ptr );
-
-#if GIET_DEBUG_INIT
-_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] updates context for task %d\n"
-        " - ctx_epc   = %x\n"
-        " - ctx_ra    = %x\n",
-        x, y, p, ltid,
+        unsigned int* ptr = (unsigned int*)_get_task_slot(x,y,p,ltid,CTX_EPC_ID);
+        _set_task_slot(x,y,p,ltid,CTX_EPC_ID,*ptr);
+
+#if GIET_DEBUG_INIT
+_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] initialises PTABS arrays"
+        " and context for task %d \n"
+        " - ptabs_vaddr[%d][%d][%d] = %x\n"
+        " - ptabs_paddr[%d][%d][%d] = %l\n"
+        " - ctx_epc              = %x\n"
+        " - ctx_ra               = %x\n",
+        x , y , p , ltid ,  
+        vsid , x , y , ptab ,
+        vsid , x , y , ((unsigned long long)ptpr)<<13 ,
         _get_task_slot( x, y, p, ltid, CTX_EPC_ID ),
         _get_task_slot( x, y, p, ltid, CTX_RA_ID ) );
@@ -246,108 +271,61 @@
     }  // end for tasks
 
+    /////////////////////////////////////////
     _sqt_barrier_wait( &_all_procs_barrier );    
-
-    ////////////////////////////////////////////////////////////////////////////
-    // step 3 : compute and set XCU masks for HWI / PTI / WTI interrupts
-
-    unsigned int isr_switch_index = 0xFFFFFFFF;
-    unsigned int hwi_mask = 0;
-    unsigned int pti_mask = 0;
-    unsigned int wti_mask = 0;
-    unsigned int irq_id;            // IN_IRQ index
-    unsigned int entry;             // interrupt vector entry
-
-    for (irq_id = 0; irq_id < 32; irq_id++) 
+    /////////////////////////////////////////
+
+    ////////////////////////////////////////////////////////////////////////////
+    // step 3 : - Each processor complete idle task context initialisation,
+    //            (only the CTX_SP, CTX_RA, CTX_EPC slot, because the CTX_PTPR
+    //            and CTX_PTAB slots have been initialised in boot code)
+    //            The 4 Kbytes idle stack is implemented in the scheduler itself.
+    //          - Each processor starts TICK timer, as soon as at least one task
+    //            is allocated.
+    //          - P[0,0,0] initialises FAT (not done before, because it must 
+    //            be done after the _ptabs_vaddr[v][x][y] array initialisation, 
+    //            for V2P translation in _fat_ioc_access() function).
+    ////////////////////////////////////////////////////////////////////////////
+
+    unsigned int sp  = ((unsigned int)psched) + 0x2000;
+    unsigned int ra  = (unsigned int)(&_ctx_eret);
+    unsigned int epc = (unsigned int)(&_idle_task);
+
+    _set_task_slot( x , y , p , IDLE_TASK_INDEX , CTX_SP_ID  , sp  );
+    _set_task_slot( x , y , p , IDLE_TASK_INDEX , CTX_RA_ID  , ra  );
+    _set_task_slot( x , y , p , IDLE_TASK_INDEX , CTX_EPC_ID , epc );
+
+    if (tasks > 0) _xcu_timer_start( cluster_xy, p, GIET_TICK_VALUE ); 
+
+#if GIET_DEBUG_INIT
+_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] initializes idle_task and starts TICK\n",  
+        x, y, p );
+#endif
+
+    if ( gpid == 0 )
     {
-        entry = psched->hwi_vector[irq_id];
-        if ( entry & 0x80000000 ) hwi_mask = hwi_mask | (1<<irq_id);
-        if ( (entry & 0x0000FFFF) == ISR_TICK ) isr_switch_index = irq_id;
-
-        entry = psched->pti_vector[irq_id];
-        if ( entry & 0x80000000 ) pti_mask = pti_mask | (1<<irq_id);
-        if ( (entry & 0x0000FFFF) == ISR_TICK ) isr_switch_index = irq_id;
-
-        entry = psched->wti_vector[irq_id];
-        if ( entry & 0x80000000 ) wti_mask = wti_mask | (1<<irq_id);
-        if ( (entry & 0x0000FFFF) == ISR_TICK ) isr_switch_index = irq_id;
+         _fat_init( 0 );   // no IRQ
+
+#if GIET_DEBUG_INIT
+_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] completes kernel FAT init\n",
+        x, y, p );
+#endif
+
     }
 
-#if GIET_DEBUG_INIT
-_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] sets XCU masks\n"
-        " - ISR_TICK_INDEX = %d\n"
-        " - XCU HWI_MASK   = %x\n"
-        " - XCU WTI_MASK   = %x\n"
-        " - XCU PTI_MASK   = %x\n",
-        x, y, p, 
-        isr_switch_index,
-        hwi_mask, wti_mask, pti_mask );
-#endif
-
-    unsigned int channel = p * IRQ_PER_PROCESSOR; 
-
-    _xcu_set_mask( cluster_xy, channel, hwi_mask, IRQ_TYPE_HWI ); 
-    _xcu_set_mask( cluster_xy, channel, wti_mask, IRQ_TYPE_WTI );
-    _xcu_set_mask( cluster_xy, channel, pti_mask, IRQ_TYPE_PTI );
-
-    ////////////////////////////////////////////////////////////////////////////
-    // step 4 : Each processor start TICK timer if at least one task
-
-    if (tasks > 0) 
-    {
-        // one ISR_TICK must be defined for each proc
-        if (isr_switch_index == 0xFFFFFFFF) 
-        {
-            _printf("\n[GIET ERROR] ISR_TICK not found for processor[%d,%d,%d]\n",
-                           x, y, p );
-            _exit();
-        }
-
-        // start system timer
-        _xcu_timer_start( cluster_xy, isr_switch_index, GIET_TICK_VALUE ); 
-
-    }
-
-#if GIET_DEBUG_INIT
-_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] starts TICK timer\n",
-        x, y, p );
-#endif
-
-    ////////////////////////////////////////////////////////////////////////////
-    // step 5 : each processor updates the idle_task context:
-    //          (CTX_SP, CTX_RA, CTX_EPC).
-    //          The 4 Kbytes idle stack is implemented in the scheduler.
-    //          The PTPR register, the CTX_PTPR and CTX_PTAB slots 
-    //          have been initialised in boot code.
-
-    unsigned int pstack = ((unsigned int)psched) + 0x2000;
-
-    _set_task_slot( x, y, p, IDLE_TASK_INDEX, CTX_SP_ID,  pstack);
-    _set_task_slot( x, y, p, IDLE_TASK_INDEX, CTX_RA_ID,  (unsigned int) &_ctx_eret);
-    _set_task_slot( x, y, p, IDLE_TASK_INDEX, CTX_EPC_ID, (unsigned int) &_idle_task);
-
-#if GIET_DEBUG_INIT
-_printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] initializes IDLE task\n"
-        " - stack_base = %x\n"
-        " - stack_size = 0x1000\n",
-        x, y, p, pstack - 0x1000 );
-#endif
-
+    /////////////////////////////////////////
     _sqt_barrier_wait( &_all_procs_barrier );    
-
-    ////////////////////////////////////////////////////////////////////////////
-    // step 6 : Each processor compute values for registers SP, SR, PTPR, EPC,
+    /////////////////////////////////////////
+
+    ////////////////////////////////////////////////////////////////////////////
+    // step 4 : Each processor compute values for registers SP, SR, PTPR, EPC,
     //          corresponding to the first allocated task (can be idle task)
-    //          and jump to user code when barrier is reached
-
-    if (tasks == 0)
-    {
-        ltid = IDLE_TASK_INDEX;
-        _printf("\n[GIET WARNING] No task allocated to processor[%d,%d,%d]\n",
-                x, y, p );
-    }
-    else
-    {
-        ltid = 0;
-    }
+    //          and jumps to user code.
+    ////////////////////////////////////////////////////////////////////////////
+
+    if (tasks == 0) _printf("\n[GIET WARNING] No task allocated to P[%d,%d,%d]\n",
+                            x, y, p );
+
+    if (tasks == 0) ltid = IDLE_TASK_INDEX;
+    else            ltid = 0;
 
     unsigned int sp_value   = _get_task_slot( x, y, p, ltid, CTX_SP_ID);
@@ -356,11 +334,9 @@
     unsigned int epc_value  = _get_task_slot( x, y, p, ltid, CTX_EPC_ID);
 
-    _sqt_barrier_wait( &_all_procs_barrier );
-
 #if GIET_DEBUG_INIT
 _printf("\n[DEBUG KERNEL_INIT] P[%d,%d,%d] jumps to user code at cycle %d\n"
-        "  sp = %x / sr = %x / ptpr = %x / epc = %x\n",
-        x, y, p, _get_proctime(),
-        sp_value, sr_value, ptpr_value, epc_value );
+        " ltid = %d / sp = %x / sr = %x / ptpr = %x / epc = %x\n",
+        x , y , p , _get_proctime() ,
+        ltid , sp_value , sr_value , ptpr_value , epc_value );
 #endif
 
Index: /soft/giet_vm/giet_kernel/sys_handler.c
===================================================================
--- /soft/giet_vm/giet_kernel/sys_handler.c	(revision 527)
+++ /soft/giet_vm/giet_kernel/sys_handler.c	(revision 528)
@@ -61,14 +61,18 @@
 #endif
 
-
 ////////////////////////////////////////////////////////////////////////////
-//     Coprocessors loks and synchronisation variables
+//        Extern variables
 ////////////////////////////////////////////////////////////////////////////
 
-__attribute__((section(".kdata")))
-simple_lock_t  _coproc_lock[X_SIZE*Y_SIZE];
-
-__attribute__((section(".kdata")))
-unsigned int   _coproc_done[X_SIZE*Y_SIZE];
+// allocated in tty0.c file.
+extern sqt_lock_t _tty0_sqt_lock;
+
+// allocated in mwr_driver.c file.
+extern simple_lock_t  _coproc_lock[X_SIZE*Y_SIZE];
+extern unsigned int   _coproc_done[X_SIZE*Y_SIZE];
+
+// allocated in tty_driver.c file.
+extern unsigned int _tty_rx_full[NB_TTY_CHANNELS];
+extern unsigned int _tty_rx_buf[NB_TTY_CHANNELS];
 
 ////////////////////////////////////////////////////////////////////////////
@@ -91,14 +95,4 @@
 __attribute__((section(".kdata")))
 unsigned int _nic_tx_channel_allocator = 0;
-
-////////////////////////////////////////////////////////////////////////////
-// These global variables are allocated in tty0.c and tty_driver.c files.
-////////////////////////////////////////////////////////////////////////////
-
-extern sqt_lock_t _tty0_sqt_lock;
-
-extern unsigned int _tty_rx_full[NB_TTY_CHANNELS];
-
-extern unsigned int _tty_rx_buf[NB_TTY_CHANNELS];
 
 ////////////////////////////////////////////////////////////////////////////
@@ -157,5 +151,5 @@
     &_sys_ukn,                  /* 0x17 */
     &_sys_ukn,                  /* 0x18 */   
-    &_context_switch,           /* 0x19 */
+    &_sys_context_switch,       /* 0x19 */
     &_sys_vseg_get_vbase,       /* 0x1A */
     &_sys_vseg_get_length,      /* 0x1B */
@@ -355,8 +349,5 @@
     unsigned int size = desc->buffer_size;
  
-    // these variables are used for the v2p translations
-    unsigned int       ptab  = _get_context_slot(CTX_PTAB_ID);
-    unsigned int       ppn;
-    unsigned int       flags;
+    // physical addresses
     unsigned long long buffer_paddr;
     unsigned int       buffer_lsb;
@@ -369,13 +360,10 @@
     unsigned int       lock_msb;
 
+    unsigned int       flags;     // unused
+
     // compute memory buffer physical address
-    _v2p_translate( (page_table_t*)ptab,
-                    desc->buffer_vaddr>>12,
-                    &ppn,
-                    &flags );
-    buffer_paddr = (((unsigned long long)ppn) << 12) | 
-                   (desc->buffer_vaddr & 0x00000FFF);
-    buffer_lsb = (unsigned int)buffer_paddr;
-    buffer_msb = (unsigned int)(buffer_paddr>>32); 
+    buffer_paddr = _v2p_translate( desc->buffer_vaddr , &flags );
+    buffer_lsb   = (unsigned int)buffer_paddr;
+    buffer_msb   = (unsigned int)(buffer_paddr>>32); 
 
     // call MWMR_DMA driver
@@ -385,28 +373,21 @@
     _mwr_set_channel_register( cluster_xy, channel, CHANNEL_BUFFER_MSB, buffer_msb ); 
                        
-    // compute MWMR descriptor and lock physical addresses (if required)
     if ( mode == MODE_MWMR )
     {
-        _v2p_translate( (page_table_t*)ptab,
-                        desc->mwmr_vaddr>>12,
-                        &ppn,
-                        &flags );
-        mwmr_paddr = (((unsigned long long)ppn) << 12) | 
-                     (desc->mwmr_vaddr & 0x00000FFF);
+        // compute MWMR descriptor physical address
+        mwmr_paddr = _v2p_translate( desc->mwmr_vaddr , &flags );
         mwmr_lsb = (unsigned int)mwmr_paddr;
         mwmr_msb = (unsigned int)(mwmr_paddr>>32); 
-
-        _v2p_translate( (page_table_t*)ptab,
-                        desc->lock_vaddr>>12,
-                        &ppn,
-                        &flags );
-        lock_paddr = (((unsigned long long)ppn) << 12) | 
-                     (desc->lock_vaddr & 0x00000FFF);
-        lock_lsb = (unsigned int)lock_paddr;
-        lock_msb = (unsigned int)(lock_paddr>>32); 
 
         // call MWMR_DMA driver
         _mwr_set_channel_register( cluster_xy, channel, CHANNEL_MWMR_LSB, mwmr_lsb ); 
         _mwr_set_channel_register( cluster_xy, channel, CHANNEL_MWMR_MSB, mwmr_msb ); 
+
+        // compute lock physical address
+        lock_paddr = _v2p_translate( desc->lock_vaddr , &flags );
+        lock_lsb = (unsigned int)lock_paddr;
+        lock_msb = (unsigned int)(lock_paddr>>32); 
+
+        // call MWMR_DMA driver
         _mwr_set_channel_register( cluster_xy, channel, CHANNEL_LOCK_LSB, lock_lsb ); 
         _mwr_set_channel_register( cluster_xy, channel, CHANNEL_LOCK_MSB, lock_msb ); 
@@ -740,15 +721,12 @@
     unsigned long long ker_chbuf_pbase;     // kernel chbuf physical address
 
-    // These variables are used for the various V2P translation
-    unsigned int       ptab  = _get_context_slot(CTX_PTAB_ID);
-    unsigned int       ppn;
-    unsigned int       flags;
-    unsigned int       vaddr;
-
     // allocate one kernel container per cluster in the (xmax / ymax) mesh
-    unsigned int        cx;              // cluster X coordinate
-    unsigned int        cy;              // cluster Y coordinate
-    unsigned int        index;           // container index in chbuf
-    unsigned long long  cont_paddr;      // container physical address
+    unsigned int        cx;                 // cluster X coordinate
+    unsigned int        cy;                 // cluster Y coordinate
+    unsigned int        index;              // container index in chbuf
+    unsigned int        vaddr;              // virtual address
+    unsigned long long  cont_paddr;         // container physical address
+
+    unsigned int        flags;              // for _v2p_translate()
 
     for ( cx = 0 ; cx < xmax ; cx++ )
@@ -770,9 +748,5 @@
 
             // compute container physical address
-            _v2p_translate( (page_table_t*)ptab,
-                            vaddr>>12,
-                            &ppn,
-                            &flags );
-            cont_paddr = (((unsigned long long)ppn) << 12) | (vaddr & 0x00000FFF);
+            cont_paddr = _v2p_translate( vaddr , &flags );
 
             // initialize chbuf entry
@@ -816,9 +790,6 @@
     if ( is_rx ) vaddr = (unsigned int)( &_nic_rx_chbuf[nic_channel] );
     else         vaddr = (unsigned int)( &_nic_tx_chbuf[nic_channel] );
-    _v2p_translate( (page_table_t*)ptab,
-                     vaddr>>12,
-                     &ppn,
-                     &flags );
-    ker_chbuf_pbase = (((unsigned long long)ppn) << 12) | (vaddr & 0x00000FFF);
+
+    ker_chbuf_pbase = _v2p_translate( vaddr , &flags );
 
 #if GIET_DEBUG_NIC
@@ -965,20 +936,11 @@
     unsigned long long kernel_buffer_paddr;  // kernel buffer physical address
     unsigned long long kernel_chbuf_paddr;   // kernel chbuf physical address
-    unsigned long long buffer_desc;          // kernel buffer descriptor
-    unsigned long long buffer_desc_paddr;    // kernel buffer descriptor physical address
+    unsigned long long buffer_descriptor;    // kernel buffer descriptor
+    unsigned long long buffer_desc_paddr;    // kernel buffer descriptor paddr
     unsigned int       index;                // kernel buffer index in chbuf
-
-    // The following variables are used for V2P translation
-    unsigned int ptab = _get_context_slot( CTX_PTAB_ID );
-    unsigned int ppn;
-    unsigned int flags;
-    unsigned int vaddr;
+    unsigned int       flags;                // for _v2P_translate
 
     // Compute user buffer physical address and check access rights
-    vaddr = (unsigned int)buffer;
-    _v2p_translate( (page_table_t*)ptab,
-                     vaddr>>12,
-                     &ppn,
-                     &flags );
+    user_buffer_paddr = _v2p_translate( (unsigned int)buffer , &flags );
 
     if ( (flags & PTE_U) == 0 )
@@ -987,5 +949,4 @@
         return -1;
     }
-    user_buffer_paddr = ((unsigned long long)ppn << 12) | (vaddr & 0x00000FFF);
 
 #if GIET_DEBUG_NIC
@@ -995,10 +956,5 @@
 
     // compute kernel chbuf physical address (required for sync)
-    vaddr = (unsigned int)chbuf;
-    _v2p_translate( (page_table_t*)ptab,
-                     vaddr>>12,
-                     &ppn,
-                     &flags );
-    kernel_chbuf_paddr = ((unsigned long long)ppn << 12) | (vaddr & 0x00000FFF);
+    kernel_chbuf_paddr = _v2p_translate( (unsigned int)chbuf , &flags );
 
     // poll local kernel container status until success
@@ -1011,19 +967,19 @@
         // inval buffer descriptor in L2 before read in L2
         _mmc_inval( buffer_desc_paddr , 8 );
-        buffer_desc = chbuf->buffer[index].desc;
+        buffer_descriptor = chbuf->buffer[index].desc;
 
 #if GIET_DEBUG_NIC
 _printf("\n[GIET DEBUG NIC] Task %d in _sys_nic_move() read buffer descriptor %d\n"
         " at cycle = %d / paddr = %l / buffer descriptor = %l\n",
-        thread, index, _get_proctime(), buffer_desc_paddr, buffer_desc );
+        thread, index, _get_proctime(), buffer_desc_paddr, buffer_descriptor );
 #endif
 
         // test buffer status and break if found
-        if ( ( is_rx != 0 ) && (buffer_desc >> 63) == 1 )  break;
-        if ( ( is_rx == 0 ) && (buffer_desc >> 63) == 0 )  break;
+        if ( ( is_rx != 0 ) && (buffer_descriptor >> 63) == 1 )  break;
+        if ( ( is_rx == 0 ) && (buffer_descriptor >> 63) == 0 )  break;
     }
 
     // compute kernel buffer physical address
-    kernel_buffer_paddr = buffer_desc & 0x0000FFFFFFFFFFFFULL;
+    kernel_buffer_paddr = buffer_descriptor & 0x0000FFFFFFFFFFFFULL;
     
     // move one container
@@ -1281,8 +1237,6 @@
 #if NB_CMA_CHANNELS > 0
 
-    unsigned int       ptab;            // page table virtual address
     unsigned int       vaddr;           // virtual address
-    unsigned int       flags;           // protection flags
-    unsigned int       ppn;             // physical page number
+    unsigned int       flags;           // for _v2p_translate()
 
     // get channel index
@@ -1308,49 +1262,35 @@
 
     // checking user buffers virtual addresses and length alignment
-    if ( ((unsigned int)vbase0 & 0x3) || ((unsigned int)vbase1 & 0x3) || (length & 0x3) ) 
-    {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : user buffer not word aligned\n");
-        return -1;
-    }
-
-    // get page table virtual address
-    ptab = _get_context_slot(CTX_PTAB_ID);
+    if ( ((unsigned int)vbase0 & 0x3) || 
+         ((unsigned int)vbase1 & 0x3) || 
+         (length & 0x3) ) 
+    {
+        _printf("\n[GIET ERROR] in _fbf_cma_start() : user buffer not aligned\n");
+        return -1;
+    }
 
     // compute frame buffer physical address and initialize _fbf_chbuf[channel]
-    vaddr = ((unsigned int)SEG_FBF_BASE);
-    _v2p_translate( (page_table_t*) ptab, 
-                    (vaddr >> 12),
-                    &ppn, 
-                    &flags );
-
-    _fbf_chbuf[channel].fbf.desc = ((paddr_t)ppn << 12) | (vaddr & 0x00000FFF);
+    vaddr = (unsigned int)SEG_FBF_BASE;
+    _fbf_chbuf[channel].fbf.desc = _v2p_translate( vaddr , &flags );
 
     // Compute user buffer 0 physical addresses and intialize _fbf_chbuf[channel]
-    vaddr = (unsigned int)vbase0; 
-    _v2p_translate( (page_table_t*) ptab, 
-                    (vaddr >> 12),
-                    &ppn, 
-                    &flags );
+    vaddr = (unsigned int)vbase0;
+    _fbf_chbuf[channel].buf0.desc = _v2p_translate( vaddr , &flags );
+
     if ((flags & PTE_U) == 0) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : user buffer 0 not in user space\n");
-        return -1;
-    }
-
-    _fbf_chbuf[channel].buf0.desc = ((paddr_t)ppn << 12) | (vaddr & 0x00000FFF);
+        _printf("\n[GIET ERROR] in _fbf_cma_start() : buf0 not in user space\n");
+        return -1;
+    }
 
     // Compute user buffer 1 physical addresses and intialize _fbf_chbuf[channel]
-    vaddr = (unsigned int)vbase1; 
-    _v2p_translate( (page_table_t*) ptab, 
-                    (vaddr >> 12),
-                    &ppn, 
-                    &flags );
+    vaddr = (unsigned int)vbase1;
+    _fbf_chbuf[channel].buf1.desc = _v2p_translate( vaddr , &flags );
+
     if ((flags & PTE_U) == 0) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : user buffer 1 not in user space\n");
-        return -1;
-    }
-
-    _fbf_chbuf[channel].buf1.desc = ((paddr_t)ppn << 12) | (vaddr & 0x00000FFF);
+        _printf("\n[GIET ERROR] in _fbf_cma_start() : buf1 not in user space\n");
+        return -1;
+    }
 
     // initializes buffer length
@@ -1358,12 +1298,7 @@
 
     // Compute and register physical adress of the fbf_chbuf descriptor
-    vaddr = (unsigned int)(&_fbf_chbuf[channel]);
-    _v2p_translate( (page_table_t*) ptab, 
-                    (vaddr >> 12),
-                    &ppn, 
-                    &flags );
+    vaddr = (unsigned int)&_fbf_chbuf[channel];
+    _fbf_chbuf_paddr[channel] = _v2p_translate( vaddr , &flags );
  
-    _fbf_chbuf_paddr[channel] = (((paddr_t)ppn) << 12) | (vaddr & 0x00000FFF);
-
     if ( USE_IOB )
     {
@@ -1594,11 +1529,11 @@
 
     // deschedule
-    _context_switch();
+    _sys_context_switch();
 
     return 0;
 } 
 
-//////////////////////
-int _context_switch() 
+/////////////////////////
+int _sys_context_switch() 
 {
     unsigned int save_sr;
@@ -1755,16 +1690,10 @@
                       unsigned int* y )
 {
-    unsigned int ppn;
     unsigned int flags;
-    unsigned int vpn  = (((unsigned int)ptr)>>12);
+    unsigned long long paddr = _v2p_translate( (unsigned int)ptr , &flags );
     
-    // get the page table pointer
-    page_table_t* pt = (page_table_t*)_get_context_slot( CTX_PTAB_ID ); 
-
-    // compute the physical address
-    _v2p_translate( pt, vpn, &ppn, &flags );
-
-    *x = (ppn>>24) & 0xF;
-    *y = (ppn>>20) & 0xF;
+    *x = (paddr>>36) & 0xF;
+    *y = (paddr>>32) & 0xF;
+
     return 0;
 }
Index: /soft/giet_vm/giet_kernel/sys_handler.h
===================================================================
--- /soft/giet_vm/giet_kernel/sys_handler.h	(revision 527)
+++ /soft/giet_vm/giet_kernel/sys_handler.h	(revision 528)
@@ -197,5 +197,5 @@
 int _sys_task_exit( char* string );
 
-int _context_switch();
+int _sys_context_switch();
 
 int _sys_local_task_id();
