Index: soft/giet_vm/sys/kernel_init.c
===================================================================
--- soft/giet_vm/sys/kernel_init.c	(revision 228)
+++ soft/giet_vm/sys/kernel_init.c	(revision 238)
@@ -33,28 +33,30 @@
 
 ///////////////////////////////////////////////////////////////////////////////////
-// array of pointers on the page tables (both virtual and physical addresses)
+// array of pointers on the page tables (virtual addresses)
 ///////////////////////////////////////////////////////////////////////////////////
 
 __attribute__((section (".kdata"))) 
-unsigned int _ptabs_paddr[GIET_NB_VSPACE_MAX]; 
+unsigned int _ptabs[GIET_NB_VSPACE_MAX];    // virtual addresses
+
+__attribute__((section (".kdata")))        
+unsigned int _ptprs[GIET_NB_VSPACE_MAX];    // physical addresses >> 13
+
+///////////////////////////////////////////////////////////////////////////////////
+// array of pointers on the schedulers (physical addresses)
+///////////////////////////////////////////////////////////////////////////////////
 
 __attribute__((section (".kdata"))) 
-unsigned int _ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
-
-///////////////////////////////////////////////////////////////////////////////////
-// array of pointers on the schedulers (physical addresses)
+static_scheduler_t* _schedulers[NB_CLUSTERS * NB_PROCS_MAX]; 
+
+///////////////////////////////////////////////////////////////////////////////////
+// staks for the "idle" tasks (256 bytes for each processor)
 ///////////////////////////////////////////////////////////////////////////////////
 
 __attribute__((section (".kdata"))) 
-static_scheduler_t * _schedulers_paddr[NB_CLUSTERS * NB_PROCS_MAX]; 
-
-///////////////////////////////////////////////////////////////////////////////////
-// staks for the "idle" tasks (256 bytes for each processor)
-///////////////////////////////////////////////////////////////////////////////////
-
-__attribute__((section (".kdata"))) 
-unsigned int _idle_stack[NB_CLUSTERS*NB_PROCS_MAX * 64]; 
-
-void _sys_exit() {
+unsigned int _idle_stack[NB_CLUSTERS * NB_PROCS_MAX * 64]; 
+
+////////////////
+void _sys_exit() 
+{
     while (1);
 }
@@ -63,42 +65,33 @@
 //////////////////////////////////////////////////////////////////////////////////
 // This function is the entry point for the last step of the boot sequence.
+// that is done in parallel by all processors, with MMU activated.
 //////////////////////////////////////////////////////////////////////////////////
-__attribute__((section (".kinit"))) void _kernel_init() {
-    // compute cluster and local processor index
-    unsigned int global_pid = _procid();
-    unsigned int cluster_id = global_pid / NB_PROCS_MAX;
-    unsigned int proc_id = global_pid % NB_PROCS_MAX;
-
-    // Step 0 : Compute number of tasks allocated to proc
-
-    unsigned int tasks = _get_tasks_number();
-
-#if GIET_DEBUG_INIT
-    _get_lock(&_tty_put_lock);
-    _puts("\n[GIET DEBUG] step 0 for processor ");
-    _putd(global_pid);
-    _puts(" : tasks = ");
-    _putd(tasks);
-    _puts("\n");
-    _release_lock(&_tty_put_lock);
-#endif
-
-    // step 1 : Initialise scheduler physical addresses array
-    //          get scheduler physical address (from CP0 register)
-
-    static_scheduler_t * psched = (static_scheduler_t *) _get_sched();
-    _schedulers_paddr[global_pid] = psched;
-
-#if GIET_DEBUG_INIT
-    _get_lock(&_tty_put_lock);
-    _puts("\n[GIET DEBUG] step 1 for processor ");
-    _putd(global_pid);
-    _puts(" / scheduler pbase = ");
-    _putx((unsigned int) psched);
-    _puts("\n");
-    _release_lock(&_tty_put_lock);
-#endif
-
-    // step 2 : initialise page table addresse arrays
+__attribute__((section (".kinit"))) void _kernel_init() 
+{
+    // Step 1 : get processor index,
+    //          get scheduler address
+    //          initialise _schedulers[] array
+
+    unsigned int        global_pid = _procid();
+    unsigned int        cluster_id = global_pid / NB_PROCS_MAX;
+    unsigned int        proc_id    = global_pid % NB_PROCS_MAX;
+    static_scheduler_t* psched     = _get_sched();
+    unsigned int        tasks      = psched->tasks;
+
+    _schedulers[global_pid] = psched;
+
+#if GIET_DEBUG_INIT
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] step 1 for processor ");
+_putd(global_pid);
+_puts(" : tasks = ");
+_putd(tasks);
+_puts(" / scheduler vbase = ");
+_putx((unsigned int) psched);
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
+
+    // step 2 : initialise ptabs[] & ptprs[] arrays
     //          each processor scans all tasks contexts in its
     //          private scheduler and get VSID, PTAB and PTPR values
@@ -106,29 +99,28 @@
     unsigned int ltid;
 
-    for (ltid = 0; ltid < tasks; ltid++) {
-        unsigned int vspace_id = _get_context_slot(ltid , CTX_VSID_ID); 
-        unsigned int ptab_vaddr = _get_context_slot(ltid , CTX_PTAB_ID); 
-        unsigned int ptab_paddr = _get_context_slot(ltid , CTX_PTPR_ID) << 13; 
-
-        _ptabs_vaddr[vspace_id] = ptab_vaddr;
-        _ptabs_paddr[vspace_id] = ptab_paddr;
-
-#if GIET_DEBUG_INIT
-        _get_lock(&_tty_put_lock);
-        _puts("\n[GIET DEBUG] step 2 for processor ");
-        _putd(global_pid);
-        _puts(" / vspace ");
-        _putd(vspace_id);
-        _puts("\n- ptab vbase = ");
-        _putx(ptab_vaddr);
-        _puts("\n- ptab pbase = ");
-        _putx(ptab_paddr);
-        _puts("\n");
-        _release_lock(&_tty_put_lock);
+    for (ltid = 0; ltid < tasks; ltid++) 
+    {
+        unsigned int vsid  = _get_task_slot(ltid , CTX_VSID_ID); 
+        unsigned int ptab  = _get_task_slot(ltid , CTX_PTAB_ID); 
+        unsigned int ptpr  = _get_task_slot(ltid , CTX_PTPR_ID); 
+
+        _ptabs[vsid] = ptab;
+        _ptprs[vsid] = ptpr;
+
+#if GIET_DEBUG_INIT
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] step 2 for processor ");
+_putd(global_pid);
+_puts(" / vspace ");
+_putd(vsid);
+_puts("\n- ptab = ");
+_putx(ptab);
+_puts("\n- ptpr = ");
+_putx(ptpr);
+_puts("\n");
+_release_lock(&_tty_put_lock);
 #endif
 
     }
-
-    unsigned int isr_switch_channel = 0xFFFFFFFF;
 
     // step 3 : compute and set ICU masks
@@ -136,41 +128,49 @@
     //          software interrupts are not supported yet
 
-    unsigned int irq_id;
+    unsigned int isr_switch_channel = 0xFFFFFFFF;
+    unsigned int irq_id;            // IN_IRQ index
     unsigned int hwi_mask = 0;
     unsigned int pti_mask = 0;
 
-    for (irq_id = 0; irq_id < 32; irq_id++) {
-        unsigned int entry = _get_interrupt_vector_entry(irq_id);
-        unsigned int isr = entry & 0x000000FF;
-
-        if ((isr == ISR_DMA) || (isr == ISR_IOC) || (isr == ISR_TTY)) {
+    for (irq_id = 0; irq_id < 32; irq_id++) 
+    {
+        unsigned int entry = psched->interrupt_vector[irq_id];
+        unsigned int isr   = entry & 0x000000FF;
+
+        if ((isr == ISR_DMA) || (isr == ISR_IOC) || (isr == ISR_TTY)) 
+        {
             hwi_mask = hwi_mask | 0x1 << irq_id;
         }
-        else if ((isr == ISR_SWITCH)) { 
+        else if ((isr == ISR_SWITCH)) 
+        { 
             pti_mask = pti_mask | 0x1 << irq_id;
             isr_switch_channel = irq_id;
         }
-        else if ((isr == ISR_TIMER)) {
+        else if ((isr == ISR_TIMER)) 
+        {
             pti_mask = pti_mask | 0x1 << irq_id;
         }
     }
+
+#if GIET_DEBUG_INIT
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] step 3 for processor ");
+_putd(global_pid);
+_puts("\n - ICU HWI_MASK = ");
+_putx(hwi_mask);
+_puts("\n - ICU PTI_MASK = ");
+_putx(pti_mask);
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
+
     _icu_set_mask(cluster_id, proc_id, hwi_mask, 0); // set HWI_MASK
     _icu_set_mask(cluster_id, proc_id, pti_mask, 1); // set PTI_MASK
 
-#if GIET_DEBUG_INIT
-    _get_lock(&_tty_put_lock);
-    _puts("\n[GIET DEBUG] step 3 for processor ");
-    _putd(global_pid);
-    _puts("\n - ICU HWI_MASK = ");
-    _putx(hwi_mask);
-    _puts("\n - ICU PTI_MASK = ");
-    _putx(pti_mask);
-    _puts("\n");
-    _release_lock(&_tty_put_lock);
-#endif
-
     // step 4 : start TICK timer if more than one task
-    if (tasks > 1) {
-        if (isr_switch_channel == 0xFFFFFFFF) {
+    if (tasks > 1) 
+    {
+        if (isr_switch_channel == 0xFFFFFFFF) 
+        {
             _get_lock(&_tty_put_lock);
             _puts("\n[GIET ERROR] ISR_SWITCH not found on proc ");
@@ -181,5 +181,6 @@
         }
 
-        if (_timer_start( cluster_id, isr_switch_channel, GIET_TICK_VALUE)) {
+        if (_timer_start( cluster_id, isr_switch_channel, GIET_TICK_VALUE)) 
+        {
             _get_lock(&_tty_put_lock);
             _puts("\n[GIET ERROR] ISR_SWITCH init error for proc ");
@@ -191,9 +192,9 @@
 
 #if GIET_DEBUG_INIT
-        _get_lock(&_tty_put_lock);
-        _puts("\n[GIET DEBUG] Step 4 for processor ");
-        _putd(global_pid);
-        _puts(" / context switch activated\n");
-        _release_lock(&_tty_put_lock);
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] Step 4 for processor ");
+_putd(global_pid);
+_puts(" / context switch activated\n");
+_release_lock(&_tty_put_lock);
 #endif
 
@@ -206,18 +207,20 @@
     //          the stack size is 256 bytes
 
-    _set_context_slot( IDLE_TASK_INDEX, CTX_RUN_ID, 1);
-    _set_context_slot( IDLE_TASK_INDEX, CTX_SR_ID,  0xFF03);
-    _set_context_slot( IDLE_TASK_INDEX, CTX_SP_ID,  (unsigned int) _idle_stack + ((global_pid + 1) << 8));
-    _set_context_slot( IDLE_TASK_INDEX, CTX_RA_ID,  (unsigned int) &_ctx_eret);
-    _set_context_slot( IDLE_TASK_INDEX, CTX_EPC_ID, (unsigned int) &_ctx_idle);
-    _set_context_slot( IDLE_TASK_INDEX, CTX_LTID_ID, IDLE_TASK_INDEX);
-    _set_context_slot( IDLE_TASK_INDEX, CTX_PTPR_ID, _ptabs_paddr[0] >> 13);
-
-#if GIET_DEBUG_INIT
-    _get_lock(&_tty_put_lock);
-    _puts("\n[GIET DEBUG] Step 5 for processor ");
-    _putd(global_pid);
-    _puts(" / idle task context set\n");
-    _release_lock(&_tty_put_lock);
+    unsigned int stack = (unsigned int)_idle_stack + ((global_pid + 1)<<8);
+
+    _set_task_slot( IDLE_TASK_INDEX, CTX_RUN_ID, 1);
+    _set_task_slot( IDLE_TASK_INDEX, CTX_SR_ID,  0xFF03);
+    _set_task_slot( IDLE_TASK_INDEX, CTX_SP_ID,  stack);
+    _set_task_slot( IDLE_TASK_INDEX, CTX_RA_ID,  (unsigned int) &_ctx_eret);
+    _set_task_slot( IDLE_TASK_INDEX, CTX_EPC_ID, (unsigned int) &_ctx_idle);
+    _set_task_slot( IDLE_TASK_INDEX, CTX_LTID_ID, IDLE_TASK_INDEX);
+    _set_task_slot( IDLE_TASK_INDEX, CTX_PTPR_ID, _ptprs[0]);
+
+#if GIET_DEBUG_INIT
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] Step 5 for processor ");
+_putd(global_pid);
+_puts(" / idle task context set\n");
+_release_lock(&_tty_put_lock);
 #endif
 
@@ -226,8 +229,9 @@
     //          and starts the "idle" task if there is no task allocated.
 
-    unsigned int task_id;
-
-    if (tasks == 0) {
-        task_id = IDLE_TASK_INDEX;
+    ltid = 0;
+
+    if (tasks == 0) 
+    {
+        ltid = IDLE_TASK_INDEX;
 
         _get_lock(&_tty_put_lock);
@@ -237,32 +241,39 @@
         _release_lock (&_tty_put_lock);
     }
-    else {
-        task_id = 0;
-    }
-
-    unsigned int sp_value = _get_context_slot(task_id, CTX_SP_ID);
-    unsigned int sr_value = _get_context_slot(task_id, CTX_SR_ID);
-    unsigned int ptpr_value = _get_context_slot(task_id, CTX_PTPR_ID);
-    unsigned int epc_value = _get_context_slot(task_id, CTX_EPC_ID);
-
-#if GIET_DEBUG_INIT
-    _get_lock(&_tty_put_lock);
-    _puts("\n[GIET DEBUG] step 6 for processor ");
-    _putd(global_pid);
-    _puts(" / registers initialised \n");
-    _puts("- sp   = ");
-    _putx(sp_value);
-    _puts("\n");
-    _puts("- sr   = ");
-    _putx(sr_value);
-    _puts("\n");
-    _puts("- ptpr = ");
-    _putx(ptpr_value << 13);
-    _puts("\n");
-    _puts("- epc  = ");
-    _putx(epc_value);
-    _puts("\n");
-    _release_lock(&_tty_put_lock);
-#endif
+
+    unsigned int sp_value   = _get_task_slot(ltid, CTX_SP_ID);
+    unsigned int sr_value   = _get_task_slot(ltid, CTX_SR_ID);
+    unsigned int ptpr_value = _get_task_slot(ltid, CTX_PTPR_ID);
+    unsigned int epc_value  = _get_task_slot(ltid, CTX_EPC_ID);
+
+    _set_task_slot( ltid, CTX_LTID_ID, ltid);
+
+#if GIET_DEBUG_INIT
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET DEBUG] step 6 for processor ");
+_putd(global_pid);
+_puts(" / registers initialised \n");
+_puts("- sp   = ");
+_putx(sp_value);
+_puts("\n");
+_puts("- sr   = ");
+_putx(sr_value);
+_puts("\n");
+_puts("- ptpr = ");
+_putx(ptpr_value);
+_puts("\n");
+_puts("- epc  = ");
+_putx(epc_value);
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
+
+_get_lock(&_tty_put_lock);
+_puts("\n[GIET] Processor ");
+_putd( global_pid );
+_puts(" starting user code at cycle ");
+_putd( _proctime() );
+_puts("\n");
+_release_lock(&_tty_put_lock);
 
     // set  registers and jump to user code
