Index: soft/giet_vm/sys/kernel_init.c
===================================================================
--- soft/giet_vm/sys/kernel_init.c	(revision 189)
+++ soft/giet_vm/sys/kernel_init.c	(revision 199)
@@ -8,9 +8,12 @@
 // It contains the kernel entry point for the last step of system initialisation. 
 // All procs in this phase have their MMU activated, and are running in parallel.
-// - each processor updates its own scheduler, to replace the ISR index 
-//   by the actual ISR virtual address, and set its own entry in the 
-//   kernel _schedulers_paddr[] array.
-// - each processor initialises the SP, SR, PTPR, EPC registers, and starts 
-//   its private Timer, before jumping to the user code with an eret. 
+// Each processor perform the following actions:
+// 1/ contributes to _schedulers_paddr[] initialisation
+// 2/ contributes to _ptabs_paddr[] and _ptabs_vaddr arrays initialisation 
+// 3/ computes and set the ICU mask for its private ICU channel
+// 4/ initialises its private TICK timer (if required)
+// 5/ initialises the "idle" task context in its private scheduler
+// 6/ initialises the SP, SR, PTPR, EPC registers
+// 7/ jumps to the user code with an eret. 
 ////////////////////////////////////////////////////////////////////////////////////
 
@@ -34,11 +37,14 @@
 
 __attribute__((section (".kdata"))) 
-page_table_t* _ptabs_paddr[GIET_NB_VSPACE_MAX]; 
-
-__attribute__((section (".kdata"))) 
-page_table_t* _ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
-
-__attribute__((section (".kdata"))) 
-static_scheduler_t*	_schedulers_paddr[NB_CLUSTERS*NB_PROCS_MAX]; 
+unsigned int 			_ptabs_paddr[GIET_NB_VSPACE_MAX]; 
+
+__attribute__((section (".kdata"))) 
+unsigned int 			_ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
+
+__attribute__((section (".kdata"))) 
+static_scheduler_t*		_schedulers_paddr[NB_CLUSTERS*NB_PROCS_MAX]; 
+
+__attribute__((section (".kdata"))) 
+unsigned int			_idle_stack[NB_CLUSTERS*NB_PROCS_MAX*64]; 
 
 //////////////////////////////////////////////////////////////////////////////////
@@ -47,10 +53,5 @@
 __attribute__((section (".kinit"))) void _kernel_init()
 {
-    // values to be written in registers
-    unsigned int	sp_value;
-    unsigned int	sr_value;
-    unsigned int	ptpr_value;
-    unsigned int	epc_value;
-
+    // compute cluster and local processor index
     unsigned int	proc_id    = _procid();
     unsigned int    cluster_id = proc_id / NB_PROCS_MAX;
@@ -66,7 +67,6 @@
 _get_lock(&_tty_put_lock);
 _puts("\n[GIET DEBUG] step 1 for processor ");
-_putw( proc_id );
-_puts("\n");
-_puts("- scheduler pbase = ");
+_putd( proc_id );
+_puts(" / scheduler pbase = ");
 _putw( (unsigned int)psched );
 _puts("\n");
@@ -74,5 +74,37 @@
 #endif
 
-    // step 2 : compute and set ICU mask 
+
+    // step 2 : initialise page table addresse arrays
+    //          it scans all tasks contexts in the scheduler 
+    //          and get VSID, PTAB and PTPR values
+
+    unsigned int ltid;
+    unsigned int tasks = _get_tasks_number();
+
+    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( proc_id );
+_puts(" / vspace ");
+_putd( vspace_id );
+_puts("\n- ptab vbase = ");
+_putw( ptab_vaddr );
+_puts("\n- ptab pbase = ");
+_putw( ptab_paddr );
+_puts("\n");
+_release_lock(&_tty_put_lock);
+#endif
+
+    }
+ 
+    // step 3 : compute and set ICU mask 
     unsigned int irq_id;
     unsigned int mask = 0;
@@ -89,8 +121,7 @@
 #if GIET_DEBUG_INIT
 _get_lock(&_tty_put_lock);
-_puts("\n[GIET DEBUG] step 2 for processor ");
-_putw( proc_id );
-_puts("\n");
-_puts("- ICU mask = ");
+_puts("\n[GIET DEBUG] step 3 for processor ");
+_putd( proc_id );
+_puts(" / ICU mask = ");
 _putw( mask );
 _puts("\n");
