Index: soft/giet_vm/boot/boot_handler.c
===================================================================
--- soft/giet_vm/boot/boot_handler.c	(revision 163)
+++ soft/giet_vm/boot/boot_handler.c	(revision 165)
@@ -6,9 +6,8 @@
 ///////////////////////////////////////////////////////////////////////////////////
 // The boot_handler.h and boot_handler.c files are part of the GIET nano-kernel.
-// This code can be used in the boot phase to build all the pages tables then jumps
-// in to the seg_kernel_init segment with an activated MMU. 
+// This code is executed in the boot phase by proc0 to build  all the pages tables,
+// then jump in the seg_kernel_init segment with an activated MMU. 
 //
-// It uses the SoCLib generic MMU (paged virtual memory) to provide two services:
-//
+// The SoCLib generic MMU (paged virtual memory) provides two services:
 // 1) classical memory protection, when several independant applications compiled
 //    in different virtual spaces are executing on the same hardware platform.
@@ -16,6 +15,6 @@
 //    of the software objects (virtual segments) on the physical memory banks.
 //
-// It uses the MAPPING_INFO binary data structures, that must be pre-loaded in the 
-// boot ROM in the seg_boot_mapping segment (at address seg_mapping_base).
+// The boot code uses the MAPPING_INFO binary data structures, that must be pre-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:
@@ -32,6 +31,6 @@
 // As most applications use only a limited number of segments, the number of PT2s 
 // actually used by a given virtual space is generally smaller than 2048, and is
-// defined in the MAPPING_INFO_BINARY data structure(using the length field). 
-// The value is calculated and put in _max_pte2 indexed by the vspace_id.
+// defined in the MAPPING_INFO_BINARY data structure (using the length field). 
+// The value is calculated and put in _max_pt2 indexed by the vspace_id.
 // The physical alignment constraints, is ensured by the align flag in the MAPPING_INFO 
 // structure.
@@ -41,16 +40,16 @@
 // - a first 8K aligned PT1[2148] array, indexed by the (ix1) field of VPN. 
 //   The PT1 contains 2048 PTD of 4 bytes => 8K bytes.
-// - an aray of array PT2[1024][_max_pte2[vspace_id]], indexed by
+// - an aray of array PT2[1024][_max_pt2[vspace_id]], indexed by
 //   the (ix2) field of the VPN, and by the PT2 index (pt2_id).
-//   Each PT2 contains 512 PTE2 of 8bytes => 4Kbytes * _max_pte2[vspace_id]
-// The size of each page table is 8K + (_max_pte2[vspace_id])*4K bytes.
+//   Each PT2 contains 512 PTE2 of 8bytes => 4Kbytes * _max_pt2[vspace_id]
+// The size of each page table is 8K + (_max_pt2[vspace_id])*4K bytes.
 // All page tables must be stored in the seg_kernel_pt segment (at address
 // seg_kernel_pt_base) 
 ////////////////////////////////////////////////////////////////////////////////////
 
-#include <mips32_registers.h>
+#include "../sys/mips32_registers.h"
 #include <boot_handler.h>
 #include <mapping_info.h>
-#include <mwmr.h>
+#include <mwmr_channel.h>
 
 #include <stdarg.h>
@@ -62,17 +61,16 @@
 
 ////////////////////////////////////////////////////////////////////////////
-//  Global variables
+//  Page Tables global variables
 ////////////////////////////////////////////////////////////////////////////
 
-// Page Tables 
-// Next free PT2 index 
+// Next free PT2 index array
 unsigned int  _next_free_pt2[GIET_NB_VSPACE_MAX] =
                          { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };
 
-// Max PT2 index 
-unsigned int  _max_pte2[GIET_NB_VSPACE_MAX] =
+// Max number of PT2 array
+unsigned int  _max_pt2[GIET_NB_VSPACE_MAX] =
                          { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };
 
-// Page table pointers
+// Page table pointers array
 page_table_t* _ptabs[GIET_NB_VSPACE_MAX];
 
@@ -107,8 +105,8 @@
 
 ////////////////////////////////////////////////////////////////////////////
-// boot_tty_puts()
+// boot_puts()
 // (it uses TTY0)
 ////////////////////////////////////////////////////////////////////////////
-void boot_tty_puts(const char *buffer) 
+void boot_puts(const char *buffer) 
 {
     unsigned int* tty_address = (unsigned int*)&seg_tty_base;
@@ -124,8 +122,8 @@
 
 ////////////////////////////////////////////////////////////////////////////
-// boot_tty_putw() 
+// boot_putw() 
 // (it uses TTY0)
 ////////////////////////////////////////////////////////////////////////////
-void boot_tty_putw(unsigned int val)
+void boot_putw(unsigned int val)
 {
     static const char   HexaTab[] = "0123456789ABCDEF";
@@ -142,5 +140,5 @@
         val = val >> 4;
     }
-    boot_tty_puts(buf);
+    boot_puts(buf);
 }
 
