Changeset 238 for soft/giet_vm/boot

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.

Location:

soft/giet_vm/boot

Files:

• boot_init.c (modified) (82 diffs)
• reset.S (modified) (1 diff)

soft/giet_vm/boot/boot_init.c

@@ -7 +7 @@
 // The boot_init.c file is part of the GIET-VM nano-kernel.
 // This code is executed in the boot phase by proc[0] to initialize the
-//  peripherals and the kernel data structures:
+// peripherals and the kernel data structures:
 // - pages tables for the various vspaces
 // - shedulers for processors (including the tasks contexts and interrupt vectors)
+//
+// This nano-kernel has been written for the MIPS32 processor.
+// The virtual adresses are on 32 bits and use the (unsigned int) type, but the 
+// physicals addresses can have up to 40 bits, and use the  (unsigned long long) type.
 //
 // The GIET-VM uses the paged virtual memory and the MAPPING_INFO binary file
@@ -20 +24 @@
 // The MAPPING_INFO binary data structure must be loaded in the the seg_boot_mapping 
 // segment (at address seg_mapping_base).
-// This MAPPING_INFO data structure defines both the hardware architecture
-// and the mapping:
-// - physical segmentation of the physical address space, 
-// - virtual spaces definition (one multi-task application per vspace), 
-// - placement of virtual objects (vobj) in the virtual segments (vseg).
-// - placement of virtual segments (vseg) in the physical segments (pseg).
-// - placement of tasks on the processors, 
+// This MAPPING_INFO data structure defines 
+// - the hardware architecture: number of clusters, number or processors, 
+//   size of the memory segments, and peripherals in each cluster.
+// - The structure of the various multi-threaded software applications:
+//   number of tasks, communication channels.
+// - The mapping: placement of virtual objects (vobj) in the virtual segments (vseg),
+//   placement of virtual segments (vseg) in the physical segments (pseg), placement 
+//   of software tasks on the processors, 
 //
 // The page table are statically build in the boot phase, and they do not 
@@ -35 +40 @@
 // The max number of virtual spaces (GIET_NB_VSPACE_MAX) is a configuration parameter.
 //
-// Each page table (one page table per virtual space) is monolithic, and
-// contains one PT1 and (GIET_NB_PT2_MAX) PT2s. The PT1 is addressed using the ix1 field
+// Each page table (one page table per virtual space) is monolithic, and contains 
+// one PT1 and up to (GIET_NB_PT2_MAX) PT2s. The PT1 is addressed using the ix1 field
 // (11 bits) of the VPN, and the selected PT2 is addressed using the ix2 field (9 bits).
-// - PT1[2048] : a first 8K aligned array of unsigned int, indexed by the (ix1) field of VPN. 
+// - PT1[2048] : a first 8K aligned array of unsigned int, indexed by (ix1) field of VPN. 
 //   Each entry in the PT1 contains a 32 bits PTD. The MSB bit PTD[31] is 
 //   the PTD valid bit, and LSB bits PTD[19:0] are the 20 MSB bits of the physical base
@@ -44 +49 @@
 //   The PT1 contains 2048 PTD of 4 bytes => 8K bytes.
 // - PT2[1024][GIET_NB_PT2_MAX] : an array of array of unsigned int. 
-//   Each PT2[1024] must be 4K aligned,  and each entry in a PT2 contains two unsigned int: 
+//   Each PT2[1024] must be 4K aligned, each entry in a PT2 contains two unsigned int: 
 //   the first word contains the protection flags, and the second word contains the PPN.
 //   Each PT2 contains 512 PTE2 of 8bytes => 4K bytes.
@@ -64 +69 @@
 #include <stdarg.h>
 
-
 #if !defined(NB_CLUSTERS)
 # error The NB_CLUSTERS value must be defined in the 'giet_config.h' file !
@@ -79 +83 @@
 ////////////////////////////////////////////////////////////////////////////
 //      Global variables for boot code
-// As both the page tables and the schedulers are physically distributed,
-// these global variables are just arrays of pointers. 
+// Both the page tables for the various virtual spaces, and the schedulers
+// for the processors are physically distributed on the clusters.
+// These global variables are just arrays of pointers. 
 ////////////////////////////////////////////////////////////////////////////
 
-// Page table pointers array
-page_table_t * boot_ptabs_vaddr[GIET_NB_VSPACE_MAX];
-page_table_t * boot_ptabs_paddr[GIET_NB_VSPACE_MAX];
-
-// Scheduler pointers array
-static_scheduler_t * boot_schedulers_paddr[NB_CLUSTERS * NB_PROCS_MAX];
+// Page table addresses arrays
+paddr_t      boot_ptabs_paddr[GIET_NB_VSPACE_MAX];
+unsigned int boot_ptabs_vaddr[GIET_NB_VSPACE_MAX];
+
+// Scheduler pointers array (virtual addresses)
+static_scheduler_t* boot_schedulers[NB_CLUSTERS * NB_PROCS_MAX];
 
 // Next free PT2 index array
@@ -102 +107 @@
 // boot_procid() 
 //////////////////////////////////////////////////////////////////////////////