@@ -99,9 +130,5 @@
 
 
-    // step 3 : TODO initialise page table addresse arrays
-
-
     // step 4 : start TICK timer if more than one task
-    unsigned int tasks = _get_tasks_number();
     if ( tasks > 1 )
     {
@@ -122,9 +149,6 @@
 _get_lock(&_tty_put_lock);
 _puts("\n[GIET DEBUG] Step 4 for processor ");
-_putw( proc_id );
-_puts("\n");
-_puts("- TICK period = ");
-_putd( period );
-_puts("\n");
+_putd( proc_id );
+_puts(" / TICK activated\n");
 _release_lock(&_tty_put_lock);
 #endif
@@ -132,21 +156,56 @@
     } 
 
-    // step 5 : each processor initialises SP, SR, PTPR, EPC, registers
+    // step 5 : initialise the "idle" task context
+    //          the SR initialisation value is 0xFF03 because
+    //          the task _ctx_idle() executes in kernel mode...
+    //          it uses the page table of vspace[0]
+  
+    _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[proc_id] + 64 );
+    _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( proc_id );
+_puts(" / idle task context set\n");
+_release_lock(&_tty_put_lock);
+#endif
+    
+    // step 6 : each processor initialises SP, SR, PTPR, EPC, registers
     //          with the values corresponding to the first allocated task,
-    //          It does nothing, and keep idle if no task allocated.
-
-    if ( tasks )		// at leat one task allocated
-    {
-        // initialise registers
-        sp_value   = _get_current_context_slot(CTX_SP_ID);
-        sr_value   = _get_current_context_slot(CTX_SR_ID);
-        ptpr_value = _get_current_context_slot(CTX_PTPR_ID);
-        epc_value  = _get_current_context_slot(CTX_EPC_ID);
-
-#if GIET_DEBUG_INIT
-_get_lock(&_tty_put_lock);
-_puts("\n[GIET DEBUG] step 5 for processor ");
-_putw( proc_id );
-_puts("\n");
+    //          and starts the "idle" task if there is no task allocated.
+
+    unsigned int task_id;
+
+    if ( tasks == 0 )
+    {
+        task_id = IDLE_TASK_INDEX;
+
+        _get_lock( &_tty_put_lock );
+        _puts("\n [GIET WARNING] No task allocated to processor ");
+        _putw( proc_id );
+        _puts(" => idle\n");
+        _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( proc_id );
+_puts(" / registers initialised \n");
 _puts("- sp   = ");
 _putw( sp_value );
@@ -163,32 +222,14 @@
 _release_lock(&_tty_put_lock);
 #endif
-    }
-    else					// no task allocated
-    {
-        _get_lock( &_tty_put_lock );
-        _puts("\n No task allocated to processor ");
-        _putw( proc_id );
-        _puts(" => keep idle\n");
-        _release_lock ( &_tty_put_lock );
-
-        // enable interrupts in kernel mode
-        asm volatile ( "li	   $26, 0xFF01  \n"
-                       "mtc0   $26, $12     \n" 
-                       ::: "$26" );
-
-		// infinite loop in kernel mode
-        while (1) asm volatile("nop");
-    }
-
-    // set critical registers and jump to user code
-    asm volatile (
-       "move	$29,	%0		\n"		/* SP <= ctx[CTX_SP_ID] */
-       "mtc0	%1,		$12		\n"		/* SR <= ctx[CTX_SR_ID] */
-       "mtc2	%2,		$0		\n"		/* PTPR <= ctx[CTX_PTPR_ID] */
-       "mtc0	%3,		$14		\n"		/* EPC <= ctx[CTX_EPC_ID] */
-       "eret					\n"		/* jump to user code */
-       "nop						\n"
-       :
-       : "r"(sp_value), "r"(sr_value), "r"(ptpr_value), "r"(epc_value) );
+
+    // set  registers and jump to user code
+    asm volatile ( "move	$29,	%0		\n"		/* SP <= ctx[CTX_SP_ID] */
+                   "mtc0	%1,		$12		\n"		/* SR <= ctx[CTX_SR_ID] */
+                   "mtc2	%2,		$0		\n"		/* PTPR <= ctx[CTX_PTPR_ID] */
+                   "mtc0	%3,		$14		\n"		/* EPC <= ctx[CTX_EPC_ID] */
+                   "eret					\n"		/* jump to user code */
+                   "nop						\n"
+                   :
+                   : "r"(sp_value), "r"(sr_value), "r"(ptpr_value), "r"(epc_value) );
 
 } // end _kernel_init()