@@ -219,42 +217,42 @@
     mapping_vseg_t*	    vseg    = boot_get_vseg_base ( header );
     mapping_task_t*	    task    = boot_get_task_base ( header );;
-    mapping_vobj_t*    vobj   = boot_get_vobj_base( header );
+    mapping_vobj_t*     vobj    = boot_get_vobj_base( header );
 
     // header
-    boot_tty_puts("mapping_info");
-
-    boot_tty_puts("\n - signature = ");
-    boot_tty_putw(header->signature);
-    boot_tty_puts("\n - name      = ");
-    boot_tty_puts(header->name);
-    boot_tty_puts("\n - clusters  = ");
-    boot_tty_putw(header->clusters);
-    boot_tty_puts("\n - psegs     = ");
-    boot_tty_putw(header->psegs);
-    boot_tty_puts("\n - ttys      = ");
-    boot_tty_putw(header->ttys);
-    boot_tty_puts("\n - vspaces   = ");
-    boot_tty_putw(header->vspaces);
-    boot_tty_puts("\n - globals   = ");
-    boot_tty_putw(header->globals);
-    boot_tty_puts("\n - vsegs     = ");
-    boot_tty_putw(header->vsegs);
-    boot_tty_puts("\n - tasks     = ");
-    boot_tty_putw(header->tasks);
-    boot_tty_puts("\n\n");
+    boot_puts("mapping_info");
+
+    boot_puts("\n - signature = ");
+    boot_putw(header->signature);
+    boot_puts("\n - name      = ");
+    boot_puts(header->name);
+    boot_puts("\n - clusters  = ");
+    boot_putw(header->clusters);
+    boot_puts("\n - psegs     = ");
+    boot_putw(header->psegs);
+    boot_puts("\n - ttys      = ");
+    boot_putw(header->ttys);
+    boot_puts("\n - fbs       = ");
+    boot_putw(header->fbs);
+    boot_puts("\n - vspaces   = ");
+    boot_putw(header->vspaces);
+    boot_puts("\n - globals   = ");
+    boot_putw(header->globals);
+    boot_puts("\n - vsegs     = ");
+    boot_putw(header->vsegs);
+    boot_puts("\n - vobjs     = ");
+    boot_putw(header->vobjs);
+    boot_puts("\n - tasks     = ");
+    boot_putw(header->tasks);
+    boot_puts("\n\n");
 
     // clusters
     for ( cluster_id = 0 ; cluster_id < header->clusters ; cluster_id++ )
     {
-        boot_tty_puts("cluster ");
-        boot_tty_putw(cluster_id);
-
-        boot_tty_puts("\n - procs  = ");
-        boot_tty_putw(cluster[cluster_id].procs);
-        boot_tty_puts("\n - timers = ");
-        boot_tty_putw(cluster[cluster_id].timers);
-        boot_tty_puts("\n - dmas   = ");
-        boot_tty_putw(cluster[cluster_id].dmas);
-        boot_tty_puts("\n\n");
+        boot_puts("cluster ");
+        boot_putw(cluster_id);
+
+        boot_puts("\n - procs  = ");
+        boot_putw(cluster[cluster_id].procs);
+        boot_puts("\n\n");
     }
 
@@ -262,14 +260,14 @@
     for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
     {
-        boot_tty_puts("pseg ");
-        boot_tty_putw(pseg_id);
-
-        boot_tty_puts("\n - name   = ");
-        boot_tty_puts( pseg[pseg_id].name );
-        boot_tty_puts("\n - base   = ");
-        boot_tty_putw( pseg[pseg_id].base );
-        boot_tty_puts("\n - length = ");
-        boot_tty_putw( pseg[pseg_id].length );
-        boot_tty_puts("\n\n");
+        boot_puts("pseg ");
+        boot_putw(pseg_id);
+
+        boot_puts("\n - name   = ");
+        boot_puts( pseg[pseg_id].name );
+        boot_puts("\n - base   = ");
+        boot_putw( pseg[pseg_id].base );
+        boot_puts("\n - length = ");
+        boot_putw( pseg[pseg_id].length );
+        boot_puts("\n\n");
     }
 
@@ -277,40 +275,39 @@
     for ( vseg_id = 0 ; vseg_id < header->globals ; vseg_id++ )
     {
-        boot_tty_puts("global vseg ");
-        boot_tty_putw(vseg_id);
-
-        boot_tty_puts("\n - name   = ");
-        boot_tty_puts( vseg[vseg_id].name );
-        boot_tty_puts("\n - vbase  = ");
-        boot_tty_putw( vseg[vseg_id].vbase );
-        boot_tty_puts("\n - length = ");
-        boot_tty_putw( vseg[vseg_id].length );
-        boot_tty_puts("\n - mode   = ");
-        boot_tty_putw( vseg[vseg_id].mode );
-        boot_tty_puts("\n - ident = ");
-        boot_tty_putw( vseg[vseg_id].ident );
-        boot_tty_puts("\n - psegname = ");
-        boot_tty_puts( pseg[vseg[vseg_id].psegid].name );
-        boot_tty_puts("\n");
-        for ( vobj_id = vseg[vseg_id].vobj_offset ; vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; vobj_id++ )
-        {
-			boot_tty_puts("vobjs: \n");
-            boot_tty_putw( vobj[vobj_id].name);
-            boot_tty_puts("\n");
-            boot_tty_puts("\t name     = ");
-			boot_tty_putw(  vobj[vobj_id].name);
-			boot_tty_puts("\n");
-            boot_tty_puts("\t type     = ");
-			boot_tty_putw( vobj[vobj_id].type);
-			boot_tty_puts("\n");
-            boot_tty_puts("\t length   = ");
-			boot_tty_putw(   vobj[vobj_id].length);
-			boot_tty_puts("\n");
-            boot_tty_puts("\t align    = ");
-			boot_tty_putw(   vobj[vobj_id].align);
-			boot_tty_puts("\n");
-            boot_tty_puts("\t binpath  = ");
-			boot_tty_putw(   vobj[vobj_id].binpath);
-			boot_tty_puts("\n\n");
+        boot_puts("global vseg ");
+        boot_putw(vseg_id);
+
+        boot_puts("\n - name        = ");
+        boot_puts( vseg[vseg_id].name );
+        boot_puts("\n - vbase       = ");
+        boot_putw( vseg[vseg_id].vbase );
+        boot_puts("\n - length      = ");
+        boot_putw( vseg[vseg_id].length );
+        boot_puts("\n - mode        = ");
+        boot_putw( vseg[vseg_id].mode );
+        boot_puts("\n - ident       = ");
+        boot_putw( vseg[vseg_id].ident );
+        boot_puts("\n - psegname    = ");
+        boot_puts( pseg[vseg[vseg_id].psegid].name );
+        boot_puts("\n - vobjs       = ");
+        boot_putw( vseg[vseg_id].vobjs );
+        boot_puts("\n - vobj_offset = ");
+        boot_putw( vseg[vseg_id].vobj_offset );
+        boot_puts("\n");
+        for ( vobj_id = vseg[vseg_id].vobj_offset ; 
+              vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; 
+              vobj_id++ )
+        {
+			boot_puts("\n\t vobj ");
+            boot_puts( vobj[vobj_id].name);
+            boot_puts("\n\t type     = ");
+			boot_putw( vobj[vobj_id].type);
+            boot_puts("\n\t length   = ");
+			boot_putw(   vobj[vobj_id].length);
+            boot_puts("\n\t align    = ");
+			boot_putw(   vobj[vobj_id].align);
+            boot_puts("\n\t binpath  = ");
+			boot_puts(   vobj[vobj_id].binpath);
+			boot_puts("\n\n");
         }
     }
@@ -319,16 +316,27 @@
     for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
     {
-        unsigned int func_id = vspace[vspace_id].vobj_offset + vspace[vspace_id].funcs_offset; 
-        boot_tty_puts("vspace ");
-        boot_tty_putw(vspace_id);
-
-        boot_tty_puts("\n - name    = ");
-        boot_tty_puts( vspace[vspace_id].name ); 
-        boot_tty_puts("\n - funcs    = ");
-        boot_tty_puts( vobj[func_id].name ); 
-        boot_tty_puts( vspace[vspace_id].name ); 
-        boot_tty_puts("\n - ttys    = ");
-        boot_tty_putw( vspace[vspace_id].ttys );
-        boot_tty_puts("\n\n");
+        unsigned int start_id = vspace[vspace_id].vobj_offset + 
+                                vspace[vspace_id].start_offset; 
+
+        boot_puts("vspace ");
+        boot_putw(vspace_id);
+
+        boot_puts("\n - name        = ");
+        boot_puts( vspace[vspace_id].name ); 
+        boot_puts("\n - start_vobj  = ");
+        boot_puts( vobj[start_id].name ); 
+        boot_puts("\n - vsegs       = ");
+        boot_putw( vspace[vspace_id].vsegs ); 
+        boot_puts("\n - vobjs       = ");
+        boot_putw( vspace[vspace_id].vobjs ); 
+        boot_puts("\n - tasks       = ");
+        boot_putw( vspace[vspace_id].tasks ); 
+        boot_puts("\n - vseg_offset = ");
+        boot_putw( vspace[vspace_id].vseg_offset ); 
+        boot_puts("\n - vobj_offset = ");
+        boot_putw( vspace[vspace_id].vobj_offset ); 
+        boot_puts("\n - task_offset = ");
+        boot_putw( vspace[vspace_id].task_offset ); 
+        boot_puts("\n\n");
 
         for ( vseg_id = vspace[vspace_id].vseg_offset ; 
@@ -336,40 +344,40 @@
               vseg_id++ )
         {
-            boot_tty_puts("    private vseg ");
-            boot_tty_putw( vseg_id );
-
-            boot_tty_puts("\n    - name   = ");
-            boot_tty_puts( vseg[vseg_id].name );
-            boot_tty_puts("\n    - vbase  = ");
-            boot_tty_putw( vseg[vseg_id].vbase );
-            boot_tty_puts("\n    - length = ");
-            boot_tty_putw( vseg[vseg_id].length );
-            boot_tty_puts("\n    - mode   = ");
-            boot_tty_putw( vseg[vseg_id].mode );
-            boot_tty_puts("\n    - ident = ");
-            boot_tty_putw( vseg[vseg_id].ident );
-            boot_tty_puts("\n    - psegname = ");
-            boot_tty_puts( pseg[vseg[vseg_id].psegid].name );
-            boot_tty_puts("\n");
-            for ( vobj_id = vseg[vseg_id].vobj_offset ; vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; vobj_id++ )
+            boot_puts("    private vseg ");
+            boot_putw( vseg_id );
+
+            boot_puts("\n    - name        = ");
+            boot_puts( vseg[vseg_id].name );
+            boot_puts("\n    - vbase       = ");
+            boot_putw( vseg[vseg_id].vbase );
+            boot_puts("\n    - length      = ");
+            boot_putw( vseg[vseg_id].length );
+            boot_puts("\n    - mode        = ");
+            boot_putw( vseg[vseg_id].mode );
+            boot_puts("\n    - ident       = ");
+            boot_putw( vseg[vseg_id].ident );
+            boot_puts("\n    - psegname    = ");
+            boot_puts( pseg[vseg[vseg_id].psegid].name );
+            boot_puts("\n    - vobjs       = ");
+            boot_putw( vseg[vseg_id].vobjs );
+            boot_puts("\n    - vobj_offset = ");
+            boot_putw( vseg[vseg_id].vobj_offset );
+            boot_puts("\n");
+
+            for ( vobj_id = vseg[vseg_id].vobj_offset ; 
+                  vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; 
+                  vobj_id++ )
             {
-                boot_tty_puts("\t\t vobjs     = ");
-				boot_tty_putw(     vobj[vobj_id].name);
-				boot_tty_puts("\n");
-                boot_tty_puts("\t\t name     = ");
-				boot_tty_putw(     vobj[vobj_id].name);
-				boot_tty_puts("\n");
-                boot_tty_puts("\t\t type     = ");
-				boot_tty_putw( vobj[vobj_id].type);
-				boot_tty_puts("\n");
-                boot_tty_puts("\t\t length   = ");
-				boot_tty_putw(   vobj[vobj_id].length);
-				boot_tty_puts("\n");
-                boot_tty_puts("\t\t align    = ");
-				boot_tty_putw(   vobj[vobj_id].align);
-				boot_tty_puts("\n");
-                boot_tty_puts("\t\t binpath  = ");
-				boot_tty_putw(   vobj[vobj_id].binpath);
-				boot_tty_puts("\n");
+                boot_puts("\n\t\t vobj ");
+                boot_puts( vobj[vobj_id].name);
+                boot_puts("\n\t\t type     = ");
+                boot_putw( vobj[vobj_id].type);
+                boot_puts("\n\t\t length   = ");
+			    boot_putw(   vobj[vobj_id].length);
+                boot_puts("\n\t\t align    = ");
+			    boot_putw(   vobj[vobj_id].align);
+                boot_puts("\n\t\t binpath  = ");
+	    		boot_puts(   vobj[vobj_id].binpath);
+    			boot_puts("\n\n");
             }
         }
@@ -379,20 +387,22 @@
               task_id++ )
         {
-            boot_tty_puts("     task");
-            boot_tty_putw( task_id );
-
-            boot_tty_puts("\n     - name = ");
-            boot_tty_puts( task[task_id].name );
-            boot_tty_puts("\n     - clusterid = ");
-            boot_tty_putw( task[task_id].clusterid );
-            boot_tty_puts("\n     - proclocid = ");
-            boot_tty_putw( task[task_id].proclocid );
-            boot_tty_puts("\n     - vobjlocid = ");
-            boot_tty_putw( task[task_id].vobjlocid );
-            boot_tty_puts("\n     - startid   = ");
-            boot_tty_putw( task[task_id].startid );
-            boot_tty_puts("\n     - ttylocid  = ");
-            boot_tty_putw( task[task_id].ttylocid );
-            boot_tty_puts("\n\n");
+            boot_puts("     task");
+            boot_putw( task_id );
+
+            boot_puts("\n     - name = ");
+            boot_puts( task[task_id].name );
+            boot_puts("\n     - clusterid = ");
+            boot_putw( task[task_id].clusterid );
+            boot_puts("\n     - proclocid = ");
+            boot_putw( task[task_id].proclocid );
+            boot_puts("\n     - vobjlocid = ");
+            boot_putw( task[task_id].vobjlocid );
+            boot_puts("\n     - startid   = ");
+            boot_putw( task[task_id].startid );
+            boot_puts("\n     - use_tty   = ");
+            boot_putw( task[task_id].use_tty );
+            boot_puts("\n     - use_fb   = ");
+            boot_putw( task[task_id].use_fb );
+            boot_puts("\n\n");
         }
     }
