Changeset 238 for soft/giet_vm/sys/drivers.c

Timestamp:

May 29, 2013, 1:24:09 AM (11 years ago)

Author:

alain

Message:

Major evolution to support physical addresses larger than 32 bits.
The map.xml format has been modified: the vsegs associated to schedulers
are now explicitely defined and mapped in the page tables.

File:

• soft/giet_vm/sys/drivers.c (modified) (58 diffs)

soft/giet_vm/sys/drivers.c

@@ -1 +1 @@
 ///////////////////////////////////////////////////////////////////////////////////
 // File     : drivers.c
-// Date     : 01/04/2012
+// Date     : 23/05/2013
 // Author   : alain greiner
 // Copyright (c) UPMC-LIP6
@@ -16 +16 @@
 // - vci_block_device
 //
-// The following global parameters must be defined in the giet_config.h file:
-// - CLUSTER_SIZE
+// For the peripherals replicated in each cluster (ICU, TIMER, DMA),
+// the corresponding (virtual) base addresses must be completed by an offset 
+// depending on the cluster index.
+//
+// The following global parameter must be defined in the giet_config.h file:
+// - GIET_CLUSTER_INCREMENT
+//
+// The following global parameters must be defined in the hard_config.h file:
 // - NB_CLUSTERS   
 // - NB_PROCS_MAX  
-// - NB_TIMERS_MAX    
-// - NB_DMAS_MAX     
-// - NB_TTYS    
+// - NB_TIM_CHANNELS    
+// - NB_DMA_CHANNELS     
+// - NB_TTY_CHANNELS_MAX    
 //
 // The following virtual base addresses must be defined in the giet_vsegs.ld file:
 // - seg_icu_base
 // - seg_tim_base
+// - seg_dma_base
 // - seg_tty_base
 // - seg_gcd_base
-// - seg_dma_base
 // - seg_fbf_base
 // - seg_ioc_base
 // - seg_nic_base
-// As some peripherals can be replicated in the clusters (ICU, TIMER, DMA)
-// These addresses must be completed by an offset depending on the cluster index
-//    full_base_address = seg_***_base + cluster_id * CLUSTER_SIZE
+// - seg_cma_base
+// - seg_iob_base
+//
 ///////////////////////////////////////////////////////////////////////////////////
 
@@ -48 +54 @@
 
 #if !defined(NB_CLUSTERS) 
-# error: You must define NB_CLUSTERS in the configs file
+# error: You must define NB_CLUSTERS in the hard_config.h file
 #endif
 
 #if !defined(NB_PROCS_MAX) 
-# error: You must define NB_PROCS_MAX in the configs file
+# error: You must define NB_PROCS_MAX in the hard_config.h file
 #endif
 
@@ -59 +65 @@
 #endif
 
-#if !defined(CLUSTER_SIZE) 
-# error: You must define CLUSTER_SIZE in the configs file
-#endif
-
-#if !defined(NB_TTYS)
-# error: You must define NB_TTYS in the configs file
-#endif
-
-#if (NB_TTYS < 1)
-# error: NB_TTYS cannot be smaller than 1!
-#endif
-
-#if !defined(NB_DMAS_MAX)
-#define NB_DMAS_MAX 0
-#endif
-
-#if !defined(NB_TIMERS_MAX)
-#define NB_TIMERS_MAX 0
-#endif
-
-#if ( (NB_TIMERS_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 the configs file 
-#endif
-
-#if ( NB_IOCS > 1 )
-# error: NB_IOCS cannot be larger than 1
+#if !defined(GIET_CLUSTER_INCREMENT) 
+# error: You must define GIET_CLUSTER_INCREMENT in the giet_config.h file
+#endif
+
+#if !defined(NB_TTY_CHANNELS)
+# error: You must define NB_TTY_CHANNELS in the hard_config.h file
+#endif
+
+#if (NB_TTY_CHANNELS < 1)
+# error: NB_TTY_CHANNELS cannot be smaller than 1!
+#endif
+
+#if !defined(NB_DMA_CHANNELS)
+# error: You must define NB_DMA_CHANNELS in the hard_config.h file 
+#endif
+
+#if (NB_DMA_CHANNELS > 8)
+# error: NB_DMA_CHANNELS cannot be smaller than 8!
+#endif
+
+#if !defined(NB_TIM_CHANNELS)
+#define NB_TIM_CHANNELS 0
+#endif
+
+#if ( (NB_TIM_CHANNELS + NB_PROC_MAX) > 32 )
+# error: NB_TIM_CHANNELS + NB_PROCS_MAX cannot be larger than 32
+#endif
+
+#if !defined(NB_IOC_CHANNELS)
+# error: You must define NB_IOC_CHANNELS in the hard_config.h file 
+#endif
+
+#if ( NB_IOC_CHANNELS > 8 )
+# error: NB_IOC_CHANNELS cannot be larger than 8
+#endif
+
+#if !defined(NB_NIC_CHANNELS)
+# error: You must define NB_NIC_CHANNELS in the hard_config.h file 
+#endif
+
+#if ( NB_NIC_CHANNELS > 8 )
+# error: NB_NIC_CHANNELS cannot be larger than 8
+#endif
+
+#if !defined(NB_CMA_CHANNELS)
+# error: You must define NB_CMA_CHANNELS in the hard_config.h file 
+#endif
+
+#if ( NB_CMA_CHANNELS > 8 )
+# error: NB_CMA_CHANNELS cannot be larger than 8
 #endif
 
 #if !defined( USE_XICU )
-# error: You must define USE_XICU in the configs file
+# error: You must define USE_XICU in the hard_config.h file
 #endif
 
 #if !defined( IOMMU_ACTIVE )
-# error: You must define IOMMU_ACTIVE in the configs file
+# error: You must define IOMMU_ACTIVE in the hard_config.h file
 #endif
 
@@ -105 +131 @@
 //     Timers driver
 //////////////////////////////////////////////////////////////////////////////
+// This peripheral is replicated in all clusters.
 // The timers can be implemented in a vci_timer component or in a vci_xicu 
 // component (depending on the USE_XICU parameter).
@@ -113 +140 @@
 // - "user" timers : requested by the task in the mapping_info data structure.
 //   For each user timer, the timer_id is stored in the context of the task.
-// The global index is cluster_id * (NB_PROCS_MAX+NB_TIMERS_MAX) + local_id
+// The global index is cluster_id * (NB_PROCS_MAX+NB_TIM_CHANNELS) + local_id
 //////////////////////////////////////////////////////////////////////////////
+// The (virtual) base address of the associated segment is:
+//
+//       timer_address = seg_icu_base + cluster_id * GIET_CLUSTER_INCREMENT
+//
+// - cluster id is an explicit argument of all access functions
+// - seg_icu_base must be defined in the giet_vsegs.ld file
+// - GIET_CLUSTER_INCREMENT must be defined in the giet_config.h file
+////////////////////////////////////////////////////////////////////////////////
 
 // 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 };
+#if (NB_TIM_CHANNELS > 0)
+in_unckdata volatile unsigned char _user_timer_event[NB_CLUSTERS * NB_TIM_CHANNELS] 
+                            = { [0 ... ((NB_CLUSTERS * NB_TIM_CHANNELS) - 1)] = 0 };
 #endif
 
@@ -131 +166 @@
 // Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////
-unsigned int _timer_start(unsigned int cluster_id, unsigned int local_id, unsigned int period) {
+unsigned int _timer_start( unsigned int cluster_id, 
+                           unsigned int local_id, 
+                           unsigned int period) 
+{
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (local_id >= NB_TIMERS_MAX) {
-        return 2;
-    }
+    if (cluster_id >= NB_CLUSTERS)  return 1;
+    if (local_id >= NB_TIM_CHANNELS)  return 2;
 
 #if USE_XICU
-    unsigned int * timer_address = (unsigned int *) ((char *) &seg_icu_base + (cluster_id * CLUSTER_SIZE));
+    unsigned int * timer_address = (unsigned int *) ((char *) &seg_icu_base + 
+                                                     (cluster_id * GIET_CLUSTER_INCREMENT));
 
     timer_address[XICU_REG(XICU_PTI_PER, local_id)] = period;
 #else
-    unsigned int* timer_address = (unsigned int *) ((char *) &seg_tim_base + (cluster_id * CLUSTER_SIZE));
+    unsigned int* timer_address = (unsigned int *) ((char *) &seg_tim_base + 
+                                                    (cluster_id * GIET_CLUSTER_INCREMENT));
 
     timer_address[local_id * TIMER_SPAN + TIMER_PERIOD] = period;
@@ -152 +188 @@
     return 0;
 }
-
 
 //////////////////////////////////////////////////////////////////////////////
@@ -160 +195 @@
 // Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////
-unsigned int _timer_stop(unsigned int cluster_id, unsigned int local_id) {
+unsigned int _timer_stop( unsigned int cluster_id, 
+                          unsigned int local_id) 
+{
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (local_id >= NB_TIMERS_MAX) {
-        return 2;
-    }
+    if (cluster_id >= NB_CLUSTERS)  return 1;
+    if (local_id >= NB_TIM_CHANNELS)  return 2;
 
 #if USE_XICU
-    unsigned int * timer_address = (unsigned int *) ((char *) &seg_icu_base + (cluster_id * CLUSTER_SIZE));
+    unsigned int * timer_address = (unsigned int *) ((char *) &seg_icu_base + 
+                                                     (cluster_id * GIET_CLUSTER_INCREMENT));
 
     timer_address[XICU_REG(XICU_PTI_PER, local_id)] = 0;
 #else
-    unsigned int* timer_address = (unsigned int *) ((char *) &seg_tim_base + (cluster_id * CLUSTER_SIZE));
+    unsigned int* timer_address = (unsigned int *) ((char *) &seg_tim_base + 
+                                                    (cluster_id * GIET_CLUSTER_INCREMENT));
+
     timer_address[local_id * TIMER_SPAN + TIMER_MODE] = 0;
 #endif
@@ -189 +225 @@
 // Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////
-unsigned int _timer_reset_irq(unsigned int cluster_id, unsigned int local_id) {
+unsigned int _timer_reset_irq( unsigned int cluster_id, 
+                               unsigned int local_id ) 
+{
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (local_id >= NB_TIMERS_MAX) {
-        return 2;
-    }
+    if (cluster_id >= NB_CLUSTERS)  return 1;
+    if (local_id >= NB_TIM_CHANNELS)  return 2;
 
 #if USE_XICU
     unsigned int * timer_address = (unsigned int *) ((char *) &seg_icu_base +
-            (cluster_id * (unsigned) CLUSTER_SIZE));
+                                                     (cluster_id * GIET_CLUSTER_INCREMENT));
 
     unsigned int bloup = timer_address[XICU_REG(XICU_PTI_ACK, local_id)];
@@ -206 +240 @@
 #else
     unsigned int * timer_address = (unsigned int *) ((char *) &seg_tim_base + 
-            (cluster_id * CLUSTER_SIZE));
+            (cluster_id * GIET_CLUSTER_INCREMENT));
 
     timer_address[local_id * TIMER_SPAN + TIMER_RESETIRQ] = 0;
 #endif
-
     return 0;
 }
@@ -223 +256 @@
 //        return 1;
 //    }
-//    if (local_id >= NB_TIMERS_MAX) {
+//    if (local_id >= NB_TIM_CHANNELS) {
 //        return 2;
 //    }
@@ -230 +263 @@
 //#error // not implemented
 //#else
-//    unsigned int * timer_address = (unsigned int *) ((char *) &seg_tim_base + (cluster_id * CLUSTER_SIZE));
+//    unsigned int * timer_address = (unsigned int *) ((char *) &seg_tim_base + (cluster_id * GIET_CLUSTER_INCREMENT));
 //    unsigned int timer_period = timer_address[local_id * TIMER_SPAN + TIMER_PERIOD];
 //
@@ -244 +277 @@
 /////////////////////////////////////////////////////////////////////////////////
 // There is only one multi_tty controler in the architecture.
-// The total number of TTYs is defined by the configuration parameter NB_TTYS.
+// The total number of TTYs is defined by the configuration parameter NB_TTY_CHANNELS.
 // The "system" terminal is TTY[0].
 // The "user" TTYs are allocated to applications by the GIET in the boot phase,
@@ -253 +286 @@
 
 // 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 volatile unsigned char _tty_get_buf[NB_TTY_CHANNELS];
+in_unckdata volatile unsigned char _tty_get_full[NB_TTY_CHANNELS] 
+                                     = { [0 ... NB_TTY_CHANNELS - 1] = 0 };
 in_unckdata unsigned int _tty_put_lock = 0;  // protect kernel TTY[0]
 
@@ -260 +294 @@
 //      _tty_error()
 ////////////////////////////////////////////////////////////////////////////////
-void _tty_error(unsigned int tty_id, unsigned int task_id) {
+void _tty_error(unsigned int tty_id, unsigned int task_id) 
+{
     unsigned int proc_id = _procid();
 
@@ -287 +322 @@
 // The function returns  the number of characters that have been written.
 /////////////////////////////////////////////////////////////////////////////////
-unsigned int _tty_write(const char * buffer, unsigned int length) {
+unsigned int _tty_write(const char * buffer, 
+                        unsigned int length) 
+{
     unsigned int nwritten;
-    unsigned int task_id = _get_proc_task_id();
-    unsigned int tty_id = _get_context_slot(task_id, CTX_TTY_ID);
-
-    if (tty_id >= NB_TTYS) {
-        _tty_error(tty_id , task_id);
-        return 0;
-    }
-
-    unsigned int * tty_address = (unsigned int *) &seg_tty_base;
-
-    for (nwritten = 0; nwritten < length; nwritten++) {
+    unsigned int tty_id = _get_context_slot(CTX_TTY_ID);
+    unsigned int* tty_address = (unsigned int *) &seg_tty_base;
+
+    for (nwritten = 0; nwritten < length; nwritten++) 
+    {
         // check tty's status 
-        if ((tty_address[tty_id * TTY_SPAN + TTY_STATUS] & 0x2) == 0x2) {
-            break;
-        }
-        else {
-            // write character 
-            tty_address[tty_id * TTY_SPAN + TTY_WRITE] = (unsigned int) buffer[nwritten];
-        }
+        if ((tty_address[tty_id * TTY_SPAN + TTY_STATUS] & 0x2) == 0x2) break;
+        tty_address[tty_id * TTY_SPAN + TTY_WRITE] = (unsigned int) buffer[nwritten];
     }
     return nwritten;
 }
-
 
 //////////////////////////////////////////////////////////////////////////////
@@ -324 +349 @@
 // Returns 0 if the kernel buffer is empty, 1 if the buffer is full.
 //////////////////////////////////////////////////////////////////////////////
-unsigned int _tty_read(char * buffer, unsigned int length) {
-    unsigned int task_id = _get_proc_task_id();
-    unsigned int tty_id = _get_context_slot(task_id, CTX_TTY_ID);
-
-    if (tty_id >= NB_TTYS) {
-        _tty_error(tty_id, task_id);
+unsigned int _tty_read(char * buffer, 
+                       unsigned int length) 
+{
+    unsigned int tty_id = _get_context_slot(CTX_TTY_ID);
+
+    if (_tty_get_full[tty_id] == 0) 
+    {
         return 0;
     }
-
-    if (_tty_get_full[tty_id] == 0) {
-        return 0;
-    }
-    else {
+    else 
+    {
         *buffer = _tty_get_buf[tty_id];
         _tty_get_full[tty_id] = 0;
@@ -342 +365 @@
     }
 }
-
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -351 +373 @@
 // Returns 0 if success, 1 if tty_id too large. 
 ////////////////////////////////////////////////////////////////////////////////
-unsigned int _tty_get_char(unsigned int tty_id, unsigned char * buffer) {
+unsigned int _tty_get_char(unsigned int tty_id, 
+                           unsigned char * buffer) 
+{
     // checking argument
-    if (tty_id >= NB_TTYS) {
-        return 1;
-    }
+    if (tty_id >= NB_TTY_CHANNELS) { return 1; }
 
     // compute terminal base address 
@@ -366 +388 @@
 
 ////////////////////////////////////////////////////////////////////////////////
-//     VciMultiIcu and VciXicu drivers
-////////////////////////////////////////////////////////////////////////////////
+//     VciMultiIcu or VciXicu driver
+////////////////////////////////////////////////////////////////////////////////
+// This hardware component is replicated in all clusters.
 // There is 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.
+// because there is one private interrupt controler per processor.
+////////////////////////////////////////////////////////////////////////////////
+// The (virtual) base address of the associated segment is:
+//
+//       icu_address = seg_icu_base + cluster_id * GIET_CLUSTER_INCREMENT
+//
+// - cluster id is an explicit argument of all access functions
+// - seg_icu_base must be defined in the giet_vsegs.ld file
+// - GIET_CLUSTER_INCREMENT must be defined in the giet_config.h file
 ////////////////////////////////////////////////////////////////////////////////
 
@@ -380 +411 @@
 // Returns 0 if success, > 0 if error.
 ////////////////////////////////////////////////////////////////////////////////
-unsigned int _icu_set_mask(
-        unsigned int cluster_id,
-        unsigned int proc_id,
-        unsigned int value,
-        unsigned int is_timer) {
+unsigned int _icu_set_mask( unsigned int cluster_id,
+                            unsigned int proc_id,
+                            unsigned int value,
+                            unsigned int is_timer) 
+{
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (proc_id >= NB_PROCS_MAX) {
-        return 1;
-    }
+    if (cluster_id >= NB_CLUSTERS) return 1; 
+    if (proc_id >= NB_PROCS_MAX)   return 1; 
 
     unsigned int * icu_address = (unsigned int *) ((char *) &seg_icu_base + 
-            (cluster_id * (unsigned) CLUSTER_SIZE));
+                                                   (cluster_id * GIET_CLUSTER_INCREMENT));
 #if USE_XICU
-    if (is_timer) {
+    if (is_timer) 
+    {
         icu_address[XICU_REG(XICU_MSK_PTI_ENABLE, proc_id)] = value;
     }
-    else {
+    else 
+    {
         icu_address[XICU_REG(XICU_MSK_HWI_ENABLE, proc_id)] = value;
     }
@@ -405 +434 @@
     icu_address[proc_id * ICU_SPAN + ICU_MASK_SET] = value; 
 #endif
-
     return 0;
 }
@@ -417 +445 @@
 // Returns 0 if success, > 0 if error.
 ////////////////////////////////////////////////////////////////////////////////
-unsigned int _icu_get_index(unsigned int cluster_id, unsigned int proc_id, unsigned int * buffer) {
+unsigned int _icu_get_index( unsigned int cluster_id, 
+                             unsigned int proc_id, 
+                             unsigned int * buffer) 
+{
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (proc_id >= NB_PROCS_MAX) {
-        return 1;
-    }
+    if (cluster_id >= NB_CLUSTERS)  return 1;
+    if (proc_id >= NB_PROCS_MAX)    return 1;
 
     unsigned int * icu_address = (unsigned int *) ((char *) &seg_icu_base + 
-            (cluster_id * (unsigned) CLUSTER_SIZE));
+                                                   (cluster_id * GIET_CLUSTER_INCREMENT));
 #if USE_XICU
     unsigned int prio = icu_address[XICU_REG(XICU_PRIO, proc_id)];
@@ -436 +463 @@
     unsigned int hwi_id = (prio & 0x001F0000) >> 16;
     unsigned int swi_id = (prio & 0x1F000000) >> 24;
-    if (pti_ok) {
-        *buffer = pti_id;
-    }
-    else if (hwi_ok) {
-        *buffer = hwi_id;
-    }
-    else if (swi_ok) {
-        *buffer = swi_id;
-    }
-    else {
-        *buffer = 32;
-    }
+    if      (pti_ok) { *buffer = pti_id; }
+    else if (hwi_ok) { *buffer = hwi_id; }
+    else if (swi_ok) { *buffer = swi_id; }
+    else             { *buffer = 32; }
 #else
     *buffer = icu_address[proc_id * ICU_SPAN + ICU_IT_VECTOR]; 
 #endif
-
     return 0;
 }
@@ -469 +487 @@
 // Returns 0 if success, > 0 if error.
 ////////////////////////////////////////////////////////////////////////////////
-unsigned int _gcd_write(unsigned int register_index, unsigned int value) {
+unsigned int _gcd_write( unsigned int register_index, 
+                         unsigned int value) 
+{
     // parameters checking
-    if (register_index >= GCD_END) {
-        return 1;
-    }
+    if (register_index >= GCD_END)  return 1; 
 
     unsigned int * gcd_address = (unsigned int *) &seg_gcd_base;
@@ -487 +505 @@
 // Returns 0 if success, > 0 if error.
 ////////////////////////////////////////////////////////////////////////////////
-unsigned int _gcd_read(unsigned int register_index, unsigned int * buffer) {
+unsigned int _gcd_read( unsigned int register_index, 
+                        unsigned int * buffer ) 
+{
     // parameters checking 
-    if (register_index >= GCD_END) {
-        return 1;
-    }
+    if (register_index >= GCD_END)  return 1;
 
     unsigned int * gcd_address = (unsigned int *) &seg_gcd_base;
@@ -567 +585 @@
 // Returns 0 if success, > 0 if error.
 ///////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_access(
-        unsigned int to_mem,
-        unsigned int lba,
-        unsigned int user_vaddr,
-        unsigned int count) {
-    unsigned int user_vpn_min; // first virtuel page index in user space
-    unsigned int user_vpn_max; // last virtual page index in user space
-    unsigned int vpn;          // current virtual page index in user space
-    unsigned int ppn;          // physical page number
-    unsigned int flags;        // page protection flags
-    unsigned int ix2;          // page index in IOMMU PT1 page table
-    unsigned int addr;         // buffer address for IOC peripheral
-    unsigned int ppn_first;    // first physical page number for user buffer
-
+unsigned int _ioc_access( unsigned int to_mem,
+                          unsigned int lba,
+                          unsigned int user_vaddr,
+                          unsigned int count) 
+{
+    unsigned int user_vpn_min;     // first virtuel page index in user space
+    unsigned int user_vpn_max;     // last virtual page index in user space
+    unsigned int vpn;              // current virtual page index in user space
+    unsigned int ppn;              // physical page number
+    unsigned int flags;            // page protection flags
+    unsigned int ix2;              // page index in IOMMU PT1 page table
+    unsigned int ppn_first;        // first physical page number for user buffer
+    unsigned int buf_xaddr = 0;    // user buffer virtual address in IO space (if IOMMU)
+    paddr_t      buf_paddr = 0;    // user buffer physical address (if no IOMMU),
+                               
     // check buffer alignment
-    if ((unsigned int) user_vaddr & 0x3) {
-        return 1;
+    if ((unsigned int) user_vaddr & 0x3)
+    {
+        _get_lock(&_tty_put_lock);
+        _puts("[GIET ERROR] in _ioc_access() : user buffer not word aligned\n");
+        _release_lock(&_tty_put_lock);
+        return 1; 
     }
 
@@ -592 +615 @@
 
     // get user space page table virtual address
-    unsigned int task_id = _get_proc_task_id();
-    unsigned int user_pt_vbase = _get_context_slot(task_id, CTX_PTAB_ID);
+    unsigned int user_pt_vbase = _get_context_slot(CTX_PTAB_ID);
 
     user_vpn_min = user_vaddr >> 12;
     user_vpn_max = (user_vaddr + length - 1) >> 12;
-    ix2 = 0;
 
     // loop on all virtual pages covering the user buffer
-    for (vpn = user_vpn_min; vpn <= user_vpn_max; vpn++) {
+    for (vpn = user_vpn_min, ix2 = 0 ; 
+         vpn <= user_vpn_max ; 
+         vpn++, ix2++ ) 
+    {
         // get ppn and flags for each vpn
-        unsigned int ko = _v2p_translate((page_table_t *) user_pt_vbase, 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 (ko)                                 
+        {
+            _get_lock(&_tty_put_lock);
+            _puts("[GIET ERROR] in _ioc_access() : user buffer unmapped\n");
+            _release_lock(&_tty_put_lock);
+            return 1; 
         }
-        if ((flags & PTE_U) == 0) {
-            return 3; // not in user space
+        if ((flags & PTE_U) == 0) 
+        {
+            _get_lock(&_tty_put_lock);
+            _puts("[GIET ERROR] in _ioc_access() : user buffer not in user space\n");
+            _release_lock(&_tty_put_lock);
+            return 1; 
         }
-        if (((flags & PTE_W) == 0 ) && to_mem) {
-            return 4; // not writable
+        if (((flags & PTE_W) == 0 ) && to_mem)
+        {
+            _get_lock(&_tty_put_lock);
+            _puts("[GIET ERROR] in _ioc_access() : user buffer not writable\n");
+            _release_lock(&_tty_put_lock);
+            return 1; 
         }
 
         // save first ppn value
-        if (ix2 == 0) {
-            ppn_first = ppn;
+        if (ix2 == 0) ppn_first = ppn;
+
+        if (IOMMU_ACTIVE) // the user buffer must be remapped in the I/0 space
+        {
+            // check buffer length < 2 Mbytes
+            if (ix2 > 511) 
+            {
+                _get_lock(&_tty_put_lock);
+                _puts("[GIET ERROR] in _ioc_access() : user buffer > 2 Mbytes\n");
+                _release_lock(&_tty_put_lock);
+                return 1; 
+            }
+
+            // map the physical page in IOMMU page table
+            _iommu_add_pte2( _ioc_iommu_ix1,    // PT1 index
+                             ix2,               // PT2 index
+                             ppn,               // Physical page number    
+                             flags);            // Protection flags
+
+            // compute user buffer virtual adress in IO space
+            buf_xaddr = (_ioc_iommu_ix1) << 21 | (user_vaddr & 0xFFF);
         }
-
-        if (IOMMU_ACTIVE) {
-            // the user buffer must be remapped in the I/0 space
-            // check buffer length < 2 Mbytes
-            if (ix2 > 511) {
-                return 2;
+        else            // No IOMMU
+        {
+            // check that physical pages are contiguous
+            if ((ppn - ppn_first) != ix2) 
+            {
+                _get_lock(&_tty_put_lock);
+                _puts("[GIET ERROR] in _ioc_access() : split physical user buffer\n");
+                _release_lock(&_tty_put_lock);
+                return 1; 
             }
 
-            // map the physical page in IOMMU page table
-            _iommu_add_pte2(
-                    _ioc_iommu_ix1,    // PT1 index
-                    ix2,               // PT2 index
-                    ppn,               // Physical page number    
-                    flags);            // Protection flags
+            // compute user buffer physical adress
+            buf_paddr = (((paddr_t)ppn_first) << 12) | (user_vaddr & 0xFFF);
         }
-        else {
-            // no IOMMU : check that physical pages are contiguous
-            if ((ppn - ppn_first) != ix2) {
-                return 5; // split physical buffer
-            }
-        }
-
-        // increment page index
-        ix2++;
     } // end for vpn
 
@@ -649 +696 @@
 
     // invalidate data cache in case of memory write
-    if (to_mem) {
-        _dcache_buf_invalidate((void *) user_vaddr, length);
-    }
-
-    // compute buffer base address for IOC depending on IOMMU activation
-    if (IOMMU_ACTIVE) {
-        addr = (_ioc_iommu_ix1) << 21 | (user_vaddr & 0xFFF);
-    }
-    else {
-        addr = (ppn_first << 12) | (user_vaddr & 0xFFF);
-    }
+    if (to_mem) _dcache_buf_invalidate((void *) user_vaddr, length);
+
+#if GIET_DEBUG_IOC_DRIVER
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG]  IOC_ACCESS at cycle ");
+_putd( _proctime() );
+_puts("\n - proc_id         = ");
+_putd( _procid() );
+_puts("\n - ioc_vbase       = ");
+_putx( (unsigned int)ioc_address );
+_puts("\n - psched_vbase    = ");
+_putx( (unsigned int)_get_sched() );
+_puts("\n - pt_vbase        = ");
+_putx( user_pt_vbase );
+_puts("\n - user_buf_vbase  = ");
+_putx( user_vaddr );
+_puts("\n - user_buf_length = ");
+_putx( length );
+_puts("\n - user_buf_paddr  = ");
+_putl( buf_paddr );
+_puts("\n - user_buf_xaddr  = ");
+_putx( buf_xaddr );
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
 
     // get the lock on ioc device 
@@ -665 +726 @@
 
     // peripheral configuration  
-    ioc_address[BLOCK_DEVICE_BUFFER] = addr;
+    if ( IOMMU_ACTIVE ) 
+    {
+        ioc_address[BLOCK_DEVICE_BUFFER] = buf_xaddr;
+    }
+    else
+    {
+        ioc_address[BLOCK_DEVICE_BUFFER]     = (unsigned int)buf_paddr;
+        ioc_address[BLOCK_DEVICE_BUFFER_EXT] = (unsigned int)(buf_paddr>>32);
+    }
     ioc_address[BLOCK_DEVICE_COUNT] = count;
     ioc_address[BLOCK_DEVICE_LBA] = lba;
-    if (to_mem == 0) {
+    if (to_mem == 0) 
+    {
         ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_WRITE;
     }
-    else {
+    else 
+    {
         ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_READ;
     }
-
-    return 0;
-}
-
+    return 0;
+}
 
 /////////////////////////////////////////////////////////////////////////////////
@@ -688 +757 @@
 // Returns 0 if success, > 0 if error.
 /////////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_completed() {
+unsigned int _ioc_completed() 
+{
     unsigned int ret;
     unsigned int ix2;
 
     // busy waiting
-    while (_ioc_done == 0) {
-        asm volatile("nop");
-    }
+    while (_ioc_done == 0) { asm volatile("nop"); }
+
+#if GIET_DEBUG_IOC_DRIVER
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG]  IOC_COMPLETED at cycle ");
+_putd( _proctime() );
+_puts("\n - proc_id         = ");
+_putd( _procid() );
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
 
     // unmap the buffer from IOMMU page table if IOMMU is activated
-    if (IOMMU_ACTIVE) {
+    if (IOMMU_ACTIVE) 
+    {
         unsigned int * iob_address = (unsigned int *) &seg_iob_base;
 
-        for (ix2 = 0; ix2 < _ioc_iommu_npages; ix2++) {
+        for (ix2 = 0; ix2 < _ioc_iommu_npages; ix2++) 
+        {
             // unmap the page in IOMMU page table
             _iommu_inval_pte2(
@@ -714 +794 @@
     // test IOC status 
     if ((_ioc_status != BLOCK_DEVICE_READ_SUCCESS)
-            && (_ioc_status != BLOCK_DEVICE_WRITE_SUCCESS)) {
-        ret = 1; // error
-    }
-    else {
-        ret = 0; // success
-    }
+            && (_ioc_status != BLOCK_DEVICE_WRITE_SUCCESS)) ret = 1; // error 
+    else                                                    ret = 0; // success
 
     // reset synchronization variables
@@ -738 +814 @@
 // Returns 0 if success, > 0 if error.
 ///////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_read(unsigned int lba, void * buffer, unsigned int count) {
+unsigned int _ioc_read( unsigned int lba, 
+                        void * buffer, 
+                        unsigned int count) 
+{
     return _ioc_access(
             1,        // read access
@@ -755 +834 @@
 // Returns 0 if success, > 0 if error.
 ///////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_write(unsigned int lba, const void * buffer, unsigned int count) {
+unsigned int _ioc_write( unsigned int lba, 
+                         const void * buffer, 
+                         unsigned int count) 
+{
     return _ioc_access(
             0, // write access
@@ -769 +851 @@
 // Returns 0 if success, > 0 if error.
 ///////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_get_status(unsigned int * status) {
+unsigned int _ioc_get_status(unsigned int * status) 
+{
     // get IOC base address
     unsigned int * ioc_address = (unsigned int *) &seg_ioc_base;
@@ -782 +865 @@
 // This function returns the block_size with which the IOC has been configured.
 ///////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_get_block_size() {
+unsigned int _ioc_get_block_size() 
+{
     // get IOC base address
     unsigned int * ioc_address = (unsigned int *) &seg_ioc_base;
@@ -794 +878 @@
 //////////////////////////////////////////////////////////////////////////////////
 // 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]
+// There is  (NB_CLUSTERS * NB_DMA_CHANNELS) channels, indexed by a global index:
+//        dma_id = cluster_id * NB_DMA_CHANNELS + loc_id
+//
+// As a DMA channel is a private ressource allocated to a task,
+// there is no lock protecting exclusive access to the channel.
 // 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];
+//////////////////////////////////////////////////////////////////////////////////
+// The (virtual) base address of the associated segment is:
+//
+//       dma_address = seg_dma_base + cluster_id * GIET_CLUSTER_INCREMENT
+//
+// - seg_dma_base  must be defined in the giet_vsegs.ld file
+// - GIET_CLUSTER_INCREMENT  must be defined in the giet_config.h file
+////////////////////////////////////////////////////////////////////////////////
+
+#if NB_DMA_CHANNELS > 0
+
+// in_unckdata unsigned int            _dma_lock[NB_DMA_CHANNELS * NB_CLUSTERS] 
+// = { [0 ... (NB_DMA_CHANNELS * NB_CLUSTERS) - 1] = 0 };
+
+in_unckdata volatile unsigned int    _dma_done[NB_DMA_CHANNELS * NB_CLUSTERS] 
+        = { [0 ... (NB_DMA_CHANNELS * NB_CLUSTERS) - 1] = 0 };
+in_unckdata volatile unsigned int _dma_status[NB_DMA_CHANNELS * NB_CLUSTERS];
 in_unckdata unsigned int _dma_iommu_ix1 = 1;
-in_unckdata unsigned int _dma_iommu_npages[NB_DMAS_MAX * NB_CLUSTERS];
+in_unckdata unsigned int _dma_iommu_npages[NB_DMA_CHANNELS * NB_CLUSTERS];
 #endif
 
@@ -823 +910 @@
 // _dma_reset_irq()
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _dma_reset_irq(unsigned int cluster_id, unsigned int channel_id) {
-#if NB_DMAS_MAX > 0
+unsigned int _dma_reset_irq( unsigned int cluster_id, 
+                             unsigned int channel_id) 
+{
+#if NB_DMA_CHANNELS > 0
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (channel_id >= NB_DMAS_MAX) {
-        return 1;
-    }
+    if (cluster_id >= NB_CLUSTERS)  return 1;
+    if (channel_id >= NB_DMA_CHANNELS)  return 1; 
 
     // compute DMA base address
     unsigned int * dma_address = (unsigned int *) ((char *) &seg_dma_base + 
-            (cluster_id * (unsigned) CLUSTER_SIZE));
+                                                   (cluster_id * GIET_CLUSTER_INCREMENT));
 
     dma_address[channel_id * DMA_SPAN + DMA_RESET] = 0;            
@@ -848 +933 @@
 // _dma_get_status()
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _dma_get_status(unsigned int cluster_id, unsigned int channel_id, unsigned int * status) {
-#if NB_DMAS_MAX > 0
+unsigned int _dma_get_status( unsigned int cluster_id, 
+                              unsigned int channel_id, 
+                              unsigned int * status) 
+{
+#if NB_DMA_CHANNELS > 0
     // parameters checking 
-    if (cluster_id >= NB_CLUSTERS) {
-        return 1;
-    }
-    if (channel_id >= NB_DMAS_MAX) {
-        return 1;
-    }
+    if (cluster_id >= NB_CLUSTERS)  return 1;
+    if (channel_id >= NB_DMA_CHANNELS)  return 1;
 
     // compute DMA base address
     unsigned int * dma_address = (unsigned int *) ((char *) &seg_dma_base + 
-            (cluster_id * (unsigned) CLUSTER_SIZE));
+                                                   (cluster_id * GIET_CLUSTER_INCREMENT));
 
     *status = dma_address[channel_id * DMA_SPAN + DMA_LEN];
@@ -873 +957 @@
 // _dma_transfer()
 // Transfer data between a user buffer and a device buffer using DMA.
-// Two devices types are supported: Frame Buffer if dev_type == 0
-//                                  Multi-Nic if dev_type != 0
+// Only one device type is supported: Frame Buffer (dev_type == 0)
 // Arguments are:
 // - dev_type     : device type.
@@ -882 +965 @@
 // - length       : number of bytes to be transfered.
 // 
-// The DMA channel is obtained from task context (CTX_FBDMA_ID / CTX_NIDMA_ID.
+// The cluster_id and channel_id are obtained from task context (CTX_DMA_ID).
 // The user buffer must be mapped in user address space and word-aligned.
 // The user buffer length must be multiple of 4 bytes. 
-// Me must compute the physical base addresses for both the device buffer
+// We compute the physical base addresses for both the device buffer
 // and the user buffer before programming the DMA transfer.
 // The GIET being fully static, we don't need to split the transfer in 4 Kbytes
@@ -891 +974 @@
 // Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _dma_transfer(
-        unsigned int dev_type,
-        unsigned int to_user,
-        unsigned int offset,
-        unsigned int user_vaddr,
-        unsigned int length) {
-#if NB_DMAS_MAX > 0
+unsigned int _dma_transfer( unsigned int dev_type,
+                            unsigned int to_user,
+                            unsigned int offset,
+                            unsigned int user_vaddr,
+                            unsigned int length ) 
+{
+#if NB_DMA_CHANNELS > 0
     unsigned int ko;           // unsuccessfull V2P translation
+    unsigned int device_vbase; // device buffer vbase address
     unsigned int flags;        // protection flags
     unsigned int ppn;          // physical page number
-    unsigned int user_pbase;   // user buffer pbase address
-    unsigned int device_pbase; // frame buffer pbase address
-    unsigned int device_vaddr; // device buffer vbase address
+    paddr_t      user_pbase;   // user buffer pbase address
+    paddr_t      device_pbase; // frame buffer pbase address
 
     // check user buffer address and length alignment
-    if ((user_vaddr & 0x3) || (length & 0x3)) {
+    if ((user_vaddr & 0x3) || (length & 0x3)) 
+    {
         _get_lock(&_tty_put_lock);
         _puts("\n[GIET ERROR] in _dma_transfer : user buffer not word aligned\n");
@@ -914 +998 @@
 
     // get DMA channel and compute DMA vbase address
-    unsigned int task_id    = _get_proc_task_id();
-    unsigned int dma_id     = _get_context_slot(task_id, CTX_DMA_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 *) ((char *) &seg_dma_base + 
-            (cluster_id * (unsigned) CLUSTER_SIZE));
-
+    unsigned int dma_id      = _get_context_slot(CTX_DMA_ID);
+    if ( dma_id == 0xFFFFFFFF )
+    {
+        _get_lock(&_tty_put_lock);
+        _puts("\n[GIET ERROR] in _dma_transfer : no DMA channel allocated\n");
+        _release_lock(&_tty_put_lock);
+        return 1;
+    }
+    unsigned int cluster_id  = dma_id / NB_DMA_CHANNELS;
+    unsigned int channel_id  = dma_id % NB_DMA_CHANNELS;
+    unsigned int * dma_vbase  = (unsigned int *) ((char *) &seg_dma_base + 
+                                                (cluster_id * GIET_CLUSTER_INCREMENT));
     // get page table address
-    unsigned int user_ptab = _get_context_slot(task_id, CTX_PTAB_ID);
-
-    // get peripheral buffer virtual address
-    if (dev_type) {
-        device_vaddr = (unsigned int) &seg_nic_base + offset;
-    }
-    else {
-        device_vaddr = (unsigned int) &seg_fbf_base + offset;
+    unsigned int user_ptab = _get_context_slot(CTX_PTAB_ID);
+
+    // get devic buffer virtual address, depending on peripheral type
+    if (dev_type == 0) 
+    {
+        device_vbase = (unsigned int) &seg_fbf_base + offset;
+    }
+    else 
+    {
+        _get_lock(&_tty_put_lock);
+        _puts("\n[GIET ERROR] in _dma_transfer : device type not supported\n");
+        _release_lock(&_tty_put_lock);
+        return 1;
     }
 
     // get device buffer physical address
-    ko = _v2p_translate((page_table_t *) user_ptab, (device_vaddr >> 12), &ppn, &flags);
-    if (ko) {
+    ko = _v2p_translate( (page_table_t*) user_ptab, 
+                         (device_vbase >> 12), 
+                         &ppn, 
+                         &flags );
+    if (ko) 
+    {
         _get_lock(&_tty_put_lock);
         _puts("\n[GIET ERROR] in _dma_transfer : device buffer unmapped\n");
         _release_lock(&_tty_put_lock);
-        return 2;
-    }
-    device_pbase = (ppn << 12) | (device_vaddr & 0x00000FFF);
+        return 1;
+    }
+    device_pbase = ((paddr_t)ppn << 12) | (device_vbase & 0x00000FFF);
 
     // Compute user buffer physical address
-    ko = _v2p_translate((page_table_t*) user_ptab, (user_vaddr >> 12), &ppn, &flags);
-    if (ko) {
+    ko = _v2p_translate( (page_table_t*) user_ptab, 
+                         (user_vaddr >> 12), 
+                         &ppn, 
+                         &flags );
+    if (ko) 
+    {
         _get_lock(&_tty_put_lock);
         _puts("\n[GIET ERROR] in _dma_transfer() : user buffer unmapped\n");
         _release_lock(&_tty_put_lock);
-        return 3;
+        return 1;
     } 
-    if ((flags & PTE_U) == 0) {
+    if ((flags & PTE_U) == 0) 
+    {
         _get_lock(&_tty_put_lock);
         _puts("[GIET ERROR] in _dma_transfer() : user buffer not in user space\n");
         _release_lock(&_tty_put_lock);
-        return 4; 
-    }
-    if (((flags & PTE_W) == 0 ) && to_user) {
+        return 1; 
+    }
+    if (((flags & PTE_W) == 0 ) && to_user) 
+    {
         _get_lock(&_tty_put_lock);
         _puts("\n[GIET ERROR] in _dma_transfer() : user buffer not writable\n");
         _release_lock(&_tty_put_lock);
-        return 5;
-    }
-    user_pbase = (ppn << 12) | (user_vaddr & 0x00000FFF);
-
-    /*  This is a draft for IOMMU support
+        return 1;
+    }
+    user_pbase = (((paddr_t)ppn) << 12) | (user_vaddr & 0x00000FFF);
+
+/*  This is a draft for IOMMU support
 
     // loop on all virtual pages covering the user buffer
@@ -1014 +1118 @@
 
     // invalidate data cache in case of memory write
-    if (to_user) {
-        _dcache_buf_invalidate((void *) user_vaddr, length);
-    }
-
-    // get the lock 
-    _get_lock(&_dma_lock[dma_id]);
+    if (to_user) _dcache_buf_invalidate((void *) user_vaddr, length);
+
+// get the lock 
+//  _get_lock(&_dma_lock[dma_id]);
+
+#if GIET_DEBUG_DMA_DRIVER
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] DMA TRANSFER at cycle ");
+_putd( _proctime() );
+_puts("\n - cluster_id       = ");
+_putx( cluster_id );
+_puts("\n - channel_id       = ");
+_putx( channel_id );
+_puts("\n - dma_vbase        = ");
+_putx( (unsigned int)dma_vbase );
+_puts("\n - device_buf_vbase = ");
+_putx( device_vbase );
+_puts("\n - device_buf_pbase = ");
+_putl( device_pbase );
+_puts("\n - user_buf_vbase   = ");
+_putx( user_vaddr );
+_puts("\n - user_buf_pbase   = ");
+_putl( user_pbase );
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
 
     // DMA configuration 
-    if (to_user) {
-        dma_base[loc_id * DMA_SPAN + DMA_SRC] = (unsigned int) device_pbase;
-        dma_base[loc_id * DMA_SPAN + DMA_DST] = (unsigned int) user_pbase;
-    }
-    else {
-        dma_base[loc_id * DMA_SPAN + DMA_SRC] = (unsigned int) user_pbase;
-        dma_base[loc_id * DMA_SPAN + DMA_DST] = (unsigned int) device_pbase;
-    }
-    dma_base[loc_id * DMA_SPAN + DMA_LEN] = (unsigned int) length;
-
-    return 0;
-#else //NB_DMAS_MAX == 0
-    return -1;
-#endif
+    if (to_user) 
+    {
+        dma_vbase[channel_id * DMA_SPAN + DMA_SRC]     = (unsigned int)(device_pbase);
+        dma_vbase[channel_id * DMA_SPAN + DMA_SRC_EXT] = (unsigned int)(device_pbase>>32);
+        dma_vbase[channel_id * DMA_SPAN + DMA_DST]     = (unsigned int)(user_pbase);
+        dma_vbase[channel_id * DMA_SPAN + DMA_DST_EXT] = (unsigned int)(user_pbase>>32);
+    }
+    else 
+    {
+        dma_vbase[channel_id * DMA_SPAN + DMA_SRC]     = (unsigned int)(user_pbase);
+        dma_vbase[channel_id * DMA_SPAN + DMA_SRC_EXT] = (unsigned int)(user_pbase>>32);
+        dma_vbase[channel_id * DMA_SPAN + DMA_DST]     = (unsigned int)(device_pbase);
+        dma_vbase[channel_id * DMA_SPAN + DMA_DST_EXT] = (unsigned int)(device_pbase>>32);
+    }
+    dma_vbase[channel_id * DMA_SPAN + DMA_LEN] = (unsigned int) length;
+
+    return 0;
+
+#else // NB_DMA_CHANNELS == 0
+    _get_lock(&_tty_put_lock);
+    _puts("\n[GIET ERROR] in _dma_transfer() : NB_DMA_CHANNELS == 0");
+    _release_lock(&_tty_put_lock);
+    return 1;
+#endif
+
 }  // end _dma_transfer()  
 
@@ -1047 +1182 @@
 // (1 == read error / 2 == DMA idle error / 3 == write error)
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _dma_completed() {
-#if NB_DMAS_MAX > 0
-    unsigned int task_id = _get_proc_task_id();
-    unsigned int dma_id  = _get_context_slot(task_id, CTX_DMA_ID);
+unsigned int _dma_completed() 
+{
+#if NB_DMA_CHANNELS > 0
+    unsigned int dma_id  = _get_context_slot(CTX_DMA_ID);
     unsigned int dma_ret;
 
     // busy waiting with a pseudo random delay between bus access
-    while (_dma_done[dma_id] == 0) {
+    while (_dma_done[dma_id] == 0) 
+    {
         unsigned int delay = (( _proctime() ^ _procid() << 4) & 0x3F) + 1;
         asm volatile(
@@ -1067 +1203 @@
     }
 
-    /* draft support for IOMMU
-    // unmap the buffer from IOMMU page table if IOMMU is activated
-    if ( GIET_IOMMU_ACTIVE )
-    {
-    unsigned int* iob_address = (unsigned int*)&seg_iob_base;
-
-    unsigned int  ix1         = _dma_iommu_ix1 + dma_id;
-    unsigned int  ix2;
-
-    for ( ix2 = 0 ; ix2 < _dma_iommu_npages[dma_id] ; ix2++ )
-    {
-    // unmap the page in IOMMU page table
-    _iommu_inval_pte2( ix1,        // PT1 index 
-    ix2 );   // PT2 index
-
-    // clear IOMMU TLB
-    iob_address[IOB_INVAL_PTE] = (ix1 << 21) | (ix2 << 12);
-    }
-    }
-    */
+#if GIET_DEBUG_DMA_DRIVER
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] DMA COMPLETED at cycle ");
+_putd( _proctime() );
+_puts("\n - cluster_id       = ");
+_putx( dma_id/NB_DMA_CHANNELS );
+_puts("\n - channel_id       = ");
+_putx( dma_id%NB_DMA_CHANNELS );
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
 
     // reset synchronization variables
@@ -1092 +1219 @@
     dma_ret = _dma_status[dma_id];
     asm volatile("sync\n");
-    _dma_lock[dma_id] = 0;
+
+//    _dma_lock[dma_id] = 0;
 
     return dma_ret;
 
-#else //NB_DMAS_MAX == 0
+#else // NB_DMA_CHANNELS == 0
     return -1;
 #endif
+
 }  // end _dma_completed
+
 
 //////////////////////////////////////////////////////////////////////////////////
@@ -1113 +1243 @@
 // The '_fb_write()', '_fb_read()' and '_fb_completed()' functions use the 
 // VciMultiDma components (distributed in the clusters) to transfer data 
-// between the user buffer and the frame buffer. A  FBDMA channel is
+// between the user buffer and the frame buffer. A DMA channel is
 // allocated to each task requesting it in the mapping_info data structure.
 //////////////////////////////////////////////////////////////////////////////////
@@ -1124 +1254 @@
 // - length : number of bytes to be transfered.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _fb_sync_write(unsigned int offset, const void * buffer, unsigned int length) {
-    unsigned char * fb_address = (unsigned char *) &seg_fbf_base + offset;
+unsigned int _fb_sync_write( unsigned int   offset, 
+                             const void*    buffer, 
+                             unsigned int   length) 
+{
+    unsigned char* fb_address = (unsigned char *) &seg_fbf_base + offset;
     memcpy((void *) fb_address, (void *) buffer, length);
     return 0;
@@ -1138 +1271 @@
 // - length : number of bytes to be transfered.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _fb_sync_read(unsigned int offset, const void * buffer, unsigned int length) {
-    unsigned char * fb_address = (unsigned char *) &seg_fbf_base + offset;
+unsigned int _fb_sync_read( unsigned int   offset, 
+                            const void*    buffer, 
+                            unsigned int   length) 
+{
+    unsigned char* fb_address = (unsigned char *) &seg_fbf_base + offset;
     memcpy((void *) buffer, (void *) fb_address, length);
     return 0;
@@ -1153 +1289 @@
 // Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _fb_write(unsigned int offset, const void * buffer, unsigned int length) {
-    return _dma_transfer(
-            0,             // frame buffer
-            0,             // write 
-            offset,
-            (unsigned int) buffer,
-            length);
+unsigned int _fb_write( unsigned int   offset, 
+                        const void*    buffer, 
+                        unsigned int   length) 
+{
+    return _dma_transfer( 0,             // frame buffer
+                          0,             // write 
+                          offset,
+                          (unsigned int) buffer,
+                          length );
 }
 
@@ -1171 +1309 @@
 // Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _fb_read(unsigned int offset, const void * buffer, unsigned int length) {
-    return _dma_transfer(
-            0,    // frame buffer
-            1,    // read 
-            offset,
-            (unsigned int) buffer,
-            length);
+unsigned int _fb_read( unsigned int   offset, 
+                       const void*    buffer, 
+                       unsigned int   length ) 
+{
+    return _dma_transfer( 0,    // frame buffer
+                          1,    // read 
+                          offset,
+                          (unsigned int) buffer,
+                          length );
 }
 
@@ -1188 +1328 @@
 // (1 == read error / 2 == DMA idle error / 3 == write error)
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _fb_completed() {
+unsigned int _fb_completed() 
+{
     return _dma_completed();
 }
@@ -1215 +1356 @@
 // - length : number of bytes to be transfered.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _nic_sync_write(unsigned int offset, const void * buffer, unsigned int length) {
-    unsigned char * nic_address = (unsigned char *) &seg_nic_base + offset;
+unsigned int _nic_sync_write( unsigned int   offset, 
+                              const void*    buffer, 
+                              unsigned int   length ) 
+{
+    unsigned char* nic_address = (unsigned char *) &seg_nic_base + offset;
     memcpy((void *) nic_address, (void *) buffer, length);
     return 0;
@@ -1279 +1423 @@
 // (1 == read error / 2 == DMA idle error / 3 == write error)
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int _nic_completed() {
+unsigned int _nic_completed() 
+{
     return _dma_completed();
 }
@@ -1286 +1431 @@
 // _heap_info()
 // This function returns the information associated to a heap (size and vaddr)
-// It uses the global task id (CTX_GTID_ID, unique for each giet task) and the
-// vspace id (CTX_VSID_ID) defined in the context 
+// It uses the global task index (CTX_GTID_ID, unique for each giet task) and the
+// vspace index (CTX_VSID_ID) defined in the task context. 
 ///////////////////////////////////////////////////////////////////////////////////
-unsigned int _heap_info(unsigned int * vaddr, unsigned int * size) {
+unsigned int _heap_info( unsigned int* vaddr, 
+                         unsigned int* size ) 
+{
     mapping_header_t * header  = (mapping_header_t *) (&seg_mapping_base);
     mapping_task_t * tasks     = _get_task_base(header);
     mapping_vobj_t * vobjs     = _get_vobj_base(header);
     mapping_vspace_t * vspaces = _get_vspace_base(header);
-    unsigned int taskid        = _get_context_slot(_get_proc_task_id(), CTX_GTID_ID);
-    unsigned int vspaceid      = _get_context_slot(_get_proc_task_id(), CTX_VSID_ID);
+
+    unsigned int taskid        = _get_context_slot(CTX_GTID_ID);
+    unsigned int vspaceid      = _get_context_slot(CTX_VSID_ID);
+
     int heap_local_vobjid      = tasks[taskid].heap_vobjid;
-    if (heap_local_vobjid != -1) {
+    if (heap_local_vobjid != -1) 
+    {
         unsigned int vobjheapid = heap_local_vobjid + vspaces[vspaceid].vobj_offset;
         *vaddr                  = vobjs[vobjheapid].vaddr;
@@ -1303 +1453 @@
         return 0;
     }
-    else {
+    else 
+    {
         *vaddr = 0;
         *size = 0;