Index: soft/giet_vm/sys/kernel_init.c
===================================================================
--- soft/giet_vm/sys/kernel_init.c	(revision 220)
+++ soft/giet_vm/sys/kernel_init.c	(revision 228)
@@ -37,8 +37,8 @@
 
 __attribute__((section (".kdata"))) 
-unsigned int 			_ptabs_paddr[GIET_NB_VSPACE_MAX]; 
-
-__attribute__((section (".kdata"))) 
-unsigned int 			_ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
+unsigned int _ptabs_paddr[GIET_NB_VSPACE_MAX]; 
+
+__attribute__((section (".kdata"))) 
+unsigned int _ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
 
 ///////////////////////////////////////////////////////////////////////////////////
@@ -47,5 +47,5 @@
 
 __attribute__((section (".kdata"))) 
-static_scheduler_t*		_schedulers_paddr[NB_CLUSTERS*NB_PROCS_MAX]; 
+static_scheduler_t * _schedulers_paddr[NB_CLUSTERS * NB_PROCS_MAX]; 
 
 ///////////////////////////////////////////////////////////////////////////////////
@@ -54,20 +54,19 @@
 
 __attribute__((section (".kdata"))) 
-unsigned int			_idle_stack[NB_CLUSTERS*NB_PROCS_MAX*64]; 
-
-void _sys_exit()
-{
-    while(1);
+unsigned int _idle_stack[NB_CLUSTERS*NB_PROCS_MAX * 64]; 
+
+void _sys_exit() {
+    while (1);
 }
+
 
 //////////////////////////////////////////////////////////////////////////////////
 // This function is the entry point for the last step of the boot sequence.
 //////////////////////////////////////////////////////////////////////////////////
-__attribute__((section (".kinit"))) void _kernel_init()
-{
+__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;
+    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
@@ -76,11 +75,11 @@
 
 #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);
+    _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
 
@@ -88,15 +87,15 @@
     //          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);
+    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
 
@@ -107,9 +106,8 @@
     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; 
+    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;
@@ -117,19 +115,19 @@
 
 #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);
-#endif
-
-    }
- 
+        _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);
+#endif
+
+    }
+
     unsigned int isr_switch_channel = 0xFFFFFFFF;
 
@@ -142,46 +140,40 @@
     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) )
-        {
-             hwi_mask = hwi_mask | 0x1<< irq_id;
-        }
-        else if ( (isr == ISR_SWITCH) )
-        { 
-            pti_mask = pti_mask | 0x1<< irq_id;
+    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)) {
+            hwi_mask = hwi_mask | 0x1 << irq_id;
+        }
+        else if ((isr == ISR_SWITCH)) { 
+            pti_mask = pti_mask | 0x1 << irq_id;
             isr_switch_channel = irq_id;
         }
-        else if ( (isr == ISR_TIMER) )
-        {
-            pti_mask = pti_mask | 0x1<< irq_id;
-        }
-    }
-    _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);
+        else if ((isr == ISR_TIMER)) {
+            pti_mask = pti_mask | 0x1 << irq_id;
+        }
+    }
+    _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 ");
-            _putd( proc_id);
+            _putd(proc_id);
             _puts("\n");
             _release_lock(&_tty_put_lock);
@@ -189,22 +181,21 @@
         }
 
-        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 ");
-            _putd( proc_id);
+            _putd(proc_id);
             _puts("\n");
             _release_lock(&_tty_put_lock);
             _sys_exit();
         }
-        
-#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);
-#endif
-    
+
+#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);
+#endif
+
     } 
 
@@ -214,21 +205,21 @@
     //          it uses the page table of vspace[0]
     //          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);
-#endif
-    
+
+    _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);
+#endif
+
     // step 6 : each processor initialises SP, SR, PTPR, EPC, registers
     //          with the values corresponding to the first allocated task,
@@ -237,53 +228,61 @@
     unsigned int task_id;
 
-    if ( tasks == 0 )
-    {
+    if (tasks == 0) {
         task_id = IDLE_TASK_INDEX;
 
-        _get_lock( &_tty_put_lock );
+        _get_lock(&_tty_put_lock);
         _puts("\n[GIET WARNING] No task allocated to processor ");
-        _putd( global_pid );
+        _putd(global_pid);
         _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( 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);
+        _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
 
     // 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) );
+    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()
+
+// Local Variables:
+// tab-width: 4
+// c-basic-offset: 4
+// c-file-offsets:((innamespace . 0)(inline-open . 0))
+// indent-tabs-mode: nil
+// End:
+// vim: filetype=c:expandtab:shiftwidth=4:tabstop=4:softtabstop=4
+