@@ -403,5 +413,5 @@
 // boot_pseg_get() 
 // This function returns the pointer on a physical segment
-// identified  by the segment index.
+// identified  by the pseg index.
 //////////////////////////////////////////////////////////////////////////////
 mapping_pseg_t*	boot_pseg_get( unsigned int seg_id)
@@ -413,6 +423,6 @@
     if ( seg_id >= header->psegs )
     {
-        boot_tty_puts("\n[BOOT ERROR] : seg_id argument too large\n");
-        boot_tty_puts("               in function boot_pseg_get()\n");
+        boot_puts("\n[BOOT ERROR] : seg_id argument too large\n");
+        boot_puts("               in function boot_pseg_get()\n");
         boot_exit();
     }
@@ -420,5 +430,4 @@
     return &pseg[seg_id];                                    
 } // end boot_pseg_get()
-
 
 //////////////////////////////////////////////////////////////////////////////
@@ -450,10 +459,10 @@
 
         
-    unsigned int max_pte2   = _max_pte2[vspace_id];
-    if(max_pte2 == 0)
-    {
-        boot_tty_puts("Unfound page table for vspace ");
-        boot_tty_putw(vspace_id);
-        boot_tty_puts("\n");
+    unsigned int max_pt2   = _max_pt2[vspace_id];
+    if(max_pt2 == 0)
+    {
+        boot_puts("Unfound page table for vspace ");
+        boot_putw(vspace_id);
+        boot_puts("\n");
         boot_exit();
     }
@@ -463,8 +472,8 @@
     {
         pt2_id = _next_free_pt2[vspace_id];
-        if ( pt2_id == max_pte2 )
-        {
-            boot_tty_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
-            boot_tty_puts("the length of the ptab vobj is too small\n"); 
+        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();
         }
@@ -487,22 +496,7 @@
     if ( ( *pt_flags & PTE_V) != 0 )    // page already mapped
     {
-        if(global)
-        {
-            boot_tty_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
-            boot_tty_puts("page already mapped\n");
-            boot_exit();
-        }else
-        {
-            /**
-             * The case where a global vseg is already mapped as private vseg of a
-             * vspace_id. Typically used when a vseg is being replicated.
-             */  
-            boot_tty_puts("\n[BOOT] global PTE for vspace ");
-            boot_tty_putw(vspace_id);
-            boot_tty_puts(" already mapped, vpn = ");
-            boot_tty_putw(vpn);
-            boot_tty_puts("\n");
-            return;
-        }
+        boot_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
+        boot_puts("page already mapped\n");
+        boot_exit();
     }
 
@@ -549,9 +543,11 @@
 
 #if BOOT_DEBUG_PT
-boot_tty_puts("- vseg ");
-boot_tty_puts( vseg[vseg_id].name );
-boot_tty_puts(" / flags = ");
-boot_tty_putw( flags );
-boot_tty_puts("\n");
+boot_puts("- vseg ");
+boot_puts( vseg[vseg_id].name );
+boot_puts(" / flags = ");
+boot_putw( flags );
+boot_puts(" / npages = ");
+boot_putw( npages );
+boot_puts("\n");
 #endif        
         // loop on 4K pages
@@ -583,11 +579,11 @@
 
 #if BOOT_DEBUG_PT
-boot_tty_puts("- vseg ");
-boot_tty_puts( vseg[vseg_id].name );
-boot_tty_puts(" / flags = ");
-boot_tty_putw( flags );
-boot_tty_puts(" / npages = ");
-boot_tty_putw( npages );
-boot_tty_puts("\n");
+boot_puts("- vseg ");
+boot_puts( vseg[vseg_id].name );
+boot_puts(" / flags = ");
+boot_putw( flags );
+boot_puts(" / npages = ");
+boot_putw( npages );
+boot_puts("\n");
 #endif        
         // loop on 4K pages
@@ -606,50 +602,13 @@
 } // end boot_vspace_pt_build()
 
-
 ///////////////////////////////////////////////////////////////////////////
 // Align the value "toAlign" to the required alignement indicated by
 // alignPow2 ( the logarithme of 2 the alignement).
 ///////////////////////////////////////////////////////////////////////////
-unsigned int align_to( unsigned toAlign, unsigned alignPow2)
-{
-    unsigned mask = (1 << alignPow2) - 1;
-    return ((toAlign + mask ) & ~mask );//page aligned 
-}
-
-///////////////////////////////////////////////////////////////////////////
-// Initialise vobjs
-// For now only one type is initialised the: PTAB
-//
-// param:
-//  vobj: the vobj to initialise
-//  region_id: the vspace in wich the vobj is located or the global space(-1).
-///////////////////////////////////////////////////////////////////////////
-void initailise_vobj(mapping_vobj_t* vobj, unsigned int region_id)
-{
-    if(vobj->type == PTAB)
-    {
-        if(region_id == ((unsigned int) -1))
-        {
-            boot_tty_puts( "No PTAB vobjs are allowed in the global region" );
-            boot_exit();
-        }
-        if(vobj->length < (PT1_SIZE + PT2_SIZE) ) //at least one pt2 => ( max_pt2 >= 1)
-        {
-            boot_tty_puts("PTAB too small, minumum size is ");
-            boot_tty_putw( PT1_SIZE + PT2_SIZE);
-            boot_exit();
-        }
-
-        _ptabs[region_id]        = (page_table_t*) vobj->paddr;
-        _max_pte2[region_id]    = (vobj->length - PT1_SIZE) / PT2_SIZE;
-
-#if BOOT_DEBUG_VIEW
-        boot_tty_puts("ptabs for vspace ");
-        boot_tty_putw(region_id);
-        boot_tty_puts(" address: ");
-        boot_tty_putw((unsigned)_ptabs[region_id]);
-        boot_tty_puts("\n");
-#endif
-    } 
+unsigned int align_to( unsigned int toAlign, 
+                       unsigned int alignPow2)
+{
+    unsigned int    mask = (1 << alignPow2) - 1;
+    return ((toAlign + mask ) & ~mask ); 
 }
 
@@ -660,12 +619,13 @@
 // It updates the page allocator (nextfreepage field of the pseg),
 // and checks a possible pseg overflow.
-// region_id: the vspace in wich the vseg is located or the global space(-1).
+// It is a global vseg if vspace_id = (-1) 
 ///////////////////////////////////////////////////////////////////////////
-void boot_vseg_map( mapping_vseg_t* vseg, unsigned int region_id ) 
-{
-    unsigned pages;
-    unsigned vobj_id;
-    unsigned cur_vaddr;
-    unsigned cur_paddr;
+void boot_vseg_map( mapping_vseg_t*     vseg, 
+                    unsigned int        vspace_id ) 
+{
+    unsigned int        pages;
+    unsigned int        vobj_id;
+    unsigned int        cur_vaddr;
+    unsigned int        cur_paddr;
     mapping_header_t*   header = (mapping_header_t*)&seg_mapping_base;  
     mapping_vobj_t*     vobj   = boot_get_vobj_base( header );
@@ -677,58 +637,83 @@
     if ( vseg->ident != 0 )            // identity mapping required
     {
-        // check physical segment overflow  
-        if ( (vseg->vbase < pseg->base) || 
-             ((vseg->vbase + vseg->length) > (pseg->base + pseg->length)) )
-        {
-            boot_tty_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
-            boot_tty_puts("impossible identity mapping for virtual segment: ");
-            boot_tty_puts( vseg->name ); 
-            boot_tty_puts("\n"); 
-            boot_exit();
-        }
-        vseg->pbase = vseg->vbase;
+         vseg->pbase = vseg->vbase;
     }
     else                                // unconstrained mapping
     {
-        // check physical segment overflow
-        if ( (vseg->vbase + vseg->length) > (pseg->base + pseg->length) )
-        {
-            boot_tty_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
-            boot_tty_puts("physical segment ");
-            boot_tty_puts( pseg->name ); 
-            boot_tty_puts(" is too small to map virtual segment");
-            boot_tty_puts( vseg->name ); 
-            boot_tty_puts("\n");
-            boot_exit();
-        }
         vseg->pbase = pseg->base + (pseg->next_free_page<<12);
     }
     
-
-    //loop on vobj:
-    // + to computes the length of the current vseg
-    // + Align vobjs
-    // + Initialise the vobj
+    // loop on vobjs to computes the length of the vseg,
+    // initialise the vaddr and paddr fields of all vobjs,
+    // and initialise the page table pointers array 
     cur_vaddr = vseg->vbase;
     cur_paddr = vseg->pbase;
-    for(vobj_id= vseg->vobj_offset; vobj_id < (vseg->vobj_offset + vseg->vobjs); vobj_id++)
-    {
-        if(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 = align_to(cur_paddr, vobj[vobj_id].align);
         }
 
-        //set vaddr/paddr
+        // set vaddr/paddr
         vobj[vobj_id].vaddr = cur_vaddr;        
         vobj[vobj_id].paddr = cur_paddr;  
       
-        //set next vaddr/paddr
+        // set next vaddr/paddr
         cur_vaddr += vobj[vobj_id].length;
         cur_paddr += vobj[vobj_id].length; 
-        initailise_vobj(&vobj[vobj_id], region_id);
+
+        // initialise _ptabs[] and _max_pt2[]
+        if ( vobj[vobj_id].type == VOBJ_TYPE_PTAB )
+        {
+            if(vobj[vobj_id].length < (PT1_SIZE + PT2_SIZE) ) // max_pt2 >= 1
+            {
+                boot_puts( "\n[BOOT ERROR] in boot_vseg_map() function: " );
+                boot_puts("PTAB vobj is too small in vspace ");
+                boot_putw(vspace_id);
+                boot_puts("\n");
+                boot_exit();
+            }
+            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();
+            }
+            _ptabs[vspace_id]   = (page_table_t*)vobj[vobj_id].paddr;
+            _max_pt2[vspace_id] = (vobj[vobj_id].length - PT1_SIZE) / PT2_SIZE;
+        }
     } 
     
-    //set the length
-    vseg->length = align_to((cur_paddr - vseg->pbase), 12);
+    //set the vseg length
+    unsigned int plength = pseg->length;
+    unsigned int vlength = cur_paddr - vseg->pbase;
+    vseg->length = align_to(vlength, 12);
+
+    // checking pseg overflow
+    if ( (vseg->pbase < pseg->base) || 
+         ((vseg->pbase + vlength) > (pseg->base + plength)) )
+    {
+        boot_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
+        boot_puts("impossible identity mapping for virtual segment: ");
+        boot_puts( vseg->name ); 
+        boot_puts("\n"); 
+        boot_puts("vseg pbase = ");
+        boot_putw( vseg->pbase ); 
+        boot_puts("\n"); 
+        boot_puts("vseg length = ");
+        boot_putw( vseg->length ); 
+        boot_puts("\n"); 
+        boot_puts("pseg pbase = ");
+        boot_putw( pseg->base ); 
+        boot_puts("\n"); 
+        boot_puts("pseg length = ");
+        boot_putw( pseg->length ); 
+        boot_puts("\n"); 
+        boot_exit();
+    }
 
     // computes number of pages
@@ -743,11 +728,11 @@
 
 #if BOOT_DEBUG_PT
-boot_tty_puts("- vseg ");
-boot_tty_puts( vseg->name );
-boot_tty_puts(" : vbase = ");
-boot_tty_putw( vseg->vbase );
-boot_tty_puts(" / pbase = ");
-boot_tty_putw( vseg->pbase );
-boot_tty_puts("\n");
+boot_puts("- vseg ");
+boot_puts( vseg->name );
+boot_puts(" : vbase = ");
+boot_putw( vseg->vbase );
+boot_puts(" / pbase = ");
+boot_putw( vseg->pbase );
+boot_puts("\n");
 #endif  
 
@@ -755,5 +740,5 @@
 
 /////////////////////////////////////////////////////////////////////
-// This function cheks the mapping_info data structure 
+// This function checks the mapping_info data structure 
 /////////////////////////////////////////////////////////////////////
 void boot_check_mapping()
@@ -764,7 +749,7 @@
     if ( header->signature != IN_MAPPING_SIGNATURE )
     {
-        boot_tty_puts("\n[BOOT ERROR] Illegal mapping signature: ");
-        boot_tty_putw(header->signature);
-        boot_tty_puts("\n");
+        boot_puts("\n[BOOT ERROR] Illegal mapping signature: ");
+        boot_putw(header->signature);
+        boot_puts("\n");
         boot_exit();
     }
@@ -777,10 +762,10 @@
     if ( header->clusters != NB_CLUSTERS )
     {
-        boot_tty_puts("\n[BOOT ERROR] Incoherent NB_CLUSTERS");
-        boot_tty_puts("\n             - In giet_config,  value = ");
-        boot_tty_putw ( NB_CLUSTERS );
-        boot_tty_puts("\n             - In mapping_info, value = ");
-        boot_tty_putw ( header->clusters );
-        boot_tty_puts("\n");
+        boot_puts("\n[BOOT ERROR] Incoherent NB_CLUSTERS");
+        boot_puts("\n             - In giet_config,  value = ");
+        boot_putw ( NB_CLUSTERS );
+        boot_puts("\n             - In mapping_info, value = ");
+        boot_putw ( header->clusters );
+        boot_puts("\n");
         boot_exit();
     }
@@ -789,10 +774,10 @@
     if ( header->ttys != NB_TTYS )
     {
-        boot_tty_puts("\n[BOOT ERROR] Incoherent NB_TTYS");
-        boot_tty_puts("\n             - In giet_config,  value = ");
-        boot_tty_putw ( NB_TTYS );
-        boot_tty_puts("\n             - In mapping_info, value = ");
-        boot_tty_putw ( header->ttys );
-        boot_tty_puts("\n");
+        boot_puts("\n[BOOT ERROR] Incoherent NB_TTYS");
+        boot_puts("\n             - In giet_config,  value = ");
+        boot_putw ( NB_TTYS );
+        boot_puts("\n             - In mapping_info, value = ");
+        boot_putw ( header->ttys );
+        boot_puts("\n");
         boot_exit();
     }
@@ -801,6 +786,6 @@
     if ( header->vspaces > GIET_NB_VSPACE_MAX )
     {
-        boot_tty_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
-        boot_tty_puts("\n");
+        boot_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
+        boot_puts("\n");
         boot_exit();
     }
@@ -825,16 +810,18 @@
     unsigned int        pseg_id;
 
-    // first loop on virtual spaces to map global vsegs
+    // checking mapping_info
+    boot_check_mapping();
+
+    // physical page allocators must be initialised 
+    for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
+    {
+        pseg[pseg_id].next_free_page = 0;
+    }
 
 #if BOOT_DEBUG_PT
-boot_tty_puts("\n******* mapping global vsegs ********");
+boot_puts("\n******* mapping global vsegs ********\n");
 #endif
             
-    // physical page allocators must be initialised ???
-    for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
-    {
-        pseg[pseg_id].next_free_page = 0;
-    }
-
+    // step 1 : first loop on virtual spaces to map global vsegs
     for ( vseg_id = 0 ; vseg_id < header->globals ; vseg_id++ )
     {
@@ -842,12 +829,12 @@
     }
 
-    // loop on virtual vspaces to map private vsegs
+    // step 2 : loop on virtual vspaces to map private vsegs
     for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
     {
 
 #if BOOT_DEBUG_PT
-boot_tty_puts("\n******* mapping private vsegs in vspace ");
-boot_tty_puts(vspace[vspace_id].name);
-boot_tty_puts(" ********\n");
+boot_puts("\n******* mapping private vsegs in vspace ");
+boot_puts(vspace[vspace_id].name);
+boot_puts(" ********\n");
 #endif
             
@@ -860,37 +847,28 @@
     } 
 
-    // loop on the vspaces to build the page tables
+    // step 3 : loop on the vspaces to build the page tables
     for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
     {
 
 #if BOOT_DEBUG_PT
-boot_tty_puts("\n******* building page table for vspace ");
-boot_tty_puts(vspace[vspace_id].name);
-boot_tty_puts(" ********\n");
+boot_puts("\n******* 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(">>> page table physical address = ");
+boot_putw((unsigned)_ptabs[vspace_id]);
+boot_puts("\n");
+#endif
     } 
+
+    boot_puts("\n[BOOT] Page Tables initialisation completed at cycle ");
+    boot_putw( boot_time() );
+    boot_puts("\n");
+
 } // end boot_pt_init()
-
-
-
-////////////////////////////////////////////////////////////////////////////////////
-// boot_init()
-// This function is executed by one single processor to initialize the page
-// tables, the tasks contexts and the peripherals, for all applications.
-////////////////////////////////////////////////////////////////////////////////////
-void boot_init()
-{
-    // checking mapping_info
-    boot_check_mapping();
-
-    // building page tables
-    boot_pt_init();
-    boot_tty_puts("\n[BOOT] Page Tables completed at cycle ");
-    boot_tty_putw( boot_time() );
-    boot_tty_puts("\n");
-
-} // end boot_init()
 
 // Local Variables:
