Index: soft/giet_vm/giet_boot/boot.c
===================================================================
--- soft/giet_vm/giet_boot/boot.c	(revision 412)
+++ soft/giet_vm/giet_boot/boot.c	(revision 427)
@@ -274,30 +274,4 @@
                     unsigned int ppn )       // 28 bits right-justified
 {
-    // compute index in PT1
-    unsigned int    ix1 = vpn >> 9;         // 11 bits for ix1
-
-    // get page table physical base address 
-    paddr_t         pt1_pbase = _ptabs_paddr[vspace_id][x][y];
-
-    // check pt1_base
-    if ( pt1_pbase == 0 )
-    {
-        _puts("\n[BOOT ERROR] in boot_add_pte1() : illegal pbase address for PTAB[");
-        _putd( vspace_id );
-        _puts(",");
-        _putd( x );
-        _puts(",");
-        _putd( y );
-        _puts("]\n");
-        _exit();
-    }
-
-    // compute pte1 : 2 bits V T / 8 bits flags / 3 bits RSVD / 19 bits bppi
-    unsigned int    pte1 = PTE_V |
-                           (flags & 0x3FC00000) |
-                           ((ppn>>9) & 0x0007FFFF);
-
-    // write pte1 in PT1
-    _physical_write( pt1_pbase + 4*ix1, pte1 );
 
 #if (BOOT_DEBUG_PT > 1)
@@ -310,4 +284,34 @@
 _puts("] : vpn = ");
 _putx( vpn );
+#endif
+
+    // compute index in PT1
+    unsigned int    ix1 = vpn >> 9;         // 11 bits for ix1
+
+    // get page table physical base address 
+    paddr_t         pt1_pbase = _ptabs_paddr[vspace_id][x][y];
+
+    // check pt1_base
+    if ( pt1_pbase == 0 )
+    {
+        _puts("\n[BOOT ERROR] in boot_add_pte1() : illegal pbase address for PTAB[");
+        _putd( vspace_id );
+        _puts(",");
+        _putd( x );
+        _puts(",");
+        _putd( y );
+        _puts("]\n");
+        _exit();
+    }
+
+    // compute pte1 : 2 bits V T / 8 bits flags / 3 bits RSVD / 19 bits bppi
+    unsigned int    pte1 = PTE_V |
+                           (flags & 0x3FC00000) |
+                           ((ppn>>9) & 0x0007FFFF);
+
+    // write pte1 in PT1
+    _physical_write( pt1_pbase + 4*ix1, pte1 );
+
+#if (BOOT_DEBUG_PT > 1)
 _puts(" / ppn = ");
 _putx( ppn );
@@ -333,4 +337,16 @@
                     unsigned int ppn )       // 28 bits right-justified
 {
+
+#if (BOOT_DEBUG_PT > 1)
+_puts(" - PTE2 in PTAB[");
+_putd( vspace_id );
+_puts(",");
+_putd( x );
+_puts(",");
+_putd( y );
+_puts("] : vpn = ");
+_putx( vpn );
+#endif
+
     unsigned int ix1;
     unsigned int ix2;
@@ -394,12 +410,4 @@
 
 #if (BOOT_DEBUG_PT > 1)
-_puts(" - PTE2 in PTAB[");
-_putd( vspace_id );
-_puts(",");
-_putd( x );
-_puts(",");
-_putd( y );
-_puts("] : vpn = ");
-_putx( vpn );
 _puts(" / ppn = ");
 _putx( ppn );
@@ -456,5 +464,6 @@
 //  
 /////////////////////////////////////////////////////////////////////////////////////
-void boot_vseg_map( mapping_vseg_t* vseg )
+void boot_vseg_map( mapping_vseg_t* vseg,
+                    unsigned int    vspace_id )
 {
     mapping_header_t*   header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
@@ -484,4 +493,9 @@
     if ( vobj[vobj_id].type == VOBJ_TYPE_PTAB ) is_ptab = 1;
     else                                        is_ptab = 0;
+
+    // compute actual vspace index
+    unsigned int vsid;
+    if ( vspace_id == 0xFFFFFFFF ) vsid = 0;
+    else                           vsid = vspace_id;
 
     //////////// First step : compute vseg length and vobj(s) vbase
@@ -549,5 +563,5 @@
                 {
                     unsigned int ix1   = vpn >> 9;   // 11 bits
-                    paddr_t      paddr = _ptabs_paddr[0][x_dest][y_dest] + (ix1<<2);
+                    paddr_t      paddr = _ptabs_paddr[vsid][x_dest][y_dest] + (ix1<<2);
                     unsigned int pte1  = _physical_read( paddr );
                     if ( (pte1 & PTE_V) == 0 )     // BPP not allocated yet
@@ -580,5 +594,6 @@
     ////////////   by dividing the vseg in several sub-segments.
     //////////// - register it in _ptabs_vaddr & _ptabs_paddr arrays,
-    ////////////   and initialize the max_pt2 and next_pt2 allocators.
+    ////////////   and initialize next_pt2 allocators.
+    //////////// - reset all entries in first level page tables
     
     if ( is_ptab )
@@ -593,5 +608,5 @@
 
         // each PTAB must be aligned on a 8 Kbytes boundary
-        nsp = ( vseg->length << 12 ) / nspaces;
+        nsp = ( vseg->length >> 12 ) / nspaces;
         if ( (nsp & 0x1) == 0x1 ) nsp = nsp - 1;
 
@@ -601,8 +616,13 @@
         for ( vs = 0 ; vs < nspaces ; vs++ )
         {
-            offset += nsp;
             _ptabs_vaddr   [vs][x_dest][y_dest] = (vpn + offset) << 12;  
             _ptabs_paddr   [vs][x_dest][y_dest] = ((paddr_t)(ppn + offset)) << 12;
             _ptabs_next_pt2[vs][x_dest][y_dest] = 0;
+            offset += nsp;
+/*
+            // reset all entries in PT1 (8 Kbytes)
+            _physical_memset( _ptabs_paddr[vs][x_dest][y_dest], PT1_SIZE, 0 );
+            
+*/
         }
     }
@@ -637,6 +657,6 @@
 //  - PTEs are replicated in all clusters for a non local vseg.
 /////////////////////////////////////////////////////////////////////////////////////
-void boot_vseg_pte_init( mapping_vseg_t*  vseg,
-                         unsigned int     vspace_id )
+void boot_vseg_pte( mapping_vseg_t*  vseg,
+                    unsigned int     vspace_id )
 {
     // compute the "global" vseg attribute and actual vspace index
@@ -802,5 +822,5 @@
         }
     }  // end for pages
-}  // end boot_vseg_pte_init()
+}  // end boot_vseg_pte()
 
 ///////////////////////////////////////////////////////////////////////////////