-inline unsigned int boot_procid() {
+inline unsigned int boot_procid() 
+{
     unsigned int ret;
     asm volatile ("mfc0 %0, $15, 1":"=r" (ret));
@@ -108 +114 @@
 }
 
-
 //////////////////////////////////////////////////////////////////////////////
 // boot_proctime() 
 //////////////////////////////////////////////////////////////////////////////
-inline unsigned int boot_proctime() {
+inline unsigned int boot_proctime() 
+{
     unsigned int ret;
     asm volatile ("mfc0 %0, $9":"=r" (ret));
@@ -118 +124 @@
 }
 
-
 //////////////////////////////////////////////////////////////////////////////
 // boot_exit() 
 //////////////////////////////////////////////////////////////////////////////
-void boot_exit() {
-    while (1) {
-        asm volatile ("nop");
-    }
-}
-
+void boot_exit() 
+{
+    while (1) { asm volatile ("nop"); }
+}
 
 //////////////////////////////////////////////////////////////////////////////
@@ -134 +137 @@
 // in all task contexts (when the task has never been executed.
 /////////////////////////////////"/////////////////////////////////////////////
-void boot_eret() {
+void boot_eret() 
+{
     asm volatile ("eret");
 }
 
-
-//////////////////////////////////////////////////////////////////////////////
-// boot_scheduler_set_context()
-// This function set a context slot in a scheduler, after a temporary
-// desactivation of the DTLB (because we use the scheduler physical address).
-// - gpid   : global processor/scheduler index
-// - ltid   : local task index
-// - slotid : context slot index
-// - value  : value to be written 
-//////////////////////////////////////////////////////////////////////////////
-inline void boot_scheduler_set_context(unsigned int gpid,
-        unsigned int ltid,
-        unsigned int slotid,
-        unsigned int value) {
-    // get scheduler physical address
-    static_scheduler_t * psched = boot_schedulers_paddr[gpid];
-
-    // get slot physical address
-    unsigned int * pslot = &(psched->context[ltid][slotid]);
-
-    asm volatile ("li      $26,    0xB     \n"
-            "mtc2    $26,    $1      \n"    /* desactivate DTLB */
-            "sw      %1,     0(%0)   \n"    /* *pslot <= value  */
-            "li      $26,    0xF     \n"
-            "mtc2    $26,    $1      \n"    /* activate DTLB    */
+////////////////////////////////////////////////////////////////////////////
+// boot_physical_read()
+// This function makes a physical read access to a 32 bits word in memory, 
+// after a temporary DTLB de-activation and paddr extension.
+////////////////////////////////////////////////////////////////////////////
+unsigned int boot_physical_read(paddr_t paddr) 
+{
+    unsigned int value;
+    unsigned int lsb = (unsigned int)paddr;
+    unsigned int msb = (unsigned int)(paddr >> 32);
+
+    asm volatile(
+            "mfc2   $2,     $1                 \n"     /* $2 <= MMU_MODE   */
+            "andi   $3,     $2,        0xb     \n"
+            "mtc2   $3,     $1                 \n"     /* DTLB off         */    
+
+            "mtc2   %2,     $24                \n"     /* PADDR_EXT <= msb */   
+            "lw     %0,     0(%1)              \n"     /* value <= *paddr  */
+            "mtc2   $0,     $24                \n"     /* PADDR_EXT <= 0   */   
+
+            "mtc2   $2,     $1                 \n"     /* restore MMU_MODE */
+            : "=r" (value)
+            : "r" (lsb), "r" (msb)
+            : "$2", "$3");
+    return value;
+}
+
+////////////////////////////////////////////////////////////////////////////
+// boot_physical_write()
+// This function makes a physical write access to a 32 bits word in memory, 
+// after a temporary DTLB de-activation and paddr extension.
+////////////////////////////////////////////////////////////////////////////
+void boot_physical_write(paddr_t      paddr, 
+                         unsigned int value) 
+{
+    unsigned int lsb = (unsigned int)paddr;
+    unsigned int msb = (unsigned int)(paddr >> 32);
+
+    asm volatile(
+            "mfc2   $2,     $1                 \n"     /* $2 <= MMU_MODE   */
+            "andi   $3,     $2,        0xb     \n"
+            "mtc2   $3,     $1                 \n"     /* DTLB off         */    
+
+            "mtc2   %2,     $24                \n"     /* PADDR_EXT <= msb */   
+            "sw     %0,     0(%1)              \n"     /* *paddr <= value  */
+            "mtc2   $0,     $24                \n"     /* PADDR_EXT <= 0   */   
+
+            "mtc2   $2,     $1                 \n"     /* restore MMU_MODE */
             :
-            :"r" (pslot), "r"(value)
-            :"$26");
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-// boot_scheduler_set_itvector()
-// This function set an interrupt vector slot in a scheduler, after a temporary
-// desactivation of the DTLB (because we use the scheduler physical address).
-// - gpid   : global processor/scheduler index
-// - slotid : context slot index
-// - value  : value to be written 
-//////////////////////////////////////////////////////////////////////////////
-inline void boot_scheduler_set_itvector(unsigned int gpid,
-        unsigned int slotid,
-        unsigned int value) {
-    // get scheduler physical address
-    static_scheduler_t * psched = boot_schedulers_paddr[gpid];
-
-    // get slot physical address
-    unsigned int * pslot = &(psched->interrupt_vector[slotid]);
-
-    asm volatile ("li      $26,    0xB     \n"
-            "mtc2    $26,    $1      \n"    /* desactivate DTLB */
-            "sw      %1,     0(%0)   \n"    /* *pslot <= value  */
-            "li      $26,    0xF     \n"
-            "mtc2    $26,    $1      \n"    /* activate DTLB    */
-            :
-            :"r" (pslot), "r"(value)
-            :"$26");
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-// boot_scheduler_get_itvector()
-// This function get an interrupt vector slot in a scheduler, after a temporary
-// desactivation of the DTLB (because we use the scheduler physical address).
-// - gpid   : global processor/scheduler index
-// - slotid : context slot index
-// - return the content of the slot 
-//////////////////////////////////////////////////////////////////////////////
-unsigned int boot_scheduler_get_itvector(unsigned int gpid, unsigned int slotid) {
-    unsigned int value;
-
-    // get scheduler physical address
-    static_scheduler_t * psched = boot_schedulers_paddr[gpid];
-
-    // get slot physical address
-    unsigned int * pslot = &(psched->interrupt_vector[slotid]);
-
-    asm volatile ("li      $26,    0xB     \n"
-            "mtc2    $26,    $1      \n"    /* desactivate DTLB */
-            "lw      %0,     0(%1)   \n"    /* *pslot <= value  */
-            "li      $26,    0xF     \n"
-            "mtc2    $26,    $1      \n"    /* activate DTLB    */
-            :"=r" (value)
-            :"r"(pslot)
-            :"$26");
-    return value;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-// boot_scheduler_get_tasks()
-// This function returns the "tasks" field of a scheduler, after temporary 
-// desactivation of the DTLB (because we use the scheduler physical address).
-// - gpid   : global processor/scheduler index
-//////////////////////////////////////////////////////////////////////////////
-inline unsigned int boot_scheduler_get_tasks(unsigned int gpid) {
-    unsigned int ret;
-
-    // get scheduler physical address
-    static_scheduler_t * psched = boot_schedulers_paddr[gpid];
-
-    // get tasks physical address
-    unsigned int * ptasks = &(psched->tasks);
-
-    asm volatile ("li      $26,    0xB     \n"
-            "mtc2    $26,    $1      \n"    /* desactivate DTLB */
-            "lw      %0,     0(%1)   \n"    /* ret <= *ptasks   */
-            "li      $26,    0xF     \n"
-            "mtc2    $26,    $1      \n"    /* activate DTLB    */
-            :"=r" (ret)
-            :"r"(ptasks)
-            :"$26");
-    return ret;
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-// boot_scheduler_set_tasks()
-// This function set the "tasks" field of a scheduler, after temporary 
-// desactivation of the DTLB (because we use the scheduler physical address).
-// - gpid   : global processor/scheduler index
-// - value  : value to be written 
-//////////////////////////////////////////////////////////////////////////////
-inline void boot_scheduler_set_tasks(unsigned int gpid, unsigned int value) {
-    // get scheduler physical address
-    static_scheduler_t * psched = boot_schedulers_paddr[gpid];
-
-    // get tasks physical address
-    unsigned int * ptasks = &(psched->tasks);
-
-    asm volatile ("li      $26,    0xB     \n"
-            "mtc2    $26,    $1      \n"    /* desactivate DTLB */
-            "sw      %1,     0(%0)   \n"    /* *ptasks <= value */
-            "li      $26,    0xF     \n"
-            "mtc2    $26,    $1      \n"    /* activate DTLB    */
-            :
-            :"r" (ptasks), "r"(value)
-            :"$26");
-}
-
-
-//////////////////////////////////////////////////////////////////////////////
-// boot_scheduler_set_current()
-// This function set the "current" field of a scheduler, after temporary 
-// desactivation of the DTLB (because we use the scheduler physical address).
-// - gpid   : global processor/scheduler index
-// - value  : value to be written 
-//////////////////////////////////////////////////////////////////////////////
-inline void boot_scheduler_set_current(unsigned int gpid, unsigned int value) {
-    // get scheduler physical address
-    static_scheduler_t *psched = boot_schedulers_paddr[gpid];
-
-    // get tasks physical address
-    unsigned int * pcur = &(psched->current);
-
-    asm volatile ("li      $26,    0xB     \n"
-            "mtc2    $26,    $1      \n"    /* desactivate DTLB */
-            "sw      %1,     0(%0)   \n"    /* *pcur   <= value */
-            "li      $26,    0xF     \n"
-            "mtc2    $26,    $1      \n"    /* activate DTLB    */
-            :
-            :"r" (pcur), "r"(value)
-            :"$26");
-}
-
+            : "r" (value), "r" (lsb), "r" (msb)
+            : "$2", "$3");
+}
 
 //////////////////////////////////////////////////////////////////////////////
@@ -307 +199 @@
 // This function set a new value for the MMU PTPR register.
 //////////////////////////////////////////////////////////////////////////////
-inline void boot_set_mmu_ptpr(unsigned int val) {
+inline void boot_set_mmu_ptpr(unsigned int val) 
+{
     asm volatile ("mtc2  %0, $0"::"r" (val));
 }
-
 
 //////////////////////////////////////////////////////////////////////////////
@@ -316 +208 @@
 // This function set a new value for the MMU MODE register.
 //////////////////////////////////////////////////////////////////////////////
-inline void boot_set_mmu_mode(unsigned int val) {
+inline void boot_set_mmu_mode(unsigned int val) 
+{
     asm volatile ("mtc2  %0, $1"::"r" (val));
 }
-
 
 ////////////////////////////////////////////////////////////////////////////
 // boot_puts()
-// (it uses TTY0)
+// display a string on TTY0
 ////////////////////////////////////////////////////////////////////////////
-void boot_puts(const char * buffer) {
+void boot_puts(const char * buffer) 
+{
     unsigned int *tty_address = (unsigned int *) &seg_tty_base;
     unsigned int n;
 
-    for (n = 0; n < 100; n++) {
-        if (buffer[n] == 0) {
-            break;
-        }
+    for (n = 0; n < 100; n++) 
+    {
+        if (buffer[n] == 0)  break; 
         tty_address[TTY_WRITE] = (unsigned int) buffer[n];
     }
 }
-
 
 ////////////////////////////////////////////////////////////////////////////
 // boot_putx() 
-// (it uses TTY0)
+// display a 32 bits unsigned int as an hexadecimal string on TTY0
 ////////////////////////////////////////////////////////////////////////////
-void boot_putx(unsigned int val) {
+void boot_putx(unsigned int val) 
+{
     static const char HexaTab[] = "0123456789ABCDEF";
     char buf[11];
@@ -351 +243 @@
     buf[10] = 0;
 
-    for (c = 0; c < 8; c++) {
+    for (c = 0; c < 8; c++) 
+    {
         buf[9 - c] = HexaTab[val & 0xF];
         val = val >> 4;
@@ -358 +251 @@
 }
 
+////////////////////////////////////////////////////////////////////////////
+// boot_putl() 
+// display a 64 bits unsigned long as an hexadecimal string on TTY0
+////////////////////////////////////////////////////////////////////////////
+void boot_putl(paddr_t val) 
+{
+    static const char HexaTab[] = "0123456789ABCDEF";
+    char buf[19];
+    unsigned int c;
+
+    buf[0] = '0';
+    buf[1] = 'x';
+    buf[18] = 0;
+
+    for (c = 0; c < 16; c++) 
+    {
+        buf[17 - c] = HexaTab[(unsigned int)val & 0xF];
+        val = val >> 4;
+    }
+    boot_puts(buf);
+}
 
 ////////////////////////////////////////////////////////////////////////////
 // boot_putd() 
-// (it uses TTY0)
+// display a 32 bits unsigned int as a decimal string on TTY0
 ////////////////////////////////////////////////////////////////////////////
-void boot_putd(unsigned int val) {
+void boot_putd(unsigned int val) 
+{
     static const char DecTab[] = "0123456789";
     char buf[11];
@@ -371 +286 @@
     buf[10] = 0;
 
-    for (i = 0; i < 10; i++) {
-        if ((val != 0) || (i == 0)) {
+    for (i = 0; i < 10; i++) 
+    {
+        if ((val != 0) || (i == 0)) 
+        {
             buf[9 - i] = DecTab[val % 10];
             first = 9 - i;
         }
-        else {
+        else 
+        {
             break;
         }
@@ -384 +302 @@
 }
 
-
 /////////////////////////////////////////////////////////////////////////////
 //  mapping_info data structure access functions
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_cluster_t *boot_get_cluster_base(mapping_header_t * header) {
+inline mapping_cluster_t *boot_get_cluster_base(mapping_header_t * header) 
+{
     return (mapping_cluster_t *) ((char *) header + MAPPING_HEADER_SIZE);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_pseg_t *boot_get_pseg_base(mapping_header_t * header) {
+inline mapping_pseg_t *boot_get_pseg_base(mapping_header_t * header) 
+{
     return (mapping_pseg_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
             MAPPING_CLUSTER_SIZE * header->clusters);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_vspace_t *boot_get_vspace_base(mapping_header_t * header) {
+inline mapping_vspace_t *boot_get_vspace_base(mapping_header_t * header) 
+{
     return (mapping_vspace_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -408 +324 @@
             MAPPING_PSEG_SIZE * header->psegs);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_vseg_t *boot_get_vseg_base(mapping_header_t * header) {
+inline mapping_vseg_t *boot_get_vseg_base(mapping_header_t * header) 
+{
     return (mapping_vseg_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -418 +333 @@
             MAPPING_VSPACE_SIZE * header->vspaces);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_vobj_t *boot_get_vobj_base(mapping_header_t * header) {
+inline mapping_vobj_t *boot_get_vobj_base(mapping_header_t * header) 
+{
     return (mapping_vobj_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -429 +343 @@
             MAPPING_VSEG_SIZE * header->vsegs);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_task_t *boot_get_task_base(mapping_header_t * header) {
+inline mapping_task_t *boot_get_task_base(mapping_header_t * header) 
+{
     return (mapping_task_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -441 +354 @@
             MAPPING_VOBJ_SIZE * header->vobjs);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_proc_t *boot_get_proc_base(mapping_header_t * header) {
+inline mapping_proc_t *boot_get_proc_base(mapping_header_t * header) 
+{
     return (mapping_proc_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -454 +366 @@
             MAPPING_TASK_SIZE * header->tasks);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_irq_t *boot_get_irq_base(mapping_header_t * header) {
+inline mapping_irq_t *boot_get_irq_base(mapping_header_t * header) 
+{
     return (mapping_irq_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -468 +379 @@
             MAPPING_PROC_SIZE * header->procs);
 }
-
-
 /////////////////////////////////////////////////////////////////////////////
-inline mapping_coproc_t *boot_get_coproc_base(mapping_header_t * header) {
+inline mapping_coproc_t *boot_get_coproc_base(mapping_header_t * header) 
+{
     return (mapping_coproc_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -483 +393 @@
             MAPPING_IRQ_SIZE * header->irqs);
 }
-
-
 ///////////////////////////////////////////////////////////////////////////////////
-inline mapping_cp_port_t *boot_get_cp_port_base(mapping_header_t * header) {
+inline mapping_cp_port_t *boot_get_cp_port_base(mapping_header_t * header) 
+{
     return (mapping_cp_port_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -499 +408 @@
             MAPPING_COPROC_SIZE * header->coprocs);
 }
-
-
 ///////////////////////////////////////////////////////////////////////////////////
-inline mapping_periph_t *boot_get_periph_base(mapping_header_t * header) {
+inline mapping_periph_t *boot_get_periph_base(mapping_header_t * header) 
+{
     return (mapping_periph_t *) ((char *) header +
             MAPPING_HEADER_SIZE +
@@ -517 +425 @@
 }
 
-
 //////////////////////////////////////////////////////////////////////////////
 //     boot_pseg_get() 
@@ -523 +430 @@
 // identified  by the pseg index.
 //////////////////////////////////////////////////////////////////////////////
-mapping_pseg_t *boot_pseg_get(unsigned int seg_id) {
+mapping_pseg_t *boot_pseg_get(unsigned int seg_id) 
+{
     mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
     mapping_pseg_t * pseg = boot_get_pseg_base(header);
 
     // checking argument
-    if (seg_id >= header->psegs) {
+    if (seg_id >= header->psegs) 
+    {
         boot_puts("\n[BOOT ERROR] : seg_id argument too large\n");
         boot_puts("               in function boot_pseg_get()\n");
@@ -535 +444 @@
 
     return &pseg[seg_id];
-}                // end boot_pseg_get()
-
+}  
 
 //////////////////////////////////////////////////////////////////////////////
 // boot_add_pte() 
-// This function registers a new PTE in the page table pointed
+// This function registers a new PTE in the page table defined
 // by the vspace_id argument, and updates both PT1 and PT2.
 // A new PT2 is used when required.
 // As the set of PT2s is implemented as a fixed size array (no dynamic 
 // allocation), this function checks a possible overflow of the PT2 array.
-//
-// The global parameter is a boolean indicating wether a global vseg is
-// being mapped.
 //////////////////////////////////////////////////////////////////////////////
 void boot_add_pte(unsigned int vspace_id,
-        unsigned int vpn, unsigned int flags, unsigned int ppn) {
+                  unsigned int vpn, 
+                  unsigned int flags, 
+                  unsigned int ppn,
+                  unsigned int verbose) 
+{
     unsigned int ix1;
     unsigned int ix2;
-    unsigned int ptba;      // PT2 base address
-    unsigned int pt2_id;    // PT2 index
-    unsigned int *pt_flags; // pointer on the pte_flags = &PT2[2*ix2]    
-    unsigned int *pt_ppn;   // pointer on the pte_ppn   = &PT2[2*ix2+1]  
+    paddr_t      pt1_pbase;     // PT1 physical base address
+    paddr_t      pt2_pbase;     // PT2 physical base address
+    paddr_t      pte_paddr;     // PTE physucal address
+    unsigned int pt2_id;        // PT2 index
+    unsigned int ptd;           // PTD : entry in PT1
+    unsigned int max_pt2;       // max number of PT2s for a given vspace
 
     ix1 = vpn >> 9;         // 11 bits
@@ -562 +473 @@
 
     // check that the boot_max_pt2[vspace_id] has been set
-    unsigned int max_pt2 = boot_max_pt2[vspace_id];
-
-    if (max_pt2 == 0) {
-        boot_puts("Unfound page table for vspace ");
+    max_pt2 = boot_max_pt2[vspace_id];
+
+    if (max_pt2 == 0) 
+    {
+        boot_puts("Undefined page table for vspace ");
         boot_putd(vspace_id);
         boot_puts("\n");
         boot_exit();
     }
-    // get page table physical address
-    page_table_t *pt = boot_ptabs_paddr[vspace_id];
-
-    if ((pt->pt1[ix1] & PTE_V) == 0) { // set a new PTD in PT1 
+
+    // get page table physical base address
+    pt1_pbase = boot_ptabs_paddr[vspace_id];
+
+    // get ptd in PT1
+    ptd = boot_physical_read( pt1_pbase + 4*ix1 );
+
+    if ((ptd & PTE_V) == 0)    // invalid PTD: compute PT2 base address, 
+                               // and set a new PTD in PT1 
+    {
         pt2_id = boot_next_free_pt2[vspace_id];
-        if (pt2_id == max_pt2) {
+        if (pt2_id == max_pt2) 
+        {
             boot_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
             boot_puts("the length of the ptab vobj is too small\n");
             boot_exit();
         }
-        else {
-            ptba = (unsigned int) pt + PT1_SIZE + PT2_SIZE * pt2_id;
-            pt->pt1[ix1] = PTE_V | PTE_T | (ptba >> 12);
+        else 
+        {
+            pt2_pbase = pt1_pbase + PT1_SIZE + PT2_SIZE * pt2_id;
+            ptd = PTE_V | PTE_T | (unsigned int)(pt2_pbase >> 12);
+            boot_physical_write( pt1_pbase + 4*ix1 , ptd);
             boot_next_free_pt2[vspace_id] = pt2_id + 1;
         }
     }
-    else {
-        ptba = pt->pt1[ix1] << 12;
-    }
-
-    // set PTE2 
-    pt_flags = (unsigned int *) (ptba + 8 * ix2);
-    pt_ppn = (unsigned int *) (ptba + 8 * ix2 + 4);
-
-    *pt_flags = flags;
-    *pt_ppn = ppn;
-
-/*
-if ( vpn == 0x00000300)
-{
-boot_puts("vpn       = ");
-boot_putx( vpn );
-boot_puts("\n");
-boot_puts("pt_flags  = ");
-boot_putx( (unsigned int)pt_flags );
-boot_puts("\n");
-boot_puts("*pt_flags = ");
-boot_putx( *pt_flags );
-boot_puts("\n");
-boot_exit();
-}
-
-    if ((*pt_flags & PTE_V) != 0) {  // page already mapped
-        boot_puts("\n[BOOT ERROR] double mapping in vspace ");
-        boot_putd(vspace_id);
-        boot_puts(" for vpn = ");
-        boot_putx(vpn);
-        boot_puts("\n");
-        boot_exit();
-    }
-*/
-}                // end boot_add_pte()
+    else                       // valid PTD: compute PT2 base address
+    {
+        pt2_pbase = ((paddr_t)(ptd & 0x0FFFFFFF)) << 12;
+    }
+
+    // set PTE in PT2 : flags & PPN in two 32 bits words
+    pte_paddr = pt2_pbase + 8*ix2;
+    boot_physical_write( pte_paddr     , flags);
+    boot_physical_write( pte_paddr + 4 , ppn);
+
+if ( verbose )
+{
+boot_puts("     / pt1_pbase = ");
+boot_putl( pt1_pbase );
+boot_puts(" / ptd = ");
+boot_putl( ptd );
+boot_puts(" / pt2_pbase = ");
+boot_putl( pt2_pbase );
+boot_puts(" / pte_paddr = ");
+boot_putl( pte_paddr );
+boot_puts(" / ppn = ");
+boot_putx( ppn );
+boot_puts("/\n");
+}
+
+}   // end boot_add_pte()
 
 
@@ -627 +538 @@
 // This function build the page table for a given vspace. 
 // The physical base addresses for all vsegs (global and private)
-// must have been previously computed.
+// must have been previously computed and stored in the mapping.
 // It initializes the MWMR channels.
 /////////////////////////////////////////////////////////////////////
-void boot_vspace_pt_build(unsigned int vspace_id) {
+void boot_vspace_pt_build(unsigned int vspace_id) 
+{
     unsigned int vseg_id;
     unsigned int npages;
@@ -637 +549 @@
     unsigned int flags;
     unsigned int page_id;
+    unsigned int verbose = 0;   // can be used to activate trace in add_pte()
 
     mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
     mapping_vspace_t * vspace = boot_get_vspace_base(header);
-    mapping_vseg_t * vseg = boot_get_vseg_base(header);
+    mapping_vseg_t   * vseg   = boot_get_vseg_base(header);
 
     // private segments
     for (vseg_id = vspace[vspace_id].vseg_offset;
-            vseg_id < (vspace[vspace_id].vseg_offset + vspace[vspace_id].vsegs);
-            vseg_id++) {
+         vseg_id < (vspace[vspace_id].vseg_offset + vspace[vspace_id].vsegs);
+         vseg_id++) 
+    {
         vpn = vseg[vseg_id].vbase >> 12;
-        ppn = vseg[vseg_id].pbase >> 12;
+        ppn = (unsigned int)(vseg[vseg_id].pbase >> 12);
         npages = vseg[vseg_id].length >> 12;
-        if ((vseg[vseg_id].length & 0xFFF) != 0) {
-            npages++;
-        }
+        if ((vseg[vseg_id].length & 0xFFF) != 0) npages++; 
 
         flags = PTE_V;
-        if (vseg[vseg_id].mode & C_MODE_MASK) {
-            flags = flags | PTE_C;
-        }
-        if (vseg[vseg_id].mode & X_MODE_MASK) {
-            flags = flags | PTE_X;
-        }
-        if (vseg[vseg_id].mode & W_MODE_MASK) {
-            flags = flags | PTE_W;
-        }
-        if (vseg[vseg_id].mode & U_MODE_MASK) {
-            flags = flags | PTE_U;
-        }
+        if (vseg[vseg_id].mode & C_MODE_MASK)  flags = flags | PTE_C;
+        if (vseg[vseg_id].mode & X_MODE_MASK)  flags = flags | PTE_X;
+        if (vseg[vseg_id].mode & W_MODE_MASK)  flags = flags | PTE_W;
+        if (vseg[vseg_id].mode & U_MODE_MASK)  flags = flags | PTE_U;
 
 #if BOOT_DEBUG_PT
@@ -674 +578 @@
         boot_putd(npages);
         boot_puts(" / pbase = ");
-        boot_putx(vseg[vseg_id].pbase);
+        boot_putl(vseg[vseg_id].pbase);
         boot_puts("\n");
 #endif
         // loop on 4K pages
-        for (page_id = 0; page_id < npages; page_id++) {
-            boot_add_pte(vspace_id, vpn, flags, ppn);
+        for (page_id = 0; page_id < npages; page_id++) 
+        {
+            boot_add_pte(vspace_id, vpn, flags, ppn, verbose);
             vpn++;
             ppn++;
@@ -686 +591 @@
 
     // global segments
-    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) {
+    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) 
+    {
         vpn = vseg[vseg_id].vbase >> 12;
-        ppn = vseg[vseg_id].pbase >> 12;
+        ppn = (unsigned int)(vseg[vseg_id].pbase >> 12);
         npages = vseg[vseg_id].length >> 12;
-        if ((vseg[vseg_id].length & 0xFFF) != 0) {
-            npages++;
-        }
+        if ((vseg[vseg_id].length & 0xFFF) != 0) npages++;
 
         flags = PTE_V;
-        if (vseg[vseg_id].mode & C_MODE_MASK) {
-            flags = flags | PTE_C;
-        }
-        if (vseg[vseg_id].mode & X_MODE_MASK) {
-            flags = flags | PTE_X;
-        }
-        if (vseg[vseg_id].mode & W_MODE_MASK) {
-            flags = flags | PTE_W;
-        }
-        if (vseg[vseg_id].mode & U_MODE_MASK) {
-            flags = flags | PTE_U;
-        }
+        if (vseg[vseg_id].mode & C_MODE_MASK)  flags = flags | PTE_C;
+        if (vseg[vseg_id].mode & X_MODE_MASK)  flags = flags | PTE_X;
+        if (vseg[vseg_id].mode & W_MODE_MASK)  flags = flags | PTE_W;
+        if (vseg[vseg_id].mode & U_MODE_MASK)  flags = flags | PTE_U;
 
 #if BOOT_DEBUG_PT
         boot_puts(vseg[vseg_id].name);
-        boot_puts(" / flags = ");
+        boot_puts(" : flags = ");
         boot_putx(flags);
         boot_puts(" / npages = ");
         boot_putd(npages);
         boot_puts(" / pbase = ");
-        boot_putx(vseg[vseg_id].pbase);
+        boot_putl(vseg[vseg_id].pbase);
         boot_puts("\n");
 #endif
         // loop on 4K pages
-        for (page_id = 0; page_id < npages; page_id++) {
-            boot_add_pte(vspace_id, vpn, flags, ppn);
+        for (page_id = 0; page_id < npages; page_id++) 
+        {
+            boot_add_pte(vspace_id, vpn, flags, ppn, verbose);
             vpn++;
             ppn++;
         }
     }
-}                // end boot_vspace_pt_build()
+}   // end boot_vspace_pt_build()
 
 
 ///////////////////////////////////////////////////////////////////////////
-// Align the value "toAlign" to the required alignement indicated by
-// alignPow2 ( the logarithme of 2 the alignement).
+// Align the value of paddr or vaddr to the required alignement,
+// defined by alignPow2 == L2(alignement).
 ///////////////////////////////////////////////////////////////////////////
-unsigned int align_to(unsigned int toAlign, unsigned int alignPow2) {
+paddr_t paddr_align_to(paddr_t paddr, unsigned int alignPow2) 
+{
+    paddr_t mask = (1 << alignPow2) - 1;
+    return ((paddr + mask) & ~mask);
+}
+
+unsigned int vaddr_align_to(unsigned int vaddr, unsigned int alignPow2) 
+{
     unsigned int mask = (1 << alignPow2) - 1;
-    return ((toAlign + mask) & ~mask);
-}
-
+    return ((vaddr + mask) & ~mask);
+}
 
 ///////////////////////////////////////////////////////////////////////////
-// This function compute the physical base address for a vseg
+// This function computes the physical base address for a vseg
 // as specified in the mapping info data structure.
 // It updates the pbase and the length fields of the vseg.
@@ -747 +650 @@
 // It is a global vseg if vspace_id = (-1). 
 ///////////////////////////////////////////////////////////////////////////
-void boot_vseg_map(mapping_vseg_t * vseg, unsigned int vspace_id) {
+void boot_vseg_map(mapping_vseg_t * vseg, unsigned int vspace_id) 
+{
     unsigned int vobj_id;
     unsigned int cur_vaddr;
-    unsigned int cur_paddr;
+    paddr_t      cur_paddr;
+    unsigned int offset;
+
     mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
-    mapping_vobj_t * vobj = boot_get_vobj_base(header);
+    mapping_vobj_t   * vobj   = boot_get_vobj_base(header);
 
     // get physical segment pointer
-    mapping_pseg_t * pseg = boot_pseg_get(vseg->psegid);
+    mapping_pseg_t* pseg = boot_pseg_get(vseg->psegid);
 
     // compute vseg physical base address
-    if (vseg->ident != 0) {   // identity mapping required
+    if (vseg->ident != 0)                   // identity mapping required
+    {
         vseg->pbase = vseg->vbase;
     }
-    else {  // unconstrained mapping
+    else                                   // unconstrained mapping
+    {
         vseg->pbase = pseg->next_base;
 
         // test alignment constraint
-        if (vobj[vseg->vobj_offset].align) {
-            vseg->pbase = align_to(vseg->pbase, vobj[vseg->vobj_offset].align);
+        if (vobj[vseg->vobj_offset].align) 
+        {
+            vseg->pbase = paddr_align_to(vseg->pbase, vobj[vseg->vobj_offset].align);
         }
     }
@@ -778 +687 @@
     cur_paddr = vseg->pbase;
 
-    for (vobj_id = vseg->vobj_offset; vobj_id < (vseg->vobj_offset + vseg->vobjs); vobj_id++) {
-        if (vobj[vobj_id].align) {
-            cur_paddr = align_to(cur_paddr, vobj[vobj_id].align);
-            cur_vaddr = align_to(cur_vaddr, vobj[vobj_id].align);
+    for (vobj_id = vseg->vobj_offset; 
+         vobj_id < (vseg->vobj_offset + vseg->vobjs); vobj_id++) 
+    {
+        if (vobj[vobj_id].align) 
+        {
+            cur_paddr = paddr_align_to(cur_paddr, vobj[vobj_id].align);
+            cur_vaddr = vaddr_align_to(cur_vaddr, vobj[vobj_id].align);
         }
         // set vaddr/paddr for current vobj
@@ -787 +699 @@
         vobj[vobj_id].paddr = cur_paddr;
         
-        // initialise boot_ptabs_vaddr[] if current vobj is a PTAB
-        if (vobj[vobj_id].type == VOBJ_TYPE_PTAB) {
-            if (vspace_id == ((unsigned int) -1)) {   // global vseg
+        // initialise boot_ptabs_vaddr[] & boot_ptabs-paddr[] if PTAB
+        if (vobj[vobj_id].type == VOBJ_TYPE_PTAB) 
+        {
+            if (vspace_id == ((unsigned int) -1))    // global vseg
+            {
                 boot_puts("\n[BOOT ERROR] in boot_vseg_map() function: ");
                 boot_puts("a PTAB vobj cannot be global");
                 boot_exit();
             }
-            // we need at least one PT2 => ( boot_max_pt2[vspace_id] >= 1)
-            if (vobj[vobj_id].length < (PT1_SIZE + PT2_SIZE)) {
+            // we need at least one PT2
+            if (vobj[vobj_id].length < (PT1_SIZE + PT2_SIZE)) 
+            {
                 boot_puts("\n[BOOT ERROR] in boot_vseg_map() function, ");
                 boot_puts("PTAB too small, minumum size is: ");
@@ -802 +717 @@
             }
             // register both physical and virtual page table address
-            boot_ptabs_vaddr[vspace_id] = (page_table_t *) vobj[vobj_id].vaddr;
-            boot_ptabs_paddr[vspace_id] = (page_table_t *) vobj[vobj_id].paddr;
-
-            /* computing the number of second level page */
+            boot_ptabs_vaddr[vspace_id] = vobj[vobj_id].vaddr;
+            boot_ptabs_paddr[vspace_id] = vobj[vobj_id].paddr;
+
+            // reset all valid bits in PT1
+            for ( offset = 0 ; offset < 8192 ; offset = offset + 4)
+            {
+                boot_physical_write( cur_paddr + offset, 0);
+            }
+
+            // computing the number of second level pages
             boot_max_pt2[vspace_id] = (vobj[vobj_id].length - PT1_SIZE) / PT2_SIZE;
         }
+
         // set next vaddr/paddr
-        cur_vaddr += vobj[vobj_id].length;
-        cur_paddr += vobj[vobj_id].length;
-
+        cur_vaddr = cur_vaddr + vobj[vobj_id].length;
+        cur_paddr = cur_paddr + vobj[vobj_id].length;
     } // end for vobjs
 
     //set the vseg length
-    vseg->length = align_to((cur_paddr - vseg->pbase), 12);
+    vseg->length = vaddr_align_to((unsigned int)(cur_paddr - vseg->pbase), 12);
 
     // checking pseg overflow
     if ((vseg->pbase < pseg->base) ||
-            ((vseg->pbase + vseg->length) > (pseg->base + pseg->length))) {
+        ((vseg->pbase + vseg->length) > (pseg->base + pseg->length))) 
+    {
         boot_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
         boot_puts("impossible mapping for virtual segment: ");
@@ -825 +747 @@
         boot_puts("\n");
         boot_puts("vseg pbase = ");
-        boot_putx(vseg->pbase);
+        boot_putl(vseg->pbase);
         boot_puts("\n");
         boot_puts("vseg length = ");
@@ -831 +753 @@
         boot_puts("\n");
         boot_puts("pseg pbase = ");
-        boot_putx(pseg->base);
+        boot_putl(pseg->base);
         boot_puts("\n");
         boot_puts("pseg length = ");
-        boot_putx(pseg->length);
+        boot_putl(pseg->length);
         boot_puts("\n");
         boot_exit();
@@ -846 +768 @@
     boot_putx(vseg->vbase);
     boot_puts(" / pbase = ");
-    boot_putx(vseg->pbase);
+    boot_putl(vseg->pbase);
     boot_puts("\n");
 #endif
 
-    // set the next_base field in vseg
-    if (vseg->ident == 0 && pseg->type != PSEG_TYPE_PERI) {
+    // set the next_base field in pseg when it's a RAM
+    if ( pseg->type == PSEG_TYPE_RAM ) 
+    {
         pseg->next_base = vseg->pbase + vseg->length;
     }
-
-}                // end boot_vseg_map()
+}    // end boot_vseg_map()
 
 /////////////////////////////////////////////////////////////////////
@@ -861 +783 @@
 // structure (soft), and the giet_config file (hard).
 /////////////////////////////////////////////////////////////////////
-void boot_check_mapping() {
+void boot_check_mapping() 
+{
     mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
     mapping_cluster_t * cluster = boot_get_cluster_base(header);
@@ -867 +790 @@
 
     // checking mapping availability
-    if (header->signature != IN_MAPPING_SIGNATURE) {
+    if (header->signature != IN_MAPPING_SIGNATURE) 
+    {
         boot_puts("\n[BOOT ERROR] Illegal mapping signature: ");
         boot_putx(header->signature);
@@ -874 +798 @@
     }
     // checking number of clusters
-    if (header->clusters != NB_CLUSTERS) {
+    if (header->clusters != NB_CLUSTERS) 
+    {
         boot_puts("\n[BOOT ERROR] Incoherent NB_CLUSTERS");
         boot_puts("\n             - In giet_config,  value = ");
@@ -884 +809 @@
     }
     // checking number of virtual spaces
-    if (header->vspaces > GIET_NB_VSPACE_MAX) {
+    if (header->vspaces > GIET_NB_VSPACE_MAX) 
+    {
         boot_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
         boot_puts("\n");
@@ -894 +820 @@
     unsigned int tty_found = 0;
     unsigned int nic_found = 0;
-    for (cluster_id = 0; cluster_id < NB_CLUSTERS; cluster_id++) {
+    for (cluster_id = 0; cluster_id < NB_CLUSTERS; cluster_id++) 
+    {
         // NB_PROCS_MAX
-        if (cluster[cluster_id].procs > NB_PROCS_MAX) {
+        if (cluster[cluster_id].procs > NB_PROCS_MAX) 
+        {
             boot_puts("\n[BOOT ERROR] too many processors in cluster ");
             boot_putd(cluster_id);
@@ -907 +835 @@
         for (periph_id = cluster[cluster_id].periph_offset;
                 periph_id < cluster[cluster_id].periph_offset + cluster[cluster_id].periphs;
-                periph_id++) {
-            // NB_TTYS
-            if (periph[periph_id].type == PERIPH_TYPE_TTY) {
-                if (tty_found) {
+                periph_id++) 
+        {
+            // NB_TTY_CHANNELS
+            if (periph[periph_id].type == PERIPH_TYPE_TTY) 
+            {
+                if (tty_found) 
+                {
                     boot_puts("\n[BOOT ERROR] TTY component should not be replicated\n");
                     boot_exit();
                 }
-                if (periph[periph_id].channels > NB_TTYS) {
-                    boot_puts("\n[BOOT ERROR] Wrong NB_TTYS in cluster ");
+                if (periph[periph_id].channels > NB_TTY_CHANNELS) 
+                {
+                    boot_puts("\n[BOOT ERROR] Wrong NB_TTY_CHANNELS in cluster ");
                     boot_putd(cluster_id);
                     boot_puts(" : ttys = ");
@@ -924 +856 @@
                 tty_found = 1;
             }
-            // NB_NICS
-            if (periph[periph_id].type == PERIPH_TYPE_NIC) {
-                if (nic_found) {
+            // NB_NIC_CHANNELS
+            if (periph[periph_id].type == PERIPH_TYPE_NIC) 
+            {
+                if (nic_found) 
+                {
                     boot_puts("\n[BOOT ERROR] NIC component should not be replicated\n");
                     boot_exit();
                 }
-                if (periph[periph_id].channels != NB_NICS) {
-                    boot_puts("\n[BOOT ERROR] Wrong NB_NICS in cluster ");
+                if (periph[periph_id].channels != NB_NIC_CHANNELS) 
+                {
+                    boot_puts("\n[BOOT ERROR] Wrong NB_NIC_CHANNELS in cluster ");
                     boot_putd(cluster_id);
                     boot_puts(" : nics = ");
@@ -941 +876 @@
             }
             // NB_TIMERS
-            if (periph[periph_id].type == PERIPH_TYPE_TIM) {
-                if (periph[periph_id].channels > NB_TIMERS_MAX) {
+            if (periph[periph_id].type == PERIPH_TYPE_TIM) 
+            {
+                if (periph[periph_id].channels > NB_TIM_CHANNELS) 
+                {
                     boot_puts("\n[BOOT ERROR] Too much user timers in cluster ");
                     boot_putd(cluster_id);
@@ -952 +889 @@
             }
             // NB_DMAS
-            if (periph[periph_id].type == PERIPH_TYPE_DMA) {
-                if (periph[periph_id].channels != NB_DMAS_MAX) {
+            if (periph[periph_id].type == PERIPH_TYPE_DMA) 
+            {
+                if (periph[periph_id].channels != NB_DMA_CHANNELS) 
+                {
                     boot_puts("\n[BOOT ERROR] Too much DMA channels in cluster ");
                     boot_putd(cluster_id);
                     boot_puts(" : channels = ");
                     boot_putd(periph[periph_id].channels);
-                    boot_puts(" - NB_DMAS_MAX : ");
-                    boot_putd(NB_DMAS_MAX);
+                    boot_puts(" - NB_DMA_CHANNELS : ");
+                    boot_putd(NB_DMA_CHANNELS);
                     boot_puts("\n");
                     boot_exit();
@@ -968 +907 @@
 } // end boot_check_mapping()
 
-
 /////////////////////////////////////////////////////////////////////
 // This function initialises the physical pages table allocators 
 // for all psegs (i.e. next_base field of the pseg). 
-// In each cluster containing processors, it reserve space for the
-// schedulers in the first RAM pseg found (4k bytes per processor). 
 /////////////////////////////////////////////////////////////////////
-void boot_psegs_init() {
-    mapping_header_t * header = (mapping_header_t *) &seg_mapping_base;
-
-    mapping_cluster_t * cluster = boot_get_cluster_base(header);
-    mapping_pseg_t * pseg = boot_get_pseg_base(header);
+void boot_psegs_init() 
+{
+    mapping_header_t* header   = (mapping_header_t *) &seg_mapping_base;
+    mapping_cluster_t* cluster = boot_get_cluster_base(header);
+    mapping_pseg_t* pseg       = boot_get_pseg_base(header);
 
     unsigned int cluster_id;
     unsigned int pseg_id;
-    unsigned int found;
 
 #if BOOT_DEBUG_PT
-    boot_puts
-        ("\n[BOOT DEBUG] ****** psegs allocators nitialisation ******\n");
-#endif
-
-    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) {
-        if (cluster[cluster_id].procs > NB_PROCS_MAX) {
+boot_puts ("\n[BOOT DEBUG] ****** psegs allocators initialisation ******\n");
+#endif
+
+    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) 
+    {
+        if (cluster[cluster_id].procs > NB_PROCS_MAX) 
+        {
             boot_puts("\n[BOOT ERROR] The number of processors in cluster ");
             boot_putd(cluster_id);
@@ -998 +934 @@
         }
 
-        found = 0;
-
         for (pseg_id = cluster[cluster_id].pseg_offset;
                 pseg_id < cluster[cluster_id].pseg_offset + cluster[cluster_id].psegs;
-                pseg_id++) {
-            unsigned int free = pseg[pseg_id].base;
-
-            if ((pseg[pseg_id].type == PSEG_TYPE_RAM) && (found == 0)) {
-                free = free + (cluster[cluster_id].procs << 12);
-                found = 1;
-            }
-            pseg[pseg_id].next_base = free;
+                pseg_id++) 
+        {
+            pseg[pseg_id].next_base = pseg[pseg_id].base;
 
 #if BOOT_DEBUG_PT
-            boot_puts("cluster ");
-            boot_putd(cluster_id);
-            boot_puts(" / pseg ");
-            boot_puts(pseg[pseg_id].name);
-            boot_puts(" : next_base = ");
-            boot_putx(pseg[pseg_id].next_base);
-            boot_puts("\n");
+boot_puts("cluster ");
+boot_putd(cluster_id);
+boot_puts(" / pseg ");
+boot_puts(pseg[pseg_id].name);
+boot_puts(" : next_base = ");
+boot_putl(pseg[pseg_id].next_base);
+boot_puts("\n");
 #endif
         }
     }
 } // end boot_psegs_init()
-
 
 /////////////////////////////////////////////////////////////////////
 // This function builds the page tables for all virtual spaces 
-// defined in the mapping_info data structure.
-// For each virtual space, it maps both the global vsegs 
-// (replicated in all vspaces), and the private vsegs.
+// defined in the mapping_info data structure, in three steps:
+// - step 1 : It computes the physical base address for global vsegs
+//            and for all associated vobjs.
+// - step 2 : It computes the physical base address for all private 
+//            vsegs and all vobjs in each virtual space.
+// - step 3 : It actually fill the page table for each vspace.
 /////////////////////////////////////////////////////////////////////
-void boot_pt_init() {
+void boot_pt_init() 
+{
     mapping_header_t * header = (mapping_header_t *) &seg_mapping_base;
-
     mapping_vspace_t * vspace = boot_get_vspace_base(header);
-    mapping_vseg_t * vseg = boot_get_vseg_base(header);
+    mapping_vseg_t   * vseg   = boot_get_vseg_base(header);
 
     unsigned int vspace_id;
@@ -1041 +972 @@
 
 #if BOOT_DEBUG_PT
-    boot_puts("\n[BOOT DEBUG] ****** mapping global vsegs ******\n");
-#endif
-
-    // step 1 : first loop on virtual spaces to map global vsegs
-    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) {
+boot_puts("\n[BOOT DEBUG] ****** mapping global vsegs ******\n");
+#endif
+
+    // step 1 : loop on virtual spaces to map global vsegs
+    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) 
+    {
         boot_vseg_map(&vseg[vseg_id], ((unsigned int) (-1)));
     }
 
     // step 2 : loop on virtual vspaces to map private vsegs
-    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) {
+    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
+    {
 
 #if BOOT_DEBUG_PT
-        boot_puts("\n[BOOT DEBUG] ****** mapping private vsegs in vspace ");
-        boot_puts(vspace[vspace_id].name);
-        boot_puts(" ******\n");
+boot_puts("\n[BOOT DEBUG] ****** mapping private vsegs in vspace ");
+boot_puts(vspace[vspace_id].name);
+boot_puts(" ******\n");
 #endif
 
         for (vseg_id = vspace[vspace_id].vseg_offset;
                 vseg_id < (vspace[vspace_id].vseg_offset + vspace[vspace_id].vsegs);
-                vseg_id++) {
+                vseg_id++) 
+        {
             boot_vseg_map(&vseg[vseg_id], vspace_id);
         }
@@ -1066 +1000 @@
 
     // step 3 : loop on the vspaces to build the page tables
-    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) {
-
+    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
+    {
 #if BOOT_DEBUG_PT
-        boot_puts("\n[BOOT DEBUG] ****** building page table for vspace ");
-        boot_puts(vspace[vspace_id].name);
-        boot_puts(" ******\n");
-#endif
-
+boot_puts("\n[BOOT DEBUG] ****** building page table for vspace ");
+boot_puts(vspace[vspace_id].name);
+boot_puts(" ******\n");
+#endif
         boot_vspace_pt_build(vspace_id);
 
 #if BOOT_DEBUG_PT
-        boot_puts("\n>>> page table physical address = ");
-        boot_putx((unsigned int) boot_ptabs_paddr[vspace_id]);
-        boot_puts(", page table number of PT2 = ");
-        boot_putd((unsigned int) boot_max_pt2[vspace_id]);
-        boot_puts("\n");
+boot_puts("\n>>> page table physical address = ");
+boot_putl(boot_ptabs_paddr[vspace_id]);
+boot_puts(", number of PT2 = ");
+boot_putd((unsigned int) boot_max_pt2[vspace_id]);
+boot_puts("\n");
 #endif
     }
 } // end boot_pt_init()
-
 
 ///////////////////////////////////////////////////////////////////////////////
@@ -1091 +1023 @@
 // such as mwmr channels, barriers and locks, because these vobjs 
 // are not known, and not initialized by the compiler.
+// Warning : The MMU is supposed to be activated...
 ///////////////////////////////////////////////////////////////////////////////
-void boot_vobjs_init() {
-    mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
-    mapping_vspace_t * vspace = boot_get_vspace_base(header);
-    mapping_vobj_t * vobj = boot_get_vobj_base(header);
+void boot_vobjs_init() 
+{
+    mapping_header_t* header = (mapping_header_t *) & seg_mapping_base;
+    mapping_vspace_t* vspace = boot_get_vspace_base(header);
+    mapping_vobj_t* vobj     = boot_get_vobj_base(header);
 
     unsigned int vspace_id;
     unsigned int vobj_id;
 
-    // loop on the vspaces 
-    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) {
+    // loop on the vspaces
+    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
+    {
 
 #if BOOT_DEBUG_VOBJS
-        boot_puts("\n[BOOT DEBUG] ****** vobjs initialisation in vspace ");
-        boot_puts(vspace[vspace_id].name);
-        boot_puts(" ******\n");
+boot_puts("\n[BOOT DEBUG] ****** vobjs initialisation in vspace ");
+boot_puts(vspace[vspace_id].name);
+boot_puts(" ******\n");
 #endif
 
@@ -1113 +1048 @@
         // loop on the vobjs
         for (vobj_id = vspace[vspace_id].vobj_offset;
-                vobj_id < (vspace[vspace_id].vobj_offset + vspace[vspace_id].vobjs);
-                vobj_id++) {
-            switch (vobj[vobj_id].type) {
+             vobj_id < (vspace[vspace_id].vobj_offset + vspace[vspace_id].vobjs);
+             vobj_id++) 
+        {
+            switch (vobj[vobj_id].type) 
+            {
                 case VOBJ_TYPE_MWMR:    // storage capacity is (vobj.length/4 - 5) words
                 {
-                    mwmr_channel_t * mwmr = (mwmr_channel_t *) (vobj[vobj_id].paddr);
+                    mwmr_channel_t* mwmr = (mwmr_channel_t *) (vobj[vobj_id].vaddr);
                     mwmr->ptw = 0;
                     mwmr->ptr = 0;
@@ -1126 +1063 @@
                     mwmr->lock = 0;
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("MWMR    : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / depth = ");
-                    boot_putd(mwmr->depth);
-                    boot_puts(" / width = ");
-                    boot_putd(mwmr->width);
-                    boot_puts("\n");
+boot_puts("MWMR    : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / depth = ");
+boot_putd(mwmr->depth);
+boot_puts(" / width = ");
+boot_putd(mwmr->width);
+boot_puts("\n");
 #endif
                     break;
@@ -1139 +1076 @@
                 {
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("ELF     : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / length = ");
-                    boot_putx(vobj[vobj_id].length);
-                    boot_puts("\n");
+boot_puts("ELF     : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / length = ");
+boot_putx(vobj[vobj_id].length);
+boot_puts("\n");
 #endif
                     break;
@@ -1150 +1087 @@
                 {
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("BLOB     : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / length = ");
-                    boot_putx(vobj[vobj_id].length);
-                    boot_puts("\n");
+boot_puts("BLOB     : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / length = ");
+boot_putx(vobj[vobj_id].length);
+boot_puts("\n");
 #endif
                     break;
@@ -1160 +1097 @@
                 case VOBJ_TYPE_BARRIER:    // init is the number of participants
                 {
-                    giet_barrier_t * barrier = (giet_barrier_t *) (vobj[vobj_id].paddr);
+                    giet_barrier_t* barrier = (giet_barrier_t *) (vobj[vobj_id].vaddr);
                     barrier->count = vobj[vobj_id].init;
                     barrier->init = vobj[vobj_id].init;
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("BARRIER : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / init_value = ");
-                    boot_putd(barrier->init);
-                    boot_puts("\n");
+boot_puts("BARRIER : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / init_value = ");
+boot_putd(barrier->init);
+boot_puts("\n");
 #endif
                     break;
                 }
-                case VOBJ_TYPE_LOCK:    // init is "not taken"
-                {
-                    unsigned int * lock = (unsigned int *) (vobj[vobj_id].paddr);
+                case VOBJ_TYPE_LOCK:    // init value is "not taken"
+                {
+                    unsigned int* lock = (unsigned int *) (vobj[vobj_id].vaddr);
                     *lock = 0;
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("LOCK    : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts("\n");
+boot_puts("LOCK    : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts("\n");
 #endif
                     break;
@@ -1186 +1123 @@
                 {
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("BUFFER  : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / paddr = ");
-                    boot_putx(vobj[vobj_id].paddr);
-                    boot_puts(" / length = ");
-                    boot_putx(vobj[vobj_id].length);
-                    boot_puts("\n");
+boot_puts("BUFFER  : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / paddr = ");
+boot_putx(vobj[vobj_id].paddr);
+boot_puts(" / length = ");
+boot_putx(vobj[vobj_id].length);
+boot_puts("\n");
 #endif
                     break;
@@ -1198 +1135 @@
                 case VOBJ_TYPE_MEMSPACE:
                 {
-                    giet_memspace_t * memspace = (giet_memspace_t *) vobj[vobj_id].paddr;
+                    giet_memspace_t* memspace = (giet_memspace_t *) vobj[vobj_id].vaddr;
                     memspace->buffer = (void *) vobj[vobj_id].vaddr + 8;
                     memspace->size = vobj[vobj_id].length - 8;
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("MEMSPACE  : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / paddr = ");
-                    boot_putx(vobj[vobj_id].paddr);
-                    boot_puts(" / vaddr = ");
-                    boot_putx(vobj[vobj_id].vaddr);
-                    boot_puts(" / length = ");
-                    boot_putx(vobj[vobj_id].length);
-                    boot_puts(" / buffer = ");
-                    boot_putx(memspace->buffer);
-                    boot_puts(" / size = ");
-                    boot_putx(memspace->size);
-                    boot_puts("\n");
+boot_puts("MEMSPACE  : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / vaddr = ");
+boot_putx(vobj[vobj_id].vaddr);
+boot_puts(" / length = ");
+boot_putx(vobj[vobj_id].length);
+boot_puts(" / buffer = ");
+boot_putx((unsigned int)memspace->buffer);
+boot_puts(" / size = ");
+boot_putx(memspace->size);
+boot_puts("\n");
 #endif
                     break;
@@ -1222 +1157 @@
                     ptab_found = 1;
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("PTAB    : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / length = ");
-                    boot_putx(vobj[vobj_id].length);
-                    boot_puts("\n");
+boot_puts("PTAB    : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / length = ");
+boot_putx(vobj[vobj_id].length);
+boot_puts("\n");
 #endif
                     break;
@@ -1232 +1167 @@
                 case VOBJ_TYPE_CONST:
                 {
-                    unsigned int *addr = (unsigned int *) vobj[vobj_id].paddr;
+                    unsigned int* addr = (unsigned int *) vobj[vobj_id].vaddr;
                     *addr = vobj[vobj_id].init;
 #if BOOT_DEBUG_VOBJS
-                    boot_puts("CONST   : ");
-                    boot_puts(vobj[vobj_id].name);
-                    boot_puts(" / Paddr :");
-                    boot_putx(vobj[vobj_id].paddr);
-                    boot_puts(" / init = ");
-                    boot_putx(*addr);
-                    boot_puts("\n");
+boot_puts("CONST   : ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" / Paddr :");
+boot_putx(vobj[vobj_id].paddr);
+boot_puts(" / init = ");
+boot_putx(*addr);
+boot_puts("\n");
 #endif
                     break;
@@ -1247 +1182 @@
                 default:
                 {
-                    boot_puts("\n[INIT ERROR] illegal vobj type: ");
+                    boot_puts("\n[BOOT ERROR] illegal vobj type: ");
                     boot_putd(vobj[vobj_id].type);
                     boot_puts("\n");
@@ -1254 +1189 @@
             }            // end switch type
         }            // end loop on vobjs
-        if (ptab_found == 0) {
-            boot_puts("\n[INIT ERROR] Missing PTAB for vspace ");
+        if (ptab_found == 0) 
+        {
+            boot_puts("\n[BOOT ERROR] Missing PTAB for vspace ");
             boot_putd(vspace_id);
             boot_exit();
@@ -1262 +1198 @@
 } // end boot_vobjs_init()
 
-
-void mwmr_hw_init(void * coproc, enum mwmrPortDirection way,
-        unsigned int no, const mwmr_channel_t * pmwmr) {
-    volatile unsigned int *cbase = (unsigned int *) coproc;
-
-    cbase[MWMR_CONFIG_FIFO_WAY] = way;
-    cbase[MWMR_CONFIG_FIFO_NO] = no;
-    cbase[MWMR_CONFIG_STATUS_ADDR] = (unsigned int) pmwmr;
-    cbase[MWMR_CONFIG_WIDTH] = pmwmr->width;
-    cbase[MWMR_CONFIG_DEPTH] = pmwmr->depth;
-    cbase[MWMR_CONFIG_BUFFER_ADDR] = (unsigned int) &pmwmr->data;
-    cbase[MWMR_CONFIG_RUNNING] = 1;
-}
-
+////////////////////////////////////////////////////////////////////////////////
+// This function initializes one MWMR controller channel.
+// - coproc_pbase  : physical base address of the Coproc configuration segment
+// - channel_pbase : physical base address of the MWMR channel segment
+// Warning : the channel physical base address should be on 32 bits, as the
+// MWMR controller configuration registers are 32 bits.
+// TODO : Introduce a MWMR_CONFIG_PADDR_EXT register in the MWMR coprocessor
+//        To support addresses > 32 bits and remove this limitation...
+/////////////////////////////////////////////////////////////////////////////// 
+void mwmr_hw_init(paddr_t                coproc_pbase, 
+                  enum mwmrPortDirection way,
+                  unsigned int           no, 
+                  paddr_t                channel_pbase) 
+{
+    if ( (channel_pbase>>32) != 0 )
+    {
+        boot_puts("\n[BOOT ERROR] MWMR controller does not support address > 32 bits\n");
+        boot_exit();
+    }
+
+    unsigned int lsb = (unsigned int)channel_pbase;
+//  unsigned int msb = (unsigned int)(channel_pbase>>32);
+
+    unsigned int depth = boot_physical_read( channel_pbase + 16 );
+    unsigned int width = boot_physical_read( channel_pbase + 20 );
+
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_FIFO_WAY*4, way );
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_FIFO_NO*4, no );
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_WIDTH*4, width);
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_DEPTH*4, depth);
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_STATUS_ADDR*4, lsb);
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_BUFFER_ADDR*4, lsb + 24 );
+//  boot_physical_write( coproc_pbase + MWMR_CONFIG_PADDR_EXT*4, msb);
+    boot_physical_write( coproc_pbase + MWMR_CONFIG_RUNNING*4, 1 );
+}
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -1281 +1238 @@
 // in the mapping_info file.
 ////////////////////////////////////////////////////////////////////////////////
-void boot_peripherals_init() {
+void boot_peripherals_init() 
+{
     mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
     mapping_cluster_t * cluster = boot_get_cluster_base(header);
@@ -1297 +1255 @@
     unsigned int channel_id;
 
-    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) {
+    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) 
+    {
 
 #if BOOT_DEBUG_PERI
-        boot_puts
-            ("\n[BOOT DEBUG] ****** peripheral initialisation in cluster ");
-        boot_putd(cluster_id);
-        boot_puts(" ******\n");
+boot_puts("\n[BOOT DEBUG] ****** peripherals initialisation in cluster ");
+boot_putd(cluster_id);
+boot_puts(" ******\n");
 #endif
 
         for (periph_id = cluster[cluster_id].periph_offset;
-                periph_id < cluster[cluster_id].periph_offset +
-                cluster[cluster_id].periphs; periph_id++) {
+             periph_id < cluster[cluster_id].periph_offset +
+             cluster[cluster_id].periphs; periph_id++) 
+        {
             unsigned int type = periph[periph_id].type;
             unsigned int channels = periph[periph_id].channels;
             unsigned int pseg_id = periph[periph_id].psegid;
 
-            unsigned int * pseg_base = (unsigned int *) pseg[pseg_id].base;
+            paddr_t pbase = pseg[pseg_id].base;
 
 #if BOOT_DEBUG_PERI
-            boot_puts("- peripheral type : ");
-            boot_putd(type);
-            boot_puts(" / address = ");
-            boot_putx((unsigned int) pseg_base);
-            boot_puts(" / channels = ");
-            boot_putd(channels);
-            boot_puts("\n");
-#endif
-
-            switch (type) {
+boot_puts("- peripheral type : ");
+boot_putd(type);
+boot_puts(" / pbase = ");
+boot_putl(pbase);
+boot_puts(" / channels = ");
+boot_putd(channels);
+boot_puts("\n");
+#endif
+
+            switch (type) 
+            {
                 case PERIPH_TYPE_IOC:    // vci_block_device component
-                    pseg_base[BLOCK_DEVICE_IRQ_ENABLE] = 1;
+                {
+                    paddr_t paddr = pbase + BLOCK_DEVICE_IRQ_ENABLE*4;
+                    boot_physical_write(paddr, 1);
 #if BOOT_DEBUG_PERI
-                    boot_puts("- IOC initialised\n");
-#endif
-                    break;
-
+boot_puts("- IOC initialised\n");
+#endif
+                }
+                break;
                 case PERIPH_TYPE_DMA:    // vci_multi_dma component
-                    for (channel_id = 0; channel_id < channels; channel_id++) {
-                        pseg_base[DMA_IRQ_DISABLE + channel_id * DMA_SPAN] = 0;
+                    for (channel_id = 0; channel_id < channels; channel_id++) 
+                    {
+                        paddr_t paddr = pbase + (channel_id*DMA_SPAN + DMA_IRQ_DISABLE) * 4;
+                        boot_physical_write(paddr, 0);
                     }
 #if BOOT_DEBUG_PERI
-                    boot_puts("- DMA initialised\n");
-#endif
-                    break;
-
+boot_puts("- DMA initialised\n");
+#endif
+                break;
                 case PERIPH_TYPE_NIC:    // vci_multi_nic component
-                    for (channel_id = 0; channel_id < channels; channel_id++) {
+                    for (channel_id = 0; channel_id < channels; channel_id++) 
+                    {
                         // TODO
                     }
 #if BOOT_DEBUG_PERI
-                    boot_puts("- NIC initialised\n");
-#endif
-                    break;
-
+boot_puts("- NIC initialised\n");
+#endif
+                break;
                 case PERIPH_TYPE_TTY:    // vci_multi_tty component
 #if BOOT_DEBUG_PERI
-                    boot_puts("- TTY initialised\n");
-#endif
-                    break;
-
+boot_puts("- TTY initialised\n");
+#endif
+                break;
                 case PERIPH_TYPE_IOB:    // vci_io_bridge component
-                    if (IOMMU_ACTIVE) {
+                    if (IOMMU_ACTIVE) 
+                    {
                         // TODO
                         // get the iommu page table physical address
@@ -1368 +1331 @@
                     }
 #if BOOT_DEBUG_PERI
-                    boot_puts("- IOB initialised\n");
-#endif
-                    break;
-            }            // end switch periph type
-        }            // end for periphs
+boot_puts("- IOB initialised\n");
+#endif
+                break;
+            }  // end switch periph type
+        }  // end for periphs
 
 #if BOOT_DEBUG_PERI
-        boot_puts
-            ("\n[BOOT DEBUG] ****** coprocessors initialisation in cluster ");
-        boot_putd(cluster_id);
-        boot_puts(" ******\n");
+boot_puts("\n[BOOT DEBUG] ****** coprocessors initialisation in cluster ");
+boot_putd(cluster_id);
+boot_puts(" ******\n");
 #endif
 
         for (coproc_id = cluster[cluster_id].coproc_offset;
-                coproc_id < cluster[cluster_id].coproc_offset +
-                cluster[cluster_id].coprocs; coproc_id++) {
-            unsigned no_fifo_to = 0;    //FIXME: should it be the map.xml who define the order?
+             coproc_id < cluster[cluster_id].coproc_offset +
+             cluster[cluster_id].coprocs; coproc_id++) 
+        {
+            unsigned no_fifo_to = 0;    //FIXME: should the map.xml define the order?
             unsigned no_fifo_from = 0;
-            unsigned int cpseg = pseg[coproc[coproc_id].psegid].base;
+
+            // Get physical base address for MWMR controler
+            paddr_t coproc_pbase = pseg[coproc[coproc_id].psegid].base;
 
 #if BOOT_DEBUG_PERI
-            boot_puts("- coprocessor name : ");
-            boot_puts(coproc[coproc_id].name);
-            boot_puts(" / nb ports = ");
-            boot_putd((unsigned int) coproc[coproc_id].ports);
-            boot_puts("\n");
+boot_puts("- coprocessor name : ");
+boot_puts(coproc[coproc_id].name);
+boot_puts(" / nb ports = ");
+boot_putd((unsigned int) coproc[coproc_id].ports);
+boot_puts("\n");
 #endif
 
             for (cp_port_id = coproc[coproc_id].port_offset;
-                    cp_port_id < coproc[coproc_id].port_offset + coproc[coproc_id].ports;
-                    cp_port_id++) {
-                //FIXME: the vspace_id should be the same for all ports: put it in the coproc?
+                 cp_port_id < coproc[coproc_id].port_offset + coproc[coproc_id].ports;
+                 cp_port_id++) 
+            {
                 unsigned int vspace_id = cp_port[cp_port_id].vspaceid;
-                unsigned int vobj_id = cp_port[cp_port_id].mwmr_vobjid + vspace[vspace_id].vobj_offset;
-
-                mwmr_channel_t * pmwmr = (mwmr_channel_t *) (vobj[vobj_id].paddr);
-
-                if (cp_port[cp_port_id].direction == PORT_TO_COPROC) {
+                unsigned int vobj_id = cp_port[cp_port_id].mwmr_vobjid + 
+                                          vspace[vspace_id].vobj_offset;
+
+                // Get MWMR channel base address 
+                paddr_t channel_pbase = vobj[vobj_id].paddr;
+
+                if (cp_port[cp_port_id].direction == PORT_TO_COPROC) 
+                {
 #if BOOT_DEBUG_PERI
-                    boot_puts("     port direction: PORT_TO_COPROC");
-#endif
-                    mwmr_hw_init((void *) cpseg, PORT_TO_COPROC, no_fifo_to, pmwmr);
+boot_puts("     port direction: PORT_TO_COPROC");
+#endif
+                    mwmr_hw_init(coproc_pbase, 
+                                 PORT_TO_COPROC, 
+                                 no_fifo_to, 
+                                 channel_pbase);
                     no_fifo_to++;
                 }
-                else {
+                else 
+                {
 #if BOOT_DEBUG_PERI
-                    boot_puts("     port direction: PORT_FROM_COPROC");
-#endif
-                    mwmr_hw_init((void *) cpseg, PORT_FROM_COPROC, no_fifo_from, pmwmr);
+boot_puts("     port direction: PORT_FROM_COPROC");
+#endif
+                    mwmr_hw_init(coproc_pbase, 
+                                 PORT_FROM_COPROC, 
+                                 no_fifo_from, 
+                                 channel_pbase);
                     no_fifo_from++;
                 }
 #if BOOT_DEBUG_PERI
-                boot_puts(", with mwmr: ");
-                boot_puts(vobj[vobj_id].name);
-                boot_puts(" of vspace: ");
-                boot_puts(vspace[vspace_id].name);
-#endif
-            }
+boot_puts(", with mwmr: ");
+boot_puts(vobj[vobj_id].name);
+boot_puts(" of vspace: ");
+boot_puts(vspace[vspace_id].name);
+#endif
+            } // end for cp_ports
         } // end for coprocs
     } // end for clusters
 } // end boot_peripherals_init()
 
+///////////////////////////////////////////////////////////////////////////////
+// This function returns in the vbase and length buffers the virtual base 
+// address and the length of the  segment allocated to the schedulers array 
+// in the cluster defined by the clusterid argument.
+///////////////////////////////////////////////////////////////////////////////
+void boot_get_sched_vaddr( unsigned int  cluster_id,
+                           unsigned int* vbase, 
+                           unsigned int* length )
+{
+    mapping_header_t* header = (mapping_header_t *) & seg_mapping_base;
+    mapping_vobj_t*   vobj   = boot_get_vobj_base(header);
+    mapping_vseg_t*   vseg   = boot_get_vseg_base(header);
+    mapping_pseg_t*   pseg   = boot_get_pseg_base(header);
+
+    unsigned int vseg_id;
+    unsigned int found = 0;
+
+    for ( vseg_id = 0 ; (vseg_id < header->vsegs) && (found == 0) ; vseg_id++ )
+    {
+        if ( (vobj[vseg[vseg_id].vobj_offset].type == VOBJ_TYPE_SCHED) && 
+             (pseg[vseg[vseg_id].psegid].cluster == cluster_id ) )
+        {
+            *vbase  = vseg[vseg_id].vbase;
+            *length = vobj[vseg[vseg_id].vobj_offset].length;
+            found = 1;
+        }
+    }
+    if ( found == 0 )
+    {
+        boot_puts("\n[BOOT ERROR] No vobj of type SCHED in cluster ");
+        boot_putd(cluster_id);
+        boot_puts("\n");
+        boot_exit();
+    }
+} // end boot_get_sched_vaddr()
 
 ///////////////////////////////////////////////////////////////////////////////
 // This function initialises all processors schedulers.
 // This is done by processor 0, and the MMU must be activated.
-// It initialises the boot_schedulers_paddr[gpid] pointers array.
+// It initialises the boot_chedulers[gpid] pointers array.
 // Finally, it scan all tasks in all vspaces to initialise the tasks contexts, 
 // as specified in the mapping_info data structure. 
 // For each task, a TTY channel, a TIMER channel, a FBDMA channel, and a NIC
-// channel can be allocated if required. 
+// channel are allocated if required. 
 ///////////////////////////////////////////////////////////////////////////////
-void boot_schedulers_init() {
-    mapping_header_t * header = (mapping_header_t *) & seg_mapping_base;
-    mapping_cluster_t * cluster = boot_get_cluster_base(header);
-    mapping_pseg_t * pseg = boot_get_pseg_base(header);
-    mapping_vspace_t * vspace = boot_get_vspace_base(header);
-    mapping_task_t * task = boot_get_task_base(header);
-    mapping_vobj_t * vobj = boot_get_vobj_base(header);
-    mapping_proc_t * proc = boot_get_proc_base(header);
-    mapping_irq_t * irq = boot_get_irq_base(header);
-
-    unsigned int alloc_tty_channel;    // TTY channel allocator
-    unsigned int alloc_nic_channel;    // NIC channel allocator
+void boot_schedulers_init() 
+{
+    mapping_header_t*  header  = (mapping_header_t *) & seg_mapping_base;
+    mapping_cluster_t* cluster = boot_get_cluster_base(header);
+    mapping_vspace_t*  vspace  = boot_get_vspace_base(header);
+    mapping_task_t*    task    = boot_get_task_base(header);
+    mapping_vobj_t*    vobj    = boot_get_vobj_base(header);
+    mapping_proc_t*    proc    = boot_get_proc_base(header);
+    mapping_irq_t*     irq     = boot_get_irq_base(header);
+
+    unsigned int cluster_id;    // cluster index in mapping_info 
+    unsigned int proc_id;       // processor index in mapping_info 
+    unsigned int irq_id;        // irq index in mapping_info
+    unsigned int vspace_id;     // vspace index in mapping_info
+    unsigned int task_id;       // task index in mapping_info
+
+    unsigned int alloc_tty_channel = 1;            // TTY channel allocator
+    unsigned int alloc_nic_channel = 0;            // NIC channel allocator
+    unsigned int alloc_cma_channel = 0;            // CMA channel allocator
+    unsigned int alloc_ioc_channel = 0;            // IOC channel allocator
     unsigned int alloc_dma_channel[NB_CLUSTERS];   // DMA channel allocators
-    unsigned int alloc_timer_channel[NB_CLUSTERS]; // user TIMER allocators
-
-    unsigned int cluster_id; // cluster global index 
-    unsigned int proc_id;    // processor global index 
-    unsigned int irq_id;     // irq global index 
-    unsigned int pseg_id;    // pseg global index 
-    unsigned int vspace_id;  // vspace global index 
-    unsigned int task_id;    // task global index;
-
-    // Step 0 : TTY, NIC, TIMERS and DMA channels allocators initialisation
-    //          global_id = cluster_id*NB_*_MAX + loc_id
-    //          - TTY[0] is reserved for the kernel
-    //          - In all clusters the first NB_PROCS_MAX timers 
-    //            are reserved for the kernel (context switch)
-
-    alloc_tty_channel = 1;
-    alloc_nic_channel = 0;
-
-    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) {
+    unsigned int alloc_tim_channel[NB_CLUSTERS];   // user TIMER allocators
+
+    /////////////////////////////////////////////////////////////////////////
+    // Step 1 : loop on the clusters and on the processors 
+    //          to initialize the schedulers[] array of pointers and
+    //          the interrupt vectors.
+    // Implementation note:
+    // We need to use both proc_id to scan the mapping info structure,
+    // and lpid to access the schedulers array.
+    // - the boot_schedulers[] array of pointers can contain "holes", because
+    //   it is indexed by the global pid = cluster_id*NB_PROCS_MAX + ltid
+    // - the mapping info array of processors is contiguous, it is indexed 
+    //   by proc_id, and use an offset specific in each cluster.
+
+    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) 
+    {
+
+#if BOOT_DEBUG_SCHED
+boot_puts("\n[BOOT DEBUG] Initialise schedulers in cluster ");
+boot_putd(cluster_id);
+boot_puts("\n");
+#endif
+
+        // TTY, NIC, CMA, IOC, TIM and DMA channels allocators 
+        // - TTY[0] is reserved for the kernel
+        // - In all clusters the first NB_PROCS_MAX timers 
+        //   are reserved for the kernel (context switch)
+
         alloc_dma_channel[cluster_id] = 0;
-        alloc_timer_channel[cluster_id] = 0;
-    }
-
-    // Step 1 : loop on the clusters and on the processors 
-    //          - initialise the boot_schedulers_paddr[] pointers array 
-    //          - initialise the interrupt vectors for each processor.
-
-    for (cluster_id = 0; cluster_id < header->clusters; cluster_id++) {
-
-#if BOOT_DEBUG_SCHED
-        boot_puts("\n[BOOT DEBUG] Initialise schedulers / IT vector in cluster ");
-        boot_putd(cluster_id);
-        boot_puts("\n");
-#endif
-        unsigned int found = 0;
-        unsigned int pseg_pbase;    // pseg base address 
-        unsigned int lpid;    // processor local index
-
-        // get the physical base address of the first PSEG_TYPE_RAM pseg in cluster
-        for (pseg_id = cluster[cluster_id].pseg_offset;
-                pseg_id < cluster[cluster_id].pseg_offset + cluster[cluster_id].psegs;
-                pseg_id++) {
-            if (pseg[pseg_id].type == PSEG_TYPE_RAM) {
-                pseg_pbase = pseg[pseg_id].base;
-                found = 1;
-                break;
-            }
-        }
-
-        if ((cluster[cluster_id].procs > 0) && (found == 0)) {
-            boot_puts("\n[BOOT ERROR] Missing RAM pseg in cluster ");
+        alloc_tim_channel[cluster_id] = NB_PROCS_MAX;
+
+        unsigned int  lpid;          // processor local index in cluster
+        unsigned int  sched_vbase;   // schedulers segment virtual base address
+        unsigned int  sched_length;  // schedulers segment length
+        unsigned int  nprocs;        // number of processors in cluster
+
+        nprocs = cluster[cluster_id].procs;
+
+        // checking processors number
+        if ( nprocs > NB_PROCS_MAX )
+        {
+            boot_puts("\n[BOOT ERROR] Too much processors in cluster ");
             boot_putd(cluster_id);
             boot_puts("\n");
             boot_exit();
         }
-        // 4 Kbytes per scheduler
-        for (lpid = 0; lpid < cluster[cluster_id].procs; lpid++) {
-            boot_schedulers_paddr[cluster_id * NB_PROCS_MAX + lpid] = (static_scheduler_t *) (pseg_pbase + (lpid << 12));
+ 
+        // get scheduler array virtual base address for cluster_id
+        boot_get_sched_vaddr( cluster_id, &sched_vbase, &sched_length );
+
+        // each processor scheduler requires 1 Kbytes
+        if ( sched_length < (nprocs<<10) ) 
+        {
+            boot_puts("\n[BOOT ERROR] Schedulers segment too small in cluster ");
+            boot_putd(cluster_id);
+            boot_puts("\n");
+            boot_exit();
         }
 
-        for (proc_id = cluster[cluster_id].proc_offset;
-                proc_id < cluster[cluster_id].proc_offset + cluster[cluster_id].procs;
-                proc_id++) {
+        for ( proc_id = cluster[cluster_id].proc_offset, lpid = 0 ;
+              proc_id < cluster[cluster_id].proc_offset + cluster[cluster_id].procs;
+              proc_id++, lpid++ ) 
+        {
+            // set the schedulers pointers array
+            boot_schedulers[cluster_id * NB_PROCS_MAX + lpid] =
+               (static_scheduler_t*)( sched_vbase + (lpid<<10) );
 
 #if BOOT_DEBUG_SCHED
-            boot_puts("\nProc ");
-            boot_putd(proc_id);
-            boot_puts(" : scheduler pbase = ");
-            boot_putx(pseg_pbase + (proc_id << 12));
-            boot_puts("\n");
-#endif
-            // initialise the "tasks" variable in scheduler
-            boot_scheduler_set_tasks(proc_id, 0);
+boot_puts("\nProc ");
+boot_putd(lpid);
+boot_puts(" : scheduler virtual base address = ");
+boot_putx( sched_vbase + (lpid<<10) );
+boot_puts("\n");
+#endif
+            // current processor scheduler pointer : psched
+            static_scheduler_t* psched = (static_scheduler_t*)(sched_vbase+(lpid<<10));
+
+            // initialise the "tasks" variable
+            psched->tasks = 0;
 
             // initialise the interrupt_vector with ISR_DEFAULT
             unsigned int slot;
-            for (slot = 0; slot < 32; slot++) {
-                boot_scheduler_set_itvector(proc_id, slot, 0);
-            }
+            for (slot = 0; slot < 32; slot++) psched->interrupt_vector[slot] = 0;
 
             // scan the IRQs actually allocated to current processor
             for (irq_id = proc[proc_id].irq_offset;
-                    irq_id < proc[proc_id].irq_offset + proc[proc_id].irqs;
-                    irq_id++) {
+                 irq_id < proc[proc_id].irq_offset + proc[proc_id].irqs;
+                 irq_id++) 
+            {
                 unsigned int type = irq[irq_id].type;
                 unsigned int icu_id = irq[irq_id].icuid;
@@ -1542 +1565 @@
                 unsigned int channel = irq[irq_id].channel;
                 unsigned int value = isr_id | (type << 8) | (channel << 16);
-                boot_scheduler_set_itvector(proc_id, icu_id, value);
+                psched->interrupt_vector[icu_id] = value;
 
 #if BOOT_DEBUG_SCHED
-                boot_puts("- IRQ : icu = ");
-                boot_putd(icu_id);
-                boot_puts(" / type = ");
-                boot_putd(type);
-                boot_puts(" / isr = ");
-                boot_putd(isr_id);
-                boot_puts(" / channel = ");
-                boot_putd(channel);
-                boot_puts("\n");
+boot_puts("- IRQ : icu = ");
+boot_putd(icu_id);
+boot_puts(" / type = ");
+boot_putd(type);
+boot_puts(" / isr = ");
+boot_putd(isr_id);
+boot_puts(" / channel = ");
+boot_putd(channel);
+boot_puts(" => vector_entry = ");
+boot_putx( value );
+boot_puts("\n");
 #endif
             }
@@ -1559 +1584 @@
     } // end for clusters
 
+    ///////////////////////////////////////////////////////////////////
     // Step 2 : loop on the vspaces and the tasks 
     //          to initialise the schedulers and the task contexts.
-
-    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) {
+    // Implementation note:
+    // This function initialises the task context for all tasks.
+    // For each processor, the scheduler virtual base address 
+    // is written in the CP0_SCHED register in reset.S 
+
+    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
+    {
 
 #if BOOT_DEBUG_SCHED
-        boot_puts
-            ("\n[BOOT DEBUG] Initialise schedulers / task contexts for vspace ");
-        boot_puts(vspace[vspace_id].name);
-        boot_puts("\n");
+boot_puts("\n[BOOT DEBUG] Initialise task contexts for vspace ");
+boot_puts(vspace[vspace_id].name);
+boot_puts("\n");
 #endif
         // We must set the PTPR depending on the vspace, because the start_vector 
         // and the stack address are defined in virtual space.
-        boot_set_mmu_ptpr((unsigned int) boot_ptabs_paddr[vspace_id] >> 13);
+        boot_set_mmu_ptpr( (unsigned int)(boot_ptabs_paddr[vspace_id] >> 13) );
 
         // loop on the tasks in vspace (task_id is the global index)
         for (task_id = vspace[vspace_id].task_offset;
-                task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks);
-                task_id++) {
+             task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks);
+             task_id++) 
+        {
+            // compute gpid (global processor index) and scheduler base address
+            unsigned int gpid = task[task_id].clusterid * NB_PROCS_MAX + 
+                                task[task_id].proclocid;
+            static_scheduler_t* psched = boot_schedulers[gpid];
+
             // ctx_ra :  the return address is &boot_eret()
             unsigned int ctx_ra = (unsigned int) &boot_eret;
@@ -1585 +1621 @@
 
             // ctx_ptpr : page table physical base address (shifted by 13 bit)
-            unsigned int ctx_ptpr = (unsigned int) boot_ptabs_paddr[vspace_id] >> 13;
-
-            // compute gpid = global processor index
-            unsigned int gpid = task[task_id].clusterid * NB_PROCS_MAX + task[task_id].proclocid;
+            unsigned int ctx_ptpr = (unsigned int)(boot_ptabs_paddr[vspace_id] >> 13);
 
             // ctx_ptab : page_table virtual base address
-            unsigned int ctx_ptab = (unsigned int) boot_ptabs_vaddr[vspace_id];
-
-            // ctx_tty : terminal global index provided by a global allocator
+            unsigned int ctx_ptab = boot_ptabs_vaddr[vspace_id];
+
+            // ctx_tty : terminal global index provided by the global allocator
             unsigned int ctx_tty = 0xFFFFFFFF;
-            if (task[task_id].use_tty) {
-                if (alloc_tty_channel >= NB_TTYS) {
+            if (task[task_id].use_tty) 
+            {
+                if (alloc_tty_channel >= NB_TTY_CHANNELS) 
+                {
                     boot_puts("\n[BOOT ERROR] TTY index too large for task ");
                     boot_puts(task[task_id].name);
@@ -1607 +1642 @@
                 alloc_tty_channel++;
             }
-            // ctx_nic : NIC channel global index provided by a global allocator
+            // ctx_nic : NIC channel global index provided by the global allocator
             unsigned int ctx_nic = 0xFFFFFFFF;
-            if (task[task_id].use_nic) {
-                if (alloc_nic_channel >= NB_NICS) {
+            if (task[task_id].use_nic) 
+            {
+                if (alloc_nic_channel >= NB_NIC_CHANNELS) 
+                {
                     boot_puts("\n[BOOT ERROR] NIC channel index too large for task ");
                     boot_puts(task[task_id].name);
@@ -1621 +1658 @@
                 alloc_nic_channel++;
             }
-            // ctx_timer : user TIMER global index provided by a cluster allocator 
-            unsigned int ctx_timer = 0xFFFFFFFF;
-            if (task[task_id].use_timer) {
+            // ctx_cma : CMA channel global index provided by the global allocator
+            unsigned int ctx_cma = 0xFFFFFFFF;
+            if (task[task_id].use_cma) 
+            {
+                if (alloc_cma_channel >= NB_CMA_CHANNELS) 
+                {
+                    boot_puts("\n[BOOT ERROR] CMA channel index too large for task ");
+                    boot_puts(task[task_id].name);
+                    boot_puts(" in vspace ");
+                    boot_puts(vspace[vspace_id].name);
+                    boot_puts("\n");
+                    boot_exit();
+                }
+                ctx_cma = alloc_cma_channel;
+                alloc_cma_channel++;
+            }
+            // ctx_ioc : IOC channel global index provided by the global allocator
+            unsigned int ctx_ioc = 0xFFFFFFFF;
+            if (task[task_id].use_ioc) 
+            {
+                if (alloc_ioc_channel >= NB_IOC_CHANNELS) 
+                {
+                    boot_puts("\n[BOOT ERROR] IOC channel index too large for task ");
+                    boot_puts(task[task_id].name);
+                    boot_puts(" in vspace ");
+                    boot_puts(vspace[vspace_id].name);
+                    boot_puts("\n");
+                    boot_exit();
+                }
+                ctx_ioc = alloc_ioc_channel;
+                alloc_ioc_channel++;
+            }
+            // ctx_tim : TIMER local channel index provided by the cluster allocator 
+            unsigned int ctx_tim = 0xFFFFFFFF;
+            if (task[task_id].use_tim) 
+            {
                 unsigned int cluster_id = task[task_id].clusterid;
-                unsigned int allocated = alloc_timer_channel[cluster_id];
-
-                if (allocated >= NB_TIMERS_MAX) {
+
+                if ( alloc_tim_channel[cluster_id] >= NB_TIM_CHANNELS ) 
+                {
                     boot_puts("\n[BOOT ERROR] local TIMER index too large for task ");
                     boot_puts(task[task_id].name);
@@ -1635 +1705 @@
                     boot_exit();
                 }
-                //assert(allocated >= 0);
-                char found = 0;
-                for (irq_id = 0; irq_id < 32; irq_id++) { //look at the isr_timer isr channel
-                    unsigned int isr = boot_scheduler_get_itvector(gpid, irq_id) & 0x000000FF;
-                    if (isr == ISR_TIMER) {
-                        if (allocated == 0) {
-                            found = 1;
-                            alloc_timer_channel[cluster_id]++;
-                            ctx_timer = cluster_id * NB_TIMERS_MAX + alloc_timer_channel[cluster_id];
-                            break;
-                        }
-                        else {
-                            allocated--;
-                        }
+
+                // checking that there is a well defined ISR_TIMER installed
+                unsigned int found = 0;
+                for ( irq_id = 0 ; irq_id < 32 ; irq_id++ )  
+                {
+                    unsigned int entry   = psched->interrupt_vector[irq_id];
+                    unsigned int isr     = entry & 0x000000FF;
+                    unsigned int channel = entry>>16;
+                    if ( (isr == ISR_TIMER) && (channel == alloc_tim_channel[cluster_id]) ) 
+                    {
+                        found     = 1;
+                        ctx_tim =  alloc_tim_channel[cluster_id];
+                        alloc_tim_channel[cluster_id]++;
+                        break;
                     }
                 }
-
-                if (!found) {
-                    boot_puts("\n[BOOT ERROR] No user timer available for task ");
+                if (!found) 
+                {
+                    boot_puts("\n[BOOT ERROR] No ISR_TIMER installed for task ");
                     boot_puts(task[task_id].name);
                     boot_puts(" in vspace ");
@@ -1660 +1730 @@
                     boot_exit();
                 }
-
             }
-            // ctx_dma : DMA global index provided by a cluster allocator  
+            // ctx_dma : the local channel index is defined by the cluster allocator  
+            //           but the ctx_dma value is a global index
             unsigned int ctx_dma = 0xFFFFFFFF;
-            if (task[task_id].use_fbdma || task[task_id].use_nic) {
+            if ( task[task_id].use_dma ) 
+            {
                 unsigned int cluster_id = task[task_id].clusterid;
-                if (alloc_dma_channel[cluster_id] >= NB_DMAS_MAX) {
+
+                if (alloc_dma_channel[cluster_id] >= NB_DMA_CHANNELS) 
+                {
                     boot_puts("\n[BOOT ERROR] local DMA index too large for task ");
                     boot_puts(task[task_id].name);
@@ -1674 +1747 @@
                     boot_exit();
                 }
-                ctx_dma = cluster_id * NB_DMAS_MAX + alloc_dma_channel[cluster_id];
+                ctx_dma = cluster_id * NB_DMA_CHANNELS + alloc_dma_channel[cluster_id];
                 alloc_dma_channel[cluster_id]++;
             }
             // ctx_epc : Get the virtual address of the start function
-            mapping_vobj_t * pvobj = &vobj[vspace[vspace_id].vobj_offset + vspace[vspace_id].start_offset];
-            unsigned int * start_vector_vbase = (unsigned int *) pvobj->vaddr;
+            mapping_vobj_t* pvobj = &vobj[vspace[vspace_id].vobj_offset + 
+                                     vspace[vspace_id].start_offset];
+            unsigned int* start_vector_vbase = (unsigned int *) pvobj->vaddr;
             unsigned int ctx_epc = start_vector_vbase[task[task_id].startid];
 
@@ -1686 +1760 @@
             unsigned int ctx_sp = vobj[vobj_id].vaddr + vobj[vobj_id].length;
 
-            // In the code below, we access the scheduler with specific access 
-            // functions, because we only have the physical address of the scheduler, 
-            // and these functions must temporary desactivate the DTLB...
-
-            // get local task index in scheduler[gpid]
-            unsigned int ltid = boot_scheduler_get_tasks(gpid);
-
-            if (ltid >= IDLE_TASK_INDEX) {
+            // get local task index in scheduler
+            unsigned int ltid = psched->tasks;
+
+            if (ltid >= IDLE_TASK_INDEX) 
+            {
                 boot_puts("\n[BOOT ERROR] : ");
                 boot_putd(ltid);
@@ -1701 +1772 @@
                 boot_exit();
             }
-            // update the "tasks" field in scheduler[gpid]
-            boot_scheduler_set_tasks(gpid, ltid + 1);
-
-            // update the "current" field in scheduler[gpid]
-            boot_scheduler_set_current(gpid, 0);
-
-            // initializes the task context in scheduler[gpid]
-            boot_scheduler_set_context(gpid, ltid, CTX_SR_ID, ctx_sr);
-            boot_scheduler_set_context(gpid, ltid, CTX_SP_ID, ctx_sp);
-            boot_scheduler_set_context(gpid, ltid, CTX_RA_ID, ctx_ra);
-            boot_scheduler_set_context(gpid, ltid, CTX_EPC_ID, ctx_epc);
-            boot_scheduler_set_context(gpid, ltid, CTX_PTPR_ID, ctx_ptpr);
-            boot_scheduler_set_context(gpid, ltid, CTX_TTY_ID, ctx_tty);
-            boot_scheduler_set_context(gpid, ltid, CTX_DMA_ID, ctx_dma);
-            boot_scheduler_set_context(gpid, ltid, CTX_NIC_ID, ctx_nic);
-            boot_scheduler_set_context(gpid, ltid, CTX_TIMER_ID, ctx_timer);
-            boot_scheduler_set_context(gpid, ltid, CTX_PTAB_ID, ctx_ptab);
-            boot_scheduler_set_context(gpid, ltid, CTX_LTID_ID, ltid);
-            boot_scheduler_set_context(gpid, ltid, CTX_VSID_ID, vspace_id);
-            boot_scheduler_set_context(gpid, ltid, CTX_GTID_ID, task_id);
-            boot_scheduler_set_context(gpid, ltid, CTX_RUN_ID, 1);
+            // update the "tasks" field in scheduler
+            psched->tasks = ltid + 1;
+
+            // update the "current" field in scheduler
+            psched->current = 0;
+
+            // initializes the task context in scheduler
+            psched->context[ltid][CTX_SR_ID]    = ctx_sr;
+            psched->context[ltid][CTX_SP_ID]    = ctx_sp;
+            psched->context[ltid][CTX_RA_ID]    = ctx_ra;
+            psched->context[ltid][CTX_EPC_ID]   = ctx_epc;
+            psched->context[ltid][CTX_PTPR_ID]  = ctx_ptpr;
+            psched->context[ltid][CTX_TTY_ID]   = ctx_tty;
+            psched->context[ltid][CTX_CMA_ID]   = ctx_cma;
+            psched->context[ltid][CTX_IOC_ID]   = ctx_ioc;
+            psched->context[ltid][CTX_NIC_ID]   = ctx_nic;
+            psched->context[ltid][CTX_TIM_ID]   = ctx_tim;
+            psched->context[ltid][CTX_DMA_ID]   = ctx_dma;
+            psched->context[ltid][CTX_PTAB_ID]  = ctx_ptab;
+            psched->context[ltid][CTX_LTID_ID]  = ltid;
+            psched->context[ltid][CTX_GTID_ID]  = task_id;
+            psched->context[ltid][CTX_VSID_ID]  = vspace_id;
+            psched->context[ltid][CTX_RUN_ID]   = 1;
 
 #if BOOT_DEBUG_SCHED
-            boot_puts("\nTask ");
-            boot_puts(task[task_id].name);
-            boot_puts(" (");
-            boot_putd(task_id);
-            boot_puts(") allocated to processor ");
-            boot_putd(gpid);
-            boot_puts("\n  - ctx[LTID]   = ");
-            boot_putd(ltid);
-            boot_puts("\n  - ctx[SR]     = ");
-            boot_putx(ctx_sr);
-            boot_puts("\n  - ctx[SR]     = ");
-            boot_putx(ctx_sp);
-            boot_puts("\n  - ctx[RA]     = ");
-            boot_putx(ctx_ra);
-            boot_puts("\n  - ctx[EPC]    = ");
-            boot_putx(ctx_epc);
-            boot_puts("\n  - ctx[PTPR]   = ");
-            boot_putx(ctx_ptpr);
-            boot_puts("\n  - ctx[TTY]    = ");
-            boot_putd(ctx_tty);
-            boot_puts("\n  - ctx[NIC]    = ");
-            boot_putd(ctx_nic);
-            boot_puts("\n  - ctx[TIMER]  = ");
-            boot_putd(ctx_timer);
-            boot_puts("\n  - ctx[DMA]    = ");
-            boot_putd(ctx_dma);
-            boot_puts("\n  - ctx[PTAB]   = ");
-            boot_putx(ctx_ptab);
-            boot_puts("\n  - ctx[VSID]   = ");
-            boot_putd(vspace_id);
-            boot_puts("\n");
+boot_puts("\nTask ");
+boot_puts(task[task_id].name);
+boot_puts(" (");
+boot_putd(task_id);
+boot_puts(") allocated to processor ");
+boot_putd(gpid);
+boot_puts("\n  - ctx[LTID]   = ");
+boot_putd(ltid);
+boot_puts("\n  - ctx[SR]     = ");
+boot_putx(ctx_sr);
+boot_puts("\n  - ctx[SR]     = ");
+boot_putx(ctx_sp);
+boot_puts("\n  - ctx[RA]     = ");
+boot_putx(ctx_ra);
+boot_puts("\n  - ctx[EPC]    = ");
+boot_putx(ctx_epc);
+boot_puts("\n  - ctx[PTPR]   = ");
+boot_putx(ctx_ptpr);
+boot_puts("\n  - ctx[TTY]    = ");
+boot_putd(ctx_tty);
+boot_puts("\n  - ctx[NIC]    = ");
+boot_putd(ctx_nic);
+boot_puts("\n  - ctx[CMA]    = ");
+boot_putd(ctx_cma);
+boot_puts("\n  - ctx[IOC]    = ");
+boot_putd(ctx_ioc);
+boot_puts("\n  - ctx[TIM]    = ");
+boot_putd(ctx_tim);
+boot_puts("\n  - ctx[DMA]    = ");
+boot_putd(ctx_dma);
+boot_puts("\n  - ctx[PTAB]   = ");
+boot_putx(ctx_ptab);
+boot_puts("\n  - ctx[GTID]   = ");
+boot_putd(task_id);
+boot_puts("\n  - ctx[VSID]   = ");
+boot_putd(vspace_id);
+boot_puts("\n");
 #endif
 
@@ -1765 +1844 @@
 // This function is executed by P[0] to wakeup all processors.
 //////////////////////////////////////////////////////////////////////////////////
-void boot_start_all_procs() {
+void boot_start_all_procs() 
+{
     mapping_header_t * header = (mapping_header_t *) &seg_mapping_base;
     header->signature = OUT_MAPPING_SIGNATURE;
@@ -1786 +1866 @@
     boot_psegs_init();
 
-    boot_puts
-        ("\n[BOOT] Pseg allocators initialisation completed at cycle ");
+    boot_puts("\n[BOOT] Pseg allocators initialisation completed at cycle ");
     boot_putd(boot_proctime());
     boot_puts("\n");
@@ -1798 +1877 @@
     boot_puts("\n");
 
+    // mmu activation ( with page table [Ø] )
+    boot_set_mmu_ptpr( (unsigned int)(boot_ptabs_paddr[0] >> 13) );
+    boot_set_mmu_mode(0xF);
+
+    boot_puts("\n[BOOT] Proc 0 MMU activation at cycle ");
+    boot_putd(boot_proctime());
+    boot_puts("\n");
+
     // vobjs initialisation
     boot_vobjs_init();
@@ -1809 +1896 @@
 
     boot_puts("\n[BOOT] Peripherals initialisation completed at cycle ");
-    boot_putd(boot_proctime());
-    boot_puts("\n");
-
-    // mmu activation
-    boot_set_mmu_ptpr((unsigned int) boot_ptabs_paddr[0] >> 13);
-    boot_set_mmu_mode(0xF);
-
-    boot_puts("\n[BOOT] MMU activation completed at cycle ");
     boot_putd(boot_proctime());
     boot_puts("\n");

soft/giet_vm/boot/reset.S

@@ -182 +182 @@
 boot_to_kernel_init:
 
-    # all processors initialise SCHED register with boot_schedulers_paddr[pid] 
+    # all processors initialise the CP0 SCHED register
+    # SCHED contains the schedulers array virtual base address
     mfc0        k0, CP0_PROCID
     andi    k0, k0, 0xFFF
     sll         k0, k0, 2               # k0 <= 4*pid 
-    la          k1, boot_schedulers_paddr
-    addu    k1, k1, k0          # k1 <= &boot_scheduler_paddr[pid] 
-    lw          k1,     0(k1)           
-    mtc0        k1, CP0_SCHED
-
-    # all processors initialize PTPR register with boot_ptabs_paddr[0] 
+    la          k1, boot_schedulers
+    addu    k1, k1, k0          # k1 <= &boot_schedulers[pid] 
+    lw          k0,     0(k1)           
+    mtc0        k0, CP0_SCHED
+
+    # all processors initialize the CP2 PTPR register
+    # At this stage, all PTPR registers contain the physical base
+    # address (13 bits right shifted) of the page table for vspace[0] 
     la      k1, boot_ptabs_paddr
-    lw      k1, 0(k1)   
-    srl     k1, k1, 13
-    mtc2        k1,     CP2_PTPR        
-
-        # all processors activate MMU 
+    lw      k0, 0(k1)           # k0 <= paddr_lsb
+    lw      k1, 4(k1)           # k1 <= paddr_msb
+    srl     k0, k0, 13          # k0 <= paddr_lsb shifted
+    sll     k1, k1, 19          # k1 <= paddr_msb shifted
+    or      k0, k0, k1
+    mtc2        k0,     CP2_PTPR        
+
+        # all processors activate MMU (already done for processor 0)
     li      k1, 0xF
     mtc2    k1, CP2_MODE