Index: soft/giet_vm/sys/drivers.c
===================================================================
--- soft/giet_vm/sys/drivers.c	(revision 169)
+++ soft/giet_vm/sys/drivers.c	(revision 189)
@@ -5,5 +5,5 @@
 // Copyright (c) UPMC-LIP6
 ///////////////////////////////////////////////////////////////////////////////////
-// The drivers.c and drivers.h files are part ot the GIET nano kernel.
+// The drivers.c and drivers.h files are part ot the GIET-VM nano kernel.
 // They contains the drivers for the peripherals available in the SoCLib library:
 // - vci_multi_tty
@@ -11,4 +11,5 @@
 // - vci_multi_dma
 // - vci_multi_icu
+// - vci_xicu
 // - vci_gcd
 // - vci_frame_buffer
@@ -16,11 +17,9 @@
 //
 // The following global parameters must be defined in the giet_config.h file:
-// - NB_CLUSTERS  : number of clusters 
-// - NB_PROCS     : number of PROCS per cluster 
-// - NB_TIMERS    : number of TIMERS per cluster
-// - NB_DMAS      : number of DMA channels
-// - NB_TTYS      : number of TTY terminals
-// - NB_TIMERS    : number of TIMERS per cluster
-// - CLUSTER_SPAN : address increment between clusters
+// - NB_CLUSTERS   
+// - NB_PROCS_MAX  
+// - NB_TIMERS_MAX    
+// - NB_DMAS_MAX     
+// - NB_TTYS    
 //
 // The following base addresses must be defined in the sys.ld file:
@@ -43,21 +42,22 @@
 #include <ctx_handler.h>
 
-#if !defined(NB_PROCS) 
-# error: You must define NB_PROCS in 'giet_config.h' file!
-#endif
 #if !defined(NB_CLUSTERS) 
-# error: You must define NB_CLUSTERS in 'giet_config.h' file!
-#endif
+# error: You must define NB_CLUSTERS in 'giet_config.h' file
+#endif
+
+#if !defined(NB_PROCS_MAX) 
+# error: You must define NB_PROCS_MAX in 'giet_config.h' file
+#endif
+
+#if (NB_PROCS_MAX > 8)
+# error: NB_PROCS_MAX cannot be larger than 8!
+#endif
+
 #if !defined(CLUSTER_SPAN) 
-# error: You must define CLUSTER_SPAN in 'giet_config.h' file!
-#endif
+# error: You must define CLUSTER_SPAN in 'giet_config.h' file
+#endif
+
 #if !defined(NB_TTYS)
-# error: You must define NB_TTYS in 'giet_config.h' file!
-#endif
-#if !defined(NB_DMAS)
-# error: You must define NB_DMAS in 'giet_config.h' file!
-#endif
-#if !defined(NB_TIMERS)
-# error: You must define NB_TIMERS in 'giet_config.h' file!
+# error: You must define NB_TTYS in 'giet_config.h' file
 #endif
 
@@ -66,124 +66,185 @@
 #endif
 
-#if (NB_TIMERS < NB_PROCS)
-# error: NB_TIMERS must be larger or equal to NB_PROCS!
-#endif
-
-#if (NB_PROCS > 8)
-# error: NB_PROCS cannot be larger than 8!
-#endif
-
-#if (NB_DMAS < 1)
-# error: NB_DMAS cannot be 0!
-#endif
-
-
-/////////////////////////////////////////////////////////////////////////////
-// 	Global (uncachable) variables
-/////////////////////////////////////////////////////////////////////////////
+#if !defined(NB_DMAS_MAX)
+# error: You must define NB_DMAS_MAX in 'giet_config.h' file
+#endif
+
+#if (NB_DMAS_MAX < 1)
+# error: NB_DMAS_MAX cannot be 0!
+#endif
+
+#if !defined(NB_TIMERS_MAX)
+# error: You must define NB_TIMERS_MAX in 'giet_config.h' file 
+#endif
+
+#if ( (NB_TIMERS_MAX + NB_PROCS_MAX) > 32 )
+# error: NB_TIMERS_MAX + NB_PROCS_MAX cannot be larger than 32
+#endif
+
+#if !defined(NB_IOCS)
+# error: You must define NB_IOCS in 'giet_config.h' file 
+#endif
+
+#if ( NB_IOCS > 1 )
+# error: NB_IOCS cannot be larger than 1
+#endif
+
 
 #define in_unckdata __attribute__((section (".unckdata")))
 
-// IOC variables
-in_unckdata volatile unsigned char _ioc_status       = 0;
-in_unckdata volatile unsigned char _ioc_done         = 0;
-in_unckdata unsigned int		   _ioc_lock         = 0;
-in_unckdata unsigned int		   _ioc_iommu_ix1    = 0;
-in_unckdata unsigned int		   _ioc_iommu_npages; 
-
-// DMA variables
-in_unckdata volatile unsigned int  _dma_status[NB_DMAS];
-in_unckdata volatile unsigned char _dma_busy[NB_DMAS] = { [0 ... NB_DMAS-1] = 0 };
-in_unckdata volatile unsigned char _dma_iommu_ix1     = 1;
-in_unckdata volatile unsigned char _dma_iommu_npages[NB_DMAS];
+
+//////////////////////////////////////////////////////////////////////////////
+// 	VciMultiTimer driver
+//////////////////////////////////////////////////////////////////////////////
+// There is one multi_timer (or xicu) component per cluster.
+// The global index is cluster_id*(NB_PROCS_MAX+NB_TIMERS_MAX) + local_id
+// There is two types of timers: 
+// - "system" timers : one per processor, used for context switch.
+//   local_id in [0, NB_PROCS_MAX-1],
+// - "user" timers : requested by the task in the mapping_info data structure.
+//   local_id in [NB_PROC_MAX, NB_PROCS_MAX+NB_TIMERS_MAX-1],
+//   For each user timer, the tty_id is stored in the context of the task
+//   and must be explicitely defined in the boot code.
+// These timers can be implemented in a vci_multi_timer component 
+// or in a vci_xicu component (depending on the GIET_USE_XICU parameter).
+//////////////////////////////////////////////////////////////////////////////
+
+// User Timer signaling variables 
+
+#if (NB_TIMERS_MAX > 0)
+in_unckdata volatile unsigned char _user_timer_event[NB_CLUSTERS*NB_TIMERS_MAX] 
+         = { [0 ... ((NB_CLUSTERS*NB_TIMERS_MAX)-1)] = 0 };
+#endif
+
+//////////////////////////////////////////////////////////////////////////////
+//     _timer_access()
+// This function is the only way to access a timer device.
+// It can be a multi-timer component or an xicu component.
+// It can be used by the kernel to initialise a "system" timer,
+// or by a task (through a system call) to configure an "user" timer.
+// Returns 0 if success, > 0 if error.
+//////////////////////////////////////////////////////////////////////////////
+unsigned int _timer_access( unsigned int	read,
+                            unsigned int	cluster_id,
+                            unsigned int	local_id,
+                            unsigned int	register_id, 
+                            unsigned int*	buffer )
+{
+    // parameters checking 
+    if ( register_id >= TIMER_SPAN)					return 1;
+    if ( cluster_id >= NB_CLUSTERS)					return 1;
+    if ( local_id >= NB_TIMERS_MAX + NB_PROCS_MAX ) return 1;
+
+#if GIET_USE_XICU
+
+    unsigned int* timer_address = //TODO
+
+#else
+
+    unsigned int* timer_address = (unsigned int*)&seg_timer_base + 
+                                  (cluster_id * CLUSTER_SPAN)  +
+                                  (local_id * TIMER_SPAN);
+#endif
+
+    if (read)	*buffer = timer_address[register_id]; // read word 
+    else		timer_address[register_id] = *buffer; // write word
+    return 0;
+}
+//////////////////////////////////////////////////////////////////////////////
+//     _timer_write()
+// This function implements a write access to a "user" timer register.
+// It gets the cluster_id and local_id from the global index stored in
+// the task context and use the timer_access() function to make the write.
+// Returns 0 if success, > 0 if error.
+//////////////////////////////////////////////////////////////////////////////
+unsigned int _timer_write( unsigned int register_id, 
+                           unsigned int value )
+{
+    unsigned int buffer     = value;
+    unsigned int timer_id   = _get_current_context_slot(CTX_TIMER_ID);
+    unsigned int cluster_id = timer_id / (NB_PROCS_MAX + NB_TIMERS_MAX);
+    unsigned int local_id   = timer_id % (NB_PROCS_MAX + NB_TIMERS_MAX);
+
+    // checking user timer
+    if ( local_id < NB_PROCS_MAX ) 
+    {
+        return 2;
+    }
+    else
+    {
+        return _timer_access ( 0,				// write access
+                               cluster_id,
+                               local_id,
+                               register_id,
+                               &buffer );
+    }
+}
+//////////////////////////////////////////////////////////////////////////////
+//     _timer_read()
+// This function implements a read access to a "user" timer register.
+// It gets the cluster_id and local_id from the global index stored in
+// the task context and use the timer_access() function to make the read.
+// Returns 0 if success, > 0 if error.
+//////////////////////////////////////////////////////////////////////////////
+unsigned int _timer_read( unsigned int  register_id, 
+                          unsigned int* buffer )
+{
+    unsigned int timer_id   = _get_current_context_slot(CTX_TIMER_ID);
+    unsigned int cluster_id = timer_id / (NB_PROCS_MAX + NB_TIMERS_MAX);
+    unsigned int local_id   = timer_id % (NB_PROCS_MAX + NB_TIMERS_MAX);
+
+    // checking user timer
+    if ( local_id < NB_PROCS_MAX ) 
+    {
+        return 2;
+    }
+    else
+    {
+        return _timer_access ( 1,				// read access
+                               cluster_id,
+                               local_id,
+                               register_id,
+                               buffer );
+    }
+}
+/////////////////////////////////////////////////////////////////////////////////
+//     _timer_check()
+/////////////////////////////////////////////////////////////////////////////////
+
+/////////////////////////////////////////////////////////////////////////////////
+// 	VciMultiTty driver
+/////////////////////////////////////////////////////////////////////////////////
+// There is only one multi_tty controler in the architecture.
+// The total number of TTYs is defined by the configuration parameter NB_TTYS.
+// The "system" terminal is TTY[0].
+// The "user" TTYs are allocated to applications by the GIET in the boot phase,
+// as defined in the mapping_info data structure. The corresponding tty_id must 
+// be stored in the context of the task by the boot code.
+// The TTY address is : seg_tty_base + tty_id*TTY_SPAN
+/////////////////////////////////////////////////////////////////////////////////
 
 // TTY variables
 in_unckdata volatile unsigned char _tty_get_buf[NB_TTYS];
 in_unckdata volatile unsigned char _tty_get_full[NB_TTYS] = { [0 ... NB_TTYS-1] = 0 };
-in_unckdata unsigned int           _tty_put_lock          = 0;
-
-//////////////////////////////////////////////////////////////////////////////
-// 	VciMultiTimer driver
-//////////////////////////////////////////////////////////////////////////////
-// There is one MULTI-TIMER component per cluster.
-// The number of timers per cluster must be larger or equal to the number 
-// processors (NB_TIMERS >= NB_PROCS), because each processor uses a private
-// yimer for context switch.
-// The total number of timers is NB_CLUSTERS * NB_TIMERS
-// The global timer index = cluster_id*NB_TIMERS + timer_id
-//////////////////////////////////////////////////////////////////////////////
-
-//////////////////////////////////////////////////////////////////////////////
-// _timer_write()
-//
-// Write a 32-bit word in a memory mapped register of a timer device,
-// identified by the cluster index and the local timer index. 
-// Returns 0 if success, > 0 if error.
-//////////////////////////////////////////////////////////////////////////////
-unsigned int _timer_write( unsigned int cluster_index,
-                           unsigned int timer_index,
-                           unsigned int register_index, 
-                           unsigned int value )
-{
-    unsigned int*	timer_address;
-
-    // parameters checking 
-    if ( register_index >= TIMER_SPAN) 		return 1;
-    if ( cluster_index >= NB_CLUSTERS)		return 1;
-    if ( timer_index >= NB_TIMERS )         return 1;
-
-    timer_address = (unsigned int*)&seg_timer_base + 
-                    ( cluster_index * CLUSTER_SPAN )  +
-                    ( timer_index * TIMER_SPAN );
-
-    timer_address[register_index] = value; // write word
-
-    return 0;
-}
-
-//////////////////////////////////////////////////////////////////////////////
-// _timer_read()
-//
-// Read a 32-bit word in a memory mapped register of a timer device,
-// identified by the cluster index and the local timer index. 
-// Returns 0 if success, > 0 if error.
-//////////////////////////////////////////////////////////////////////////////
-unsigned int _timer_read(unsigned int cluster_index,
-                         unsigned int timer_index, 
-                         unsigned int register_index, 
-                         unsigned int *buffer)
-{
-    unsigned int *timer_address;
-
-    // parameters checking
-    if ( register_index >= TIMER_SPAN) 		return 1;
-    if ( cluster_index >= NB_CLUSTERS)		return 1;
-    if ( timer_index >= NB_TIMERS )         return 1;
-
-    timer_address = (unsigned int*)&seg_timer_base + 
-                    ( cluster_index * CLUSTER_SPAN )  +
-                    ( timer_index * TIMER_SPAN );
-
-    *buffer = timer_address[register_index]; // read word 
-
-    return 0;
-}
-
+in_unckdata unsigned int           _tty_put_lock = 0;  // protect kernel TTY[0]
+
+////////////////////////////////////////////////////////////////////////////////
+//      _tty_error()
+////////////////////////////////////////////////////////////////////////////////
+void _tty_error()
+{
+    unsigned int task_id = _get_current_task_id();
+    unsigned int proc_id = _procid();
+
+    _get_lock(&_tty_put_lock);
+    _puts("\n[GIET ERROR] TTY index too large for task ");
+    _putw( task_id );
+    _puts(" on processor ");
+    _putw( proc_id );
+    _puts("\n");
+    _release_lock(&_tty_put_lock);
+}
 /////////////////////////////////////////////////////////////////////////////////
-// 	VciMultiTty driver
-/////////////////////////////////////////////////////////////////////////////////
-// The total number of TTYs is defined by the configuration parameter NB_TTYS.
-// The system terminal is TTY[0].
-// The TTYs are allocated to applications by the GIET in the boot phase.
-// The nummber of TTYs allocated to each application, and used by each
-// task can be defined in the mapping_info data structure.
-// For each user task, the tty_id is stored in the context of the task (slot 34),
-// and must be explicitely defined in the boot code.
-// The TTY address is always computed as : seg_tty_base + tty_id*TTY_SPAN
-///////////////////////////////////////////////////////////////////////////////////
-
-//////////////////////////////////////////////////////////////////////////////
-// _tty_write()
-//
+//      _tty_write()
 // Write one or several characters directly from a fixed-length user buffer to
 // the TTY_WRITE register of the TTY controler.
@@ -192,21 +253,18 @@
 // the transfer as soon as the TTY_STATUS[WRITE] bit is set. 
 // The function returns  the number of characters that have been written.
-//////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////////////////////////////////////////////////////
 unsigned int _tty_write( const char		*buffer, 
                          unsigned int	length)
 {
-    volatile unsigned int *tty_address;
-
-    unsigned int proc_id;
-    unsigned int task_id;
-    unsigned int tty_id;
-    unsigned int nwritten;
-
-    proc_id = _procid();
-    
-    task_id = _scheduler[proc_id].current;
-    tty_id  = _scheduler[proc_id].context[task_id][CTX_TTY_ID];
-
-    tty_address = (unsigned int*)&seg_tty_base + tty_id*TTY_SPAN;
+    unsigned int	nwritten;
+
+    unsigned int	tty_id = _get_current_context_slot(CTX_TTY_ID);
+    if ( tty_id >= NB_TTYS )
+    {
+        _tty_error();
+        return 0;
+    }
+
+    unsigned int*	tty_address = (unsigned int*)&seg_tty_base + tty_id*TTY_SPAN;
 
     for (nwritten = 0; nwritten < length; nwritten++)
@@ -221,8 +279,6 @@
     return nwritten;
 }
-
 //////////////////////////////////////////////////////////////////////////////
-// _tty_read_irq()
-//
+//      _tty_read_irq()
 // This non-blocking function uses the TTY_GET_IRQ[tty_id] interrupt and 
 // the associated kernel buffer, that has been written by the ISR.
@@ -235,16 +291,15 @@
                             unsigned int	length)
 {
-    unsigned int proc_id;
-    unsigned int task_id;
-    unsigned int tty_id;
-    unsigned int ret;
-
-    proc_id = _procid();
-    task_id = _scheduler[proc_id].current;
-    tty_id  = _scheduler[proc_id].context[task_id][CTX_TTY_ID];
+    unsigned int	tty_id = _get_current_context_slot(CTX_TTY_ID);
+
+    if ( tty_id >= NB_TTYS )
+    {
+        _tty_error();
+        return 0;
+    }
 
     if (_tty_get_full[tty_id] == 0) 
     {
-        ret = 0;
+        return 0;
     }
     else
@@ -252,12 +307,9 @@
         *buffer = _tty_get_buf[tty_id];
         _tty_get_full[tty_id] = 0;
-        ret = 1;
-    }
-    return ret;
-}
-
-////////////////////////////////////////////////////////////////////////////////
-// _tty_read()
-//
+        return 1;
+    }
+} 
+////////////////////////////////////////////////////////////////////////////////
+//     _tty_read()
 // This non-blocking function fetches one character directly from the TTY_READ 
 // register of the TTY controler, and writes this character to the user buffer.
@@ -268,33 +320,34 @@
                         unsigned int	length)
 {
-    volatile unsigned int *tty_address;
-
-    unsigned int proc_id;
-    unsigned int task_id;
-    unsigned int tty_id;
-
-    proc_id = _procid();
-    task_id = _scheduler[proc_id].current;
-    tty_id  = _scheduler[proc_id].context[task_id][CTX_TTY_ID];
-
-    tty_address = (unsigned int*)&seg_tty_base + tty_id*TTY_SPAN;
-
-    if ((tty_address[TTY_STATUS] & 0x1) != 0x1) return 0;
-
-    *buffer = (char)tty_address[TTY_READ];
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////////////
-// 	VciMultiIcu driver
-////////////////////////////////////////////////////////////////////////////////
-// There is in principle one MULTI-ICU component per cluster, and the
-// number of independant ICUs is equal to NB_PROCS, because there is 
-// one ICU per processor.
-////////////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////////////
-// _icu_write()
-//
+    unsigned int	tty_id = _get_current_context_slot(CTX_TTY_ID);
+    if ( tty_id >= NB_TTYS )
+    {
+        _tty_error();
+        return 0;
+    }
+
+    unsigned int*	tty_address = (unsigned int*)&seg_tty_base + tty_id*TTY_SPAN;
+
+    if ((tty_address[TTY_STATUS] & 0x1) != 0x1) 
+    {
+        return 0;
+    }
+    else
+    {
+        *buffer = (char)tty_address[TTY_READ];
+        return 1;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////////////
+// 	VciMultiIcu and VciXicu drivers
+////////////////////////////////////////////////////////////////////////////////
+// There is in principle one vci_multi_icu (or vci_xicu) component per cluster, 
+// and the number of independant ICUs is equal to NB_PROCS_MAX, because there is 
+// one private interrupr controler per processor.
+////////////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////////////
+//     _icu_write()
 // Write a 32-bit word in a memory mapped register of the MULTI_ICU device,
 // identified by the cluster index, and a processor local index.
@@ -306,22 +359,24 @@
                          unsigned int value )
 {
-    unsigned int *icu_address;
+#if GIET_USE_XICU
+
+#else
 
     // parameters checking 
     if ( register_index >= ICU_SPAN) 		return 1;
     if ( cluster_index >= NB_CLUSTERS)		return 1;
-    if ( proc_index >= NB_PROCS )           return 1;
-
-    icu_address = (unsigned int*)&seg_icu_base + 
-                  ( cluster_index * CLUSTER_SPAN )  +
-                  ( proc_index * ICU_SPAN );
+    if ( proc_index >= NB_PROCS_MAX )       return 1;
+
+    unsigned int *icu_address = (unsigned int*)&seg_icu_base + 
+                                (cluster_index * CLUSTER_SPAN)  +
+                                (proc_index * ICU_SPAN);
 
     icu_address[register_index] = value;   // write word 
     return 0;
-}
-
-////////////////////////////////////////////////////////////////////////////////
-// _icu_read()
-//
+
+#endif
+}
+////////////////////////////////////////////////////////////////////////////////
+//     _icu_read()
 // Read a 32-bit word in a memory mapped register of the MULTI_ICU device,
 // identified by the cluster index and a processor local index.
@@ -333,17 +388,21 @@
                          unsigned int* buffer )
 {
-    unsigned int *icu_address;
+#if GIET_USE_XICU
+
+#else
 
     // parameters checking 
     if ( register_index >= ICU_SPAN) 		return 1;
     if ( cluster_index >= NB_CLUSTERS)		return 1;
-    if ( proc_index >= NB_PROCS )           return 1;
-
-    icu_address = (unsigned int*)&seg_icu_base + 
-                  ( cluster_index * CLUSTER_SPAN )  +
-                  ( proc_index * ICU_SPAN );
+    if ( proc_index >= NB_PROCS_MAX )       return 1;
+
+    unsigned int *icu_address = (unsigned int*)&seg_icu_base + 
+                                (cluster_index * CLUSTER_SPAN)  +
+                                (proc_index * ICU_SPAN);
 
     *buffer = icu_address[register_index]; // read word 
     return 0;
+
+#endif
 }
 
@@ -357,6 +416,5 @@
 
 ////////////////////////////////////////////////////////////////////////////////
-// _gcd_write()
-//
+//     _gcd_write()
 // Write a 32-bit word in a memory mapped register of the GCD coprocessor.
 // Returns 0 if success, > 0 if error.
@@ -376,8 +434,6 @@
     return 0;
 }
-
-////////////////////////////////////////////////////////////////////////////////
-// _gcd_read()
-//
+////////////////////////////////////////////////////////////////////////////////
+//     _gcd_read()
 // Read a 32-bit word in a memory mapped register of the GCD coprocessor.
 // Returns 0 if success, > 0 if error.
@@ -448,40 +504,15 @@
 ///////////////////////////////////////////////////////////////////////////////
 
+// IOC global variables
+in_unckdata volatile unsigned int	_ioc_status       = 0;
+in_unckdata volatile unsigned int	_ioc_done         = 0;
+in_unckdata unsigned int			_ioc_lock         = 0;
+in_unckdata unsigned int			_ioc_iommu_ix1    = 0;
+in_unckdata unsigned int			_ioc_iommu_npages; 
+
 ///////////////////////////////////////////////////////////////////////////////
-// _ioc_get_lock()
-//
-// This blocking helper is used by '_ioc_read()' and '_ioc_write()' functions
-// to get _ioc_lock using atomic LL/SC.
-///////////////////////////////////////////////////////////////////////////////
-static inline void _ioc_get_lock()
-{
-    register unsigned int delay = (_proctime() & 0xF) << 4;
-    register unsigned int *plock = (unsigned int*)&_ioc_lock;
-
-    asm volatile (
-            "_ioc_llsc:             \n"
-            "ll   $2,    0(%0)      \n" /* $2 <= _ioc_lock current value */
-            "bnez $2,    _ioc_delay \n" /* delay if _ioc_lock already taken */
-            "li   $3,    1          \n" /* $3 <= argument for sc */
-            "sc   $3,    0(%0)      \n" /* try to set _ioc_lock */
-            "bnez $3,    _ioc_ok    \n" /* exit if atomic */
-            "_ioc_delay:            \n"
-            "move $4,    %1         \n" /* $4 <= delay */
-            "_ioc_loop:             \n"
-            "beqz $4,    _ioc_loop  \n" /* test end delay */
-            "addi $4,    $4,    -1  \n" /* $4 <= $4 - 1 */
-            "j           _ioc_llsc  \n" /* retry ll */
-            "nop                    \n"
-            "_ioc_ok:               \n"
-            :
-            :"r"(plock), "r"(delay)
-            :"$2", "$3", "$4");
-}
-
-///////////////////////////////////////////////////////////////////////////////
-//  _ioc_access()
+//      _ioc_access()
 // This function transfer data between a memory buffer and the block device.
 // The buffer lentgth is (count*block_size) bytes.
-//
 // Arguments are:
 // - to_mem     : from external storage to memory when non 0
@@ -503,9 +534,5 @@
     unsigned int		ix2;			// page index in IOMMU PT1 page table
     unsigned int		addr;			// buffer address for IOC peripheral
-    unsigned int		user_ptp;		// page table pointer in user space
-    unsigned int		ko;				// bool returned by _v2p_translate()
     unsigned int		ppn_first;		// first physical page number for user buffer
-    unsigned int		ltid;			// current task local index
-    static_scheduler_t*	psched;			// pointer on the current task scheduler
         
     // check buffer alignment
@@ -517,7 +544,5 @@
 
     // get user space page table virtual address
-    psched   = &_scheduler[_procid()];
-    ltid     = psched->current;
-    user_ptp = psched->context[ltid][CTX_PTAB_ID];
+    unsigned int user_pt_vbase = _get_current_context_slot(CTX_PTAB_ID);
     
     user_vpn_min = user_vaddr >> 12;
@@ -529,8 +554,8 @@
     {
         // get ppn and flags for each vpn
-        ko = _v2p_translate( (page_table_t*)user_ptp,
-                             vpn,
-                             &ppn,
-                             &flags );
+        unsigned int ko = _v2p_translate( (page_table_t*)user_pt_vbase,
+                                           vpn,
+                                           &ppn,
+                                           &flags );
 
         // check access rights
@@ -573,5 +598,5 @@
 
     // get the lock on ioc device 
-    _ioc_get_lock();
+    _get_lock( &_ioc_lock );
 
     // peripheral configuration  
@@ -584,5 +609,4 @@
     return 0;
 }
-
 /////////////////////////////////////////////////////////////////////////////////
 // _ioc_completed()
@@ -630,7 +654,6 @@
     return ret;
 }
-
 ///////////////////////////////////////////////////////////////////////////////
-// _ioc_read()
+//     _ioc_read()
 // Transfer data from the block device to a memory buffer in user space. 
 // - lba    : first block index on the block device
@@ -643,12 +666,11 @@
                         unsigned int	count )
 {
-    return _ioc_access( 1,		// read
+    return _ioc_access( 1,		// read access
                         lba,
                         (unsigned int)buffer,
                         count );
 }
-
 ///////////////////////////////////////////////////////////////////////////////
-// _ioc_write()
+//     _ioc_write()
 // Transfer data from a memory buffer in user space to the block device. 
 // - lba    : first block index on the block device
@@ -661,5 +683,5 @@
                          unsigned int	count )
 {
-    return _ioc_access( 0,		// write
+    return _ioc_access( 0,		// write access
                         lba,
                         (unsigned int)buffer,
@@ -668,6 +690,39 @@
 
 //////////////////////////////////////////////////////////////////////////////////
+// VciMultiDma driver
+//////////////////////////////////////////////////////////////////////////////////
+// The DMA controllers are physically distributed in the clusters.
+// There is  (NB_CLUSTERS * NB_DMAS_MAX) channels, indexed by a global index:
+//        dma_id = cluster_id * NB_DMA_MAX + loc_id
+//
+// As a DMA channel can be used by several tasks, each DMA channel is protected 
+// by a specific lock: _dma_lock[dma_id]
+// The signalisation between the OS and the DMA uses the _dma_done[dma_id] 
+// synchronisation variables  (set by the ISR, and reset by the OS).
+// The transfer status is copied by the ISR in the _dma_status[dma_id] variables.
+//
+// These DMA channels can be used by the FB driver, or by the NIC driver.
+//////////////////////////////////////////////////////////////////////////////////
+
+#if  (NB_DMAS_MAX > 0) 
+in_unckdata unsigned int			_dma_lock[NB_DMAS_MAX * NB_CLUSTERS]
+                                       = { [0 ... (NB_DMAS_MAX * NB_CLUSTERS)-1] = 0 };
+
+in_unckdata volatile unsigned int	_dma_done[NB_DMAS_MAX * NB_CLUSTERS]
+                                       = { [0 ... (NB_DMAS_MAX * NB_CLUSTERS)-1] = 0 };
+
+in_unckdata volatile unsigned int	_dma_status[NB_DMAS_MAX * NB_CLUSTERS];
+
+in_unckdata unsigned int			_dma_iommu_ix1 = 1;
+
+in_unckdata unsigned int            _dma_iommu_npages[NB_DMAS_MAX * NB_CLUSTERS];
+#endif
+
+//////////////////////////////////////////////////////////////////////////////////
 // 	VciFrameBuffer driver
 //////////////////////////////////////////////////////////////////////////////////
+// The vci_frame_buffer device can be accessed directly by software with memcpy(),
+// or it can be accessed through a multi-channels DMA component:
+//  
 // The '_fb_sync_write' and '_fb_sync_read' functions use a memcpy strategy to
 // implement the transfer between a data buffer (user space) and the frame
@@ -675,11 +730,7 @@
 //
 // The '_fb_write()', '_fb_read()' and '_fb_completed()' functions use the DMA
-// coprocessor to transfer data between the user buffer and the frame buffer.
-// These  functions use a polling policy to test the global variables _dma_busy[i] 
-// and detect the transfer completion.  
-// There is  NB_DMA channels, that are indexed by the dma_id stored in the 
-// task context.
-// The _dma_busy[i] synchronisation variables (one per channel) are set by the OS, 
-// and reset by the DMA ISR.
+// controlers (distributed in the clusters) to transfer data 
+// between the user buffer and the frame buffer. A  DMA channel is
+// allocated to each task requesting it in the mapping_info data structure.
 //////////////////////////////////////////////////////////////////////////////////
 
@@ -697,16 +748,16 @@
                              unsigned int 	length )
 {
-    volatile unsigned char *fb_address;
 
     // buffer must be mapped in user space 
     if ( ((unsigned int)buffer + length ) >= 0x80000000 )
+    {
         return 1;
-
-    fb_address = (unsigned char*)&seg_fb_base + offset;
-
-    // buffer copy 
-    memcpy((void*)fb_address, (void*)buffer, length);
-
-    return 0;
+    }
+    else
+    {
+        unsigned char *fb_address = (unsigned char*)&seg_fb_base + offset;
+        memcpy((void*)fb_address, (void*)buffer, length);
+        return 0;
+    }
 }
 
@@ -724,22 +775,21 @@
                             unsigned int 	length )
 {
-    volatile unsigned char *fb_address;
-
     // buffer must be mapped in user space 
     if ( ((unsigned int)buffer + length ) >= 0x80000000 )
+    {
         return 1;
-
-    fb_address = (unsigned char*)&seg_fb_base + offset;
-
-    // buffer copy 
-    memcpy((void*)buffer, (void*)fb_address, length);
-
-    return 0;
-}
-
-//////////////////////////////////////////////////////////////////////////////////
-// _fb_access()
-// Transfer data between a memory buffer and the frame_buffer device using DMA.
-// - to_mem     : from frame buffer to memory when true.
+    }
+    else
+    {
+        unsigned char *fb_address = (unsigned char*)&seg_fb_base + offset;
+        memcpy((void*)buffer, (void*)fb_address, length);
+        return 0;
+    }
+}
+
+//////////////////////////////////////////////////////////////////////////////////
+// _fb_dma_access()
+// Transfer data between a user buffer and the frame_buffer using DMA.
+// - to_user    : from frame buffer to user buffer when true.
 // - offset     : offset (in bytes) in the frame buffer.
 // - user_vaddr : virtual base address of the memory buffer.
@@ -747,56 +797,98 @@
 // The memory buffer must be mapped in user address space and word-aligned.
 // The user buffer length must be multiple of 4 bytes. 
-// Returns 0 if success, > 0 if error.
-//////////////////////////////////////////////////////////////////////////////////
-unsigned int _fb_access( unsigned int 	to_mem,
-                         unsigned int   offset,
-                         unsigned int   user_vaddr,
-                         unsigned int   length )
-{
-    static_scheduler_t*	psched;		// pointer on the current task scheduler
-    unsigned char*		fb_base;	// frame buffer base address
-    unsigned int*		dma_base;	// dma component base address
-    unsigned int		task_id;	// task local index (for scheduler)
-    unsigned int		dma_id;		// DMA channel index
-    unsigned int		vpn;		// current virtual page number
-    unsigned int		flags;		// protection flags
-    unsigned int		ppn;		// current physical page number
-    unsigned int		buf_base;	// buffer base address for DMA access
-    unsigned int		ppn_first;	// first physical page index for user buffer
-
-    fb_base  = (unsigned char*)&seg_fb_base + offset;
-
-    psched   = &_scheduler[_procid()];
-    task_id  = psched->current;
-    dma_id   = psched->context[task_id][CTX_FBDMA_ID];
-    dma_base = (unsigned int*)&seg_dma_base + (dma_id * DMA_SPAN);
-
-    // check buffer address and ength alignment
-    if ( user_vaddr & 0x3 ) return 1;
-    if ( length     & 0x3 ) return 1;
+// Me must compute the physical base addresses for both the frame buffer
+// and the user buffer before programming the DMA transfer.
+// The GIET being fully static, we don't need to split the transfer in 4Kbytes
+// pages, because the user buffer is contiguous in physical space.
+// Returns 0 if success, > 0 if error.
+//////////////////////////////////////////////////////////////////////////////////
+unsigned int _fb_dma_access( unsigned int 	to_user,
+                             unsigned int   offset,
+                             unsigned int   user_vaddr,
+                             unsigned int   length )
+{
+    unsigned int	ko;				// unsuccessfull V2P translation
+    unsigned int	flags;			// protection flags
+    unsigned int	ppn;			// physical page number
+    unsigned int    user_pbase;		// user buffer pbase address
+    unsigned int    fb_pbase;		// frame buffer pbase address
+
+    // get DMA channel and compute DMA vbase address
+    unsigned int	dma_id     = _get_current_context_slot(CTX_FBDMA_ID);
+    unsigned int    cluster_id = dma_id / NB_DMAS_MAX;
+    unsigned int    loc_id     = dma_id % NB_DMAS_MAX;
+    unsigned int*	dma_base   = (unsigned int*)&seg_dma_base +
+                                 (cluster_id * CLUSTER_SPAN) + 
+                                 (loc_id * DMA_SPAN);
+
+    // check user buffer address and length alignment
+    if ( (user_vaddr & 0x3) || (length & 0x3) )
+    {
+        _puts("[GIET ERROR] in _fbdma_access() : user buffer not word aligned\n");
+        return 1;
+    }
 
     // get user space page table virtual address
-    unsigned int user_ptp = psched->context[task_id][CTX_PTAB_ID];
-
+    unsigned int	user_ptab = _get_current_context_slot(CTX_PTAB_ID);
+
+    // compute frame buffer pbase address
+    unsigned int fb_vaddr = (unsigned int)&seg_fb_base + offset;
+
+    ko = _v2p_translate( (page_table_t*)user_ptab,
+                         (fb_vaddr >> 12),
+                         &ppn,
+                         &flags );
+    fb_pbase = (ppn << 12) | (fb_vaddr & 0x00000FFF);
+
+    if ( ko )
+    {
+        _puts("[GIET ERROR] in _fbdma_access() : frame buffer unmapped\n");
+        return 2;
+    }
+
+    // Compute user buffer pbase address
+    ko = _v2p_translate( (page_table_t*)user_ptab,
+                         (user_vaddr >> 12),
+                         &ppn,
+                         &flags );
+    user_pbase = (ppn << 12) | (user_vaddr & 0x00000FFF);
+
+    if ( ko )
+    {
+        _puts("[GIET ERROR] in _fbdma_access() : user buffer unmapped\n");
+        return 3;
+    } 
+    if ( (flags & PTE_U) == 0 )
+    {
+        _puts("[GIET ERROR] in _fbdma_access() : user buffer not in user space\n");
+        return 4; 
+    }
+    if ( ( (flags & PTE_W) == 0 ) && to_user ) 
+    {
+        _puts("[GIET ERROR] in _fbdma_access() : user buffer not writable\n");
+        return 5;
+    }
+
+
+
+/*
+    // loop on all virtual pages covering the user buffer
     unsigned int user_vpn_min = user_vaddr >> 12;
     unsigned int user_vpn_max = (user_vaddr + length - 1) >> 12;
     unsigned int ix2          = 0;
     unsigned int ix1          = _dma_iommu_ix1 + dma_id;
-    unsigned int ko;
-    unsigned int i;
-
-    // loop on all virtual pages covering the user buffer
+
     for ( vpn = user_vpn_min ; vpn <= user_vpn_max ; vpn++ )
     {
         // get ppn and flags for each vpn
-        ko = _v2p_translate( (page_table_t*)user_ptp,
-                             vpn,
-                             &ppn,
-                             &flags );
+        unsigned int ko = _v2p_translate( (page_table_t*)user_pt_vbase,
+                                          vpn,
+                                          &ppn,
+                                          &flags );
 
         // check access rights
-        if ( ko )                                 return 2;     // unmapped
-        if ( (flags & PTE_U) == 0 )               return 3;     // not in user space
-        if ( ( (flags & PTE_W) == 0 ) && to_mem ) return 4;     // not writable
+        if ( ko )                                 return 3;     // unmapped
+        if ( (flags & PTE_U) == 0 )               return 4;     // not in user space
+        if ( ( (flags & PTE_W) == 0 ) && to_user ) return 5;     // not writable
 
         // save first ppn value
@@ -816,5 +908,5 @@
         else            // no IOMMU : check that physical pages are contiguous
         {
-            if ( (ppn - ppn_first) != ix2 )       return 5;     // split physical buffer  
+            if ( (ppn - ppn_first) != ix2 )       return 6;     // split physical buffer  
         }
 
@@ -823,37 +915,24 @@
     } // end for vpn
 
-    // register the number of pages to be unmapped
+    // register the number of pages to be unmapped if iommu activated
     _dma_iommu_npages[dma_id] = (user_vpn_max - user_vpn_min) + 1;
 
+*/
     // invalidate data cache in case of memory write
-    if ( to_mem ) _dcache_buf_invalidate( (void*)user_vaddr, length );
-
-    // compute buffer base address for DMA depending on IOMMU activation
-    if ( GIET_IOMMU_ACTIVE ) buf_base = ( ix1 ) << 21 | (user_vaddr & 0xFFF);
-    else                     buf_base = (ppn_first << 12) | (user_vaddr & 0xFFF);
-
-
-    // waiting until DMA device is available 
-    while (_dma_busy[dma_id] != 0)
-    {
-        // busy wait with a pseudo random delay between bus access
-        unsigned int delay = (_proctime() & 0xF) << 4;
-        for (i = 0; i < delay; i++)
-            asm volatile("nop");
-    }
-
-    _dma_busy[dma_id] = 1;
+    if ( to_user ) _dcache_buf_invalidate( (void*)user_vaddr, length );
+
+    // get the lock 
+    _get_lock( &_dma_lock[dma_id] );
 
     // DMA configuration 
-    dma_base[DMA_IRQ_DISABLE] = 0;
-    if ( to_mem )
-    {
-        dma_base[DMA_SRC] = (unsigned int)fb_base;
-        dma_base[DMA_DST] = (unsigned int)buf_base;
+    if ( to_user )
+    {
+        dma_base[DMA_SRC] = (unsigned int)fb_pbase;
+        dma_base[DMA_DST] = (unsigned int)user_pbase;
     }
     else
     {
-        dma_base[DMA_SRC] = (unsigned int)buf_base;
-        dma_base[DMA_DST] = (unsigned int)fb_base;
+        dma_base[DMA_SRC] = (unsigned int)user_pbase;
+        dma_base[DMA_DST] = (unsigned int)fb_pbase;
     }
     dma_base[DMA_LEN] = (unsigned int)length;
@@ -873,8 +952,8 @@
                         unsigned int 	length )
 {
-    return _fb_access( 0,						// write to frame buffer
-                       offset,
-                       (unsigned int)buffer,
-                       length );	
+    return _fb_dma_access( 0,						// write to frame buffer
+                           offset,
+                           (unsigned int)buffer,
+                           length );	
 }
 
@@ -891,8 +970,8 @@
                        unsigned int 	length )
 {
-    return _fb_access( 1,						// read from frame buffer
-                       offset,
-                       (unsigned int)buffer,
-                       length );	
+    return _fb_dma_access( 1,						// read from frame buffer
+                           offset,
+                           (unsigned int)buffer,
+                           length );	
 }
 
@@ -906,14 +985,11 @@
 unsigned int _fb_completed()
 {
-    static_scheduler_t* psched  = &_scheduler[_procid()];
-    unsigned int        task_id = psched->current;
-
-    volatile unsigned int   dma_id  = psched->context[task_id][CTX_FBDMA_ID];
+    unsigned int dma_id = _get_current_context_slot(CTX_FBDMA_ID);
 
     // busy waiting with a pseudo random delay between bus access
-    while (_dma_busy[dma_id] != 0)
+    while (_dma_done[dma_id] == 0)
     {
 	    unsigned int i;
-        unsigned int delay = (_proctime() & 0xF) << 4;
+        unsigned int delay = ( _proctime() ^ _procid()<<4 ) & 0xFF;
         for (i = 0; i < delay; i++)
             asm volatile("nop");
@@ -938,4 +1014,8 @@
     }
 
+    // reset synchronization variables
+    _dma_lock[dma_id] = 0;
+    _dma_done[dma_id] = 0;
+
     return _dma_status[dma_id];
 }
