Index: soft/giet_vm/boot/boot_init.c
===================================================================
--- soft/giet_vm/boot/boot_init.c	(revision 198)
+++ soft/giet_vm/boot/boot_init.c	(revision 199)
@@ -23,17 +23,14 @@
 // and the mapping:
 // - physical segmentation of the physical address space, 
-// - number of virtual spaces (one multi-task application per vspace), 
-// - static placement of tasks on the processors, 
-// - static placement of virtual segments (vseg) in the physical segments (pseg).
-// - static placement of virtual objects (vobj) on virtual segments (vseg).
+// - 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, 
 //
-// The page table are statically constructed in the boot phase, and they do not 
+// The page table are statically build in the boot phase, and they do not 
 // change during execution. The GIET uses only 4 Kbytes pages.
 // 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
-// computed using the length of the vobj and stored in the boot_max_pt2 global variable,
-// which is a table indexed by the vspace_id.
-
-// defined by the (GIET_NB_PT2_MAX) configuration parameter.
+// computed during the boot phase.
 // The max number of virtual spaces (GIET_NB_VSPACE_MAX) is a configuration parameter.
 //
@@ -794,8 +791,4 @@
     mapping_periph_t*   periph  = boot_get_periph_base( header );
 
-    unsigned int periph_id;
-    unsigned int cluster_id;
-    unsigned int channels;
-
     // checking mapping availability
     if ( header->signature != IN_MAPPING_SIGNATURE )
@@ -807,5 +800,5 @@
     }
 
-    // checking NB_CLUSTERS
+    // checking Rnumber of clusters
     if ( header->clusters != NB_CLUSTERS )
     {
@@ -819,54 +812,101 @@
     }
 
-    // checking NB_PROC_MAX
+    // checking number of virtual spaces
+    if ( header->vspaces > GIET_NB_VSPACE_MAX )
+    {
+        boot_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
+        boot_puts("\n");
+        boot_exit();
+    }
+
+    // checking harware
+    unsigned int periph_id;
+    unsigned int cluster_id;
+    unsigned int channels;
+    unsigned int tty_found = 0;
+    unsigned int nic_found = 0;
     for ( cluster_id = 0 ; cluster_id < NB_CLUSTERS ; cluster_id++ )
     {
+        // NB_PROCS_MAX
         if ( cluster[cluster_id].procs > NB_PROCS_MAX )
         {
             boot_puts("\n[BOOT ERROR] too much processors in cluster ");
             boot_putw( cluster_id );
-            boot_puts("\n             - In giet_config, NB_PROCS_MAX = ");
-            boot_putw ( NB_PROCS_MAX );
-            boot_puts("\n             - In mapping_info, nprocs = ");
+            boot_puts(" : procs = ");
             boot_putw ( cluster[cluster_id].procs );
             boot_puts("\n");
             boot_exit();
         }
-    }
-
-    // checking number of virtual spaces
-    if ( header->vspaces > GIET_NB_VSPACE_MAX )
-    {
-        boot_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
-        boot_puts("\n");
-        boot_exit();
-    }
-
-    // checking TTY number
-    cluster_id = header->tty_clusterid;
-    for ( periph_id = cluster[cluster_id].periph_offset ;
-          periph_id < cluster[cluster_id].periph_offset + cluster[cluster_id].periphs ;
-          periph_id++ )
-    {
-        if ( periph[periph_id].type == PERIPH_TYPE_TTY ) 
-        {
-            channels = periph[periph_id].channels;
-            break;
-        }
-                
-    } 
-    if ( channels > NB_TTYS )
-    {
-        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 ( channels );
-        boot_puts("\n");
-        boot_exit();
-    }
-
-    // TODO same type of checking for TIMERS, DMAS, NIC channels
-
+
+        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 )
+                {
+                    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] Too much TTY terminals in cluster ");
+                    boot_putw( cluster_id );
+                    boot_puts(" : ttys = ");
+                    boot_putw ( periph[periph_id].channels );
+                    boot_puts("\n");
+                    boot_exit();
+                }
+                tty_found = 1;
+            }
+            // NB_NICS
+            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] Too much NIC channels in cluster ");
+                    boot_putw( cluster_id );
+                    boot_puts(" : nics = ");
+                    boot_putw ( periph[periph_id].channels );
+                    boot_puts("\n");
+                    boot_exit();
+                }
+                nic_found = 1;
+            }
+            // NB_TIMERS
+            if ( periph[periph_id].type == PERIPH_TYPE_TIM ) 
+            {
+                if ( periph[periph_id].channels > NB_TIMERS_MAX )
+                {
+                    boot_puts("\n[BOOT ERROR] Too much user timers in cluster ");
+                    boot_putw( cluster_id );
+                    boot_puts(" : timers = ");
+                    boot_putw ( periph[periph_id].channels );
+                    boot_puts("\n");
+                    boot_exit();
+                }
+            }
+            // NB_DMAS
+            if ( periph[periph_id].type == PERIPH_TYPE_DMA ) 
+            {
+                if ( periph[periph_id].channels > NB_DMAS_MAX )
+                {
+                    boot_puts("\n[BOOT ERROR] Too much DMA channels in cluster ");
+                    boot_putw( cluster_id );
+                    boot_puts(" : channels = ");
+                    boot_putw ( periph[periph_id].channels );
+                    boot_puts("\n");
+                    boot_exit();
+                }
+            }
+        } // end for periphs
+    } // end for clusters
 } // end boot_check_mapping()
 
@@ -1419,18 +1459,18 @@
               task_id++ )
         {
-            // ra :  the return address is &boot_eret()
-            unsigned int ra = (unsigned int)&boot_eret;
-
-            // sr : value required before an eret instruction
-            unsigned int sr = 0x0000FF13; 
-
-            // ptpr : page table physical base address (shifted by 13 bit)
-            unsigned int ptpr = (unsigned int)boot_ptabs_paddr[vspace_id] >> 13;
-
-            // ptab : page_table virtual base address (not a register)
-            unsigned int ptab = (unsigned int)boot_ptabs_vaddr[vspace_id];
-
-            // tty : terminal global index provided by a global allocator
-            unsigned int tty = 0xFFFFFFFF;
+            // ctx_ra :  the return address is &boot_eret()
+            unsigned int ctx_ra = (unsigned int)&boot_eret;
+
+            // ctx_sr : value required before an eret instruction
+            unsigned int ctx_sr = 0x0000FF13; 
+
+            // ctx_ptpr : page table physical base address (shifted by 13 bit)
+            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_tty = 0xFFFFFFFF;
             if ( task[task_id].use_tty ) 
             {
@@ -1444,10 +1484,10 @@
                     boot_exit();
                 }
-                tty = alloc_tty_channel;
+                ctx_tty = alloc_tty_channel;
                 alloc_tty_channel++;
             }
 
-            // nic : NIC channel global index provided by a global allocator
-            unsigned int nic = 0xFFFFFFFF;
+            // ctx_nic : NIC channel global index provided by a global allocator
+            unsigned int ctx_nic = 0xFFFFFFFF;
             if ( task[task_id].use_nic ) 
             {
@@ -1461,10 +1501,10 @@
                     boot_exit();
                 }
-                nic = alloc_nic_channel;
+                ctx_nic = alloc_nic_channel;
                 alloc_nic_channel++;
             }
 
-            // timer : user TIMER global index provided by a cluster allocator 
-            unsigned int timer = 0xFFFFFFFF;
+            // ctx_timer : user TIMER global index provided by a cluster allocator 
+            unsigned int ctx_timer = 0xFFFFFFFF;
             if ( task[task_id].use_timer ) 
             {
@@ -1479,10 +1519,10 @@
                     boot_exit();
                 }
-                timer = cluster_id*NB_TIMERS_MAX + alloc_timer_channel[cluster_id];
+                ctx_timer = cluster_id*NB_TIMERS_MAX + alloc_timer_channel[cluster_id];
                 alloc_timer_channel[cluster_id]++;
             }
 
-            // fbdma : DMA global index provided by a cluster allocator  
-            unsigned int fbdma = 0xFFFFFFFF;
+            // ctx_fbdma : DMA global index provided by a cluster allocator  
+            unsigned int ctx_fbdma = 0xFFFFFFFF;
             if ( task[task_id].use_fbdma ) 
             {
@@ -1497,18 +1537,17 @@
                     boot_exit();
                 }
-                fbdma = cluster_id*NB_DMAS_MAX + alloc_fbdma_channel[cluster_id];
+                ctx_fbdma = cluster_id*NB_DMAS_MAX + alloc_fbdma_channel[cluster_id];
                 alloc_fbdma_channel[cluster_id]++;
             }
 
-            // epc : Get the (virtual) base address of the start_vector containing
-            // the start addresses for all tasks defined in the vspace.
+            // 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;
-            unsigned int epc = start_vector_vbase[task[task_id].startid];
-
-            // sp :  Get the vobj containing the stack 
+            unsigned int ctx_epc = start_vector_vbase[task[task_id].startid];
+
+            // ctx_sp :  Get the vobj containing the stack 
             unsigned int vobj_id = task[task_id].vobjlocid + vspace[vspace_id].vobj_offset;
-            unsigned int sp = vobj[vobj_id].vaddr + vobj[vobj_id].length;
+            unsigned int ctx_sp = vobj[vobj_id].vaddr + vobj[vobj_id].length;
 
             // compute gpid = global processor index
@@ -1516,7 +1555,4 @@
                                 task[task_id].proclocid;
 
-            // sched : scheduler physical address
-            unsigned int sched = (unsigned int)boot_schedulers_paddr[gpid];
-
             // In the code below, we access the scheduler with specific access 
             // functions, because we only have the physical address of the scheduler, 
@@ -1526,5 +1562,5 @@
             unsigned int ltid = boot_scheduler_get_tasks( gpid );
 
-            if ( ltid >= 15 )
+            if ( ltid >= IDLE_TASK_INDEX )
             {
                 boot_puts("\n[BOOT ERROR] : ");
@@ -1543,14 +1579,17 @@
 
             // initializes the task context in scheduler[gpid]
-            boot_scheduler_set_context( gpid, ltid, CTX_SR_ID    , sr    );
-            boot_scheduler_set_context( gpid, ltid, CTX_SP_ID    , sp    );
-            boot_scheduler_set_context( gpid, ltid, CTX_RA_ID    , ra    );
-            boot_scheduler_set_context( gpid, ltid, CTX_EPC_ID   , epc   );
-            boot_scheduler_set_context( gpid, ltid, CTX_PTPR_ID  , ptpr  );
-            boot_scheduler_set_context( gpid, ltid, CTX_TTY_ID   , tty   );
-            boot_scheduler_set_context( gpid, ltid, CTX_TIMER_ID , timer );
-            boot_scheduler_set_context( gpid, ltid, CTX_FBDMA_ID , fbdma );
-            boot_scheduler_set_context( gpid, ltid, CTX_PTAB_ID  , ptab  );
-            boot_scheduler_set_context( gpid, ltid, CTX_SCHED_ID , sched );
+            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_FBDMA_ID , ctx_fbdma  );
+            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_RUN_ID   , 1          );
                                         
 #if BOOT_DEBUG_SCHED
@@ -1559,47 +1598,52 @@
 boot_puts(" allocated to processor ");
 boot_putw( gpid );
-boot_puts(" / ltid = ");
+boot_puts("  - ctx[LTID]   = ");
 boot_putw( ltid );
 boot_puts("\n");
 
-boot_puts("  - SR          = ");
-boot_putw( sr );
-boot_puts("\n");
-
-boot_puts("  - SP          = ");
-boot_putw( sp );
-boot_puts("\n");
-
-boot_puts("  - RA          = ");
-boot_putw( ra );
-boot_puts("\n");
-
-boot_puts("  - EPC         = ");
-boot_putw( epc );
-boot_puts("\n");
-
-boot_puts("  - PTPR        = ");
-boot_putw( ptpr<<13 );
-boot_puts("\n");
-
-boot_puts("  - TTY         = ");
-boot_putw( tty );
-boot_puts("\n");
-
-boot_puts("  - TIMER       = ");
-boot_putw( timer );
-boot_puts("\n");
-
-boot_puts("  - FBDMA       = ");
-boot_putw( fbdma );
-boot_puts("\n");
-
-boot_puts("  - PTAB        = ");
-boot_putw( ptab );
-boot_puts("\n");
-
-boot_puts("  - SCHED       = ");
-boot_putw( sched );
-boot_puts("\n");
+boot_puts("  - ctx[SR]     = ");
+boot_putw( ctx_sr );
+boot_puts("\n");
+
+boot_puts("  - ctx[SR]     = ");
+boot_putw( ctx_sp );
+boot_puts("\n");
+
+boot_puts("  - ctx[RA]     = ");
+boot_putw( ctx_ra );
+boot_puts("\n");
+
+boot_puts("  - ctx[EPC]    = ");
+boot_putw( ctx_epc );
+boot_puts("\n");
+
+boot_puts("  - ctx[PTPR]   = ");
+boot_putw( ctx_ptpr );
+boot_puts("\n");
+
+boot_puts("  - ctx[TTY]    = ");
+boot_putw( ctx_tty );
+boot_puts("\n");
+
+boot_puts("  - ctx[NIC]    = ");
+boot_putw( ctx_nic );
+boot_puts("\n");
+
+boot_puts("  - ctx[TIMER]  = ");
+boot_putw( ctx_timer );
+boot_puts("\n");
+
+boot_puts("  - ctx[FBDMA]  = ");
+boot_putw( ctx_fbdma );
+boot_puts("\n");
+
+boot_puts("  - ctx[PTAB]   = ");
+boot_putw( ctx_ptab );
+boot_puts("\n");
+
+boot_puts("  - ctx[VSID]   = ");
+boot_putw( vspace_id );
+boot_puts("\n");
+
 #endif
 