@@ -818,5 +838,5 @@
 //    _ptabs_vaddr and _ptabs_paddr arrays if the vseg is a PTAB.
 //
-// B) page table initialisation : the boot_vseg_pte_init() function initialise 
+// B) page table initialisation : the boot_vseg_pte() function initialise 
 //    the PTEs (both PTE1 and PTE2) in one or several page tables:
 //    - PTEs are replicated in all vspaces for a global vseg.
@@ -858,5 +878,5 @@
         if ( (vobj[vobj_id].type == VOBJ_TYPE_PTAB) )
         {
-            boot_vseg_map( &vseg[vseg_id] );
+            boot_vseg_map( &vseg[vseg_id], 0xFFFFFFFF );
             vseg[vseg_id].mapped = 1;
         }
@@ -868,5 +888,5 @@
         if ( (vobj[vobj_id].type == VOBJ_TYPE_PTAB) )
         {
-            boot_vseg_pte_init( &vseg[vseg_id], 0xFFFFFFFF );
+            boot_vseg_pte( &vseg[vseg_id], 0xFFFFFFFF );
             vseg[vseg_id].mapped = 1;
         }
@@ -885,7 +905,7 @@
              (vseg[vseg_id].mapped == 0) )
         {
-            boot_vseg_map( &vseg[vseg_id] );
+            boot_vseg_map( &vseg[vseg_id], 0xFFFFFFFF );
             vseg[vseg_id].mapped = 1;
-            boot_vseg_pte_init( &vseg[vseg_id], 0xFFFFFFFF );
+            boot_vseg_pte( &vseg[vseg_id], 0xFFFFFFFF );
         }
     }
@@ -901,7 +921,7 @@
         if ( vseg[vseg_id].mapped == 0 )
         {
-            boot_vseg_map( &vseg[vseg_id] );
+            boot_vseg_map( &vseg[vseg_id], 0xFFFFFFFF );
             vseg[vseg_id].mapped = 1;
-            boot_vseg_pte_init( &vseg[vseg_id], 0xFFFFFFFF );
+            boot_vseg_pte( &vseg[vseg_id], 0xFFFFFFFF );
         }
     }
@@ -922,7 +942,7 @@
              vseg_id++) 
         {
-            boot_vseg_map( &vseg[vseg_id] );
+            boot_vseg_map( &vseg[vseg_id], vspace_id );
             vseg[vseg_id].mapped = 1;
-            boot_vseg_pte_init( &vseg[vseg_id], vspace_id );
+            boot_vseg_pte( &vseg[vseg_id], vspace_id );
         }
     }
@@ -1602,5 +1622,5 @@
 #endif
             // compute gpid (global processor index) and scheduler base address
-            unsigned int gpid = cluster_xy * NB_PROCS_MAX + lpid;
+            unsigned int gpid = (cluster_xy << P_WIDTH) + lpid;
             psched            = _schedulers[x][y][lpid];
 
@@ -2545,22 +2565,22 @@
     ///////////////////////////////////////////////////////////////////////////////
 
+    // all processor initialise the SCHED register
+    // from the _schedulers[x][y][lpid array]
+    unsigned int cluster_xy = gpid >> P_WIDTH;
+    unsigned int lpid       = gpid & ((1<<P_WIDTH)-1);
+    unsigned int x          = cluster_xy >> Y_WIDTH;
+    unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
+    _set_sched( (unsigned int)_schedulers[x][y][lpid] );
+
+    // all processors (but Proc[0,0,0]) activate MMU
+    if ( gpid != 0 )
+    {
+        _set_mmu_ptpr( (unsigned int)(_ptabs_paddr[0][x][y]>>13) );
+        _set_mmu_mode( 0xF );
+    }
+
     // all processors reset BEV bit in the status register to use
     // the GIET_VM exception handler instead of the PRELOADER exception handler
     _set_sr( 0 );
-
-    // all processor initialise the SCHED register
-    // from the _schedulers[x][y][lpid array]
-    unsigned int cluster_xy = gpid / NB_PROCS_MAX;
-    unsigned int lpid       = gpid % NB_PROCS_MAX;
-    unsigned int x          = cluster_xy >> Y_WIDTH;
-    unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
-    _set_sched( (unsigned int)_schedulers[x][y][lpid] );
-
-    // all processors (but Proc[0,0,0]) activate MMU
-    if ( gpid != 0 )
-    {
-        _set_mmu_ptpr( (unsigned int)(_ptabs_paddr[0][x][y]>>13) );
-        _set_mmu_mode( 0xF );
-    }
 
     // all processors jump to kernel_init 
