Index: trunk/kernel/kern/kernel_init.c
===================================================================
--- trunk/kernel/kern/kernel_init.c	(revision 124)
+++ trunk/kernel/kern/kernel_init.c	(revision 127)
@@ -1,5 +1,5 @@
 /*
  * kernel_init.c - kernel parallel initialization
- * 
+ *
  * Authors :  Mohamed Lamine Karaoui (2015)
  *            Alain Greiner  (2016,2017)
@@ -64,8 +64,8 @@
 // They are initialised by the kernel_init() function.
 //
-// WARNING : The section names have been defined to control the base addresses of the 
+// WARNING : The section names have been defined to control the base addresses of the
 // boot_info structure and the idle thread descriptors, through the kernel.ld script:
-// - the boot_info structure is build by the bootloader, and used by kernel_init.
-//   it must be first object in the kdata segment.
+// - the boot_info structure is built by the bootloader, and used by kernel_init.
+//   it must be the first object in the kdata segment.
 // - the array of idle threads descriptors must be placed on the first page boundary after
 //   the boot_info structure in the kdata segment.
@@ -81,5 +81,5 @@
                                    CONFIG_MAX_LOCAL_CORES]   CONFIG_PPM_PAGE_ALIGNED;
 
-// This variable defines the local cluster manager 
+// This variable defines the local cluster manager
 __attribute__((section(".kdata")))
 cluster_t            cluster_manager                         CONFIG_CACHE_LINE_ALIGNED;
@@ -105,17 +105,17 @@
 cxy_t                local_cxy                               CONFIG_CACHE_LINE_ALIGNED;
 
-// This variable defines the TXT0 chdev descriptor 
+// This variable defines the TXT0 chdev descriptor
 __attribute__((section(".kdata")))
 chdev_t              txt0_chdev                              CONFIG_CACHE_LINE_ALIGNED;
 
-// This variable is used for CP0 cores sychronisation in kernel_init()
+// This variable is used for CP0 cores synchronisation in kernel_init()
 __attribute__((section(".kdata")))
 remote_barrier_t     global_barrier                          CONFIG_CACHE_LINE_ALIGNED;
 
-// This variable is used for local cores sychronisation in kernel_init()
+// This variable is used for local cores synchronisation in kernel_init()
 __attribute__((section(".kdata")))
 barrier_t            local_barrier                           CONFIG_CACHE_LINE_ALIGNED;
 
-// This variable defines the array of supported File System contexts 
+// This variable defines the array of supported File System contexts
 __attribute__((section(".kdata")))
 vfs_ctx_t            fs_context[FS_TYPES_NR]                 CONFIG_CACHE_LINE_ALIGNED;
@@ -126,5 +126,5 @@
 ///////////////////////////////////////////////////////////////////////////////////////////
 static void print_banner( uint32_t nclusters , uint32_t ncores )
-{ 
+{
     printk("\n"
            "                    _        __    __     _____     ______         __    __    _   __   _     _   \n"
@@ -137,17 +137,17 @@
            "    /_/        \\_\\ |______| |_|    |_|   \\_____/  |______/        |_|    |_|  |_|  \\_\\ |_|   |_|  \n"
            "\n\n\t\t Advanced Locality Management Operating System / Multi Kernel Hybrid\n"
-           "\n\n\t\t\t Version 0.0   :   %d clusters   /   %d cores per cluster\n\n", nclusters , ncores ); 
+           "\n\n\t\t\t Version 0.0   :   %d clusters   /   %d cores per cluster\n\n", nclusters , ncores );
 }
 
 
 ///////////////////////////////////////////////////////////////////////////////////////////
-// This static function initializes the TXT0 chdev descriptor, associated to the "kernel 
-// terminal", and shared by all kernel instances for debug messages. It also register it
+// This static function initializes the TXT0 chdev descriptor, associated to the "kernel
+// terminal", and shared by all kernel instances for debug messages. It also registers it
 // in the chdev directory, containing extended pointers on all chdevs.
 // The global variable txt0_chdev is replicated in all clusters, but only the chdev
 // allocated in I/O cluster is used by ALMOS-MKH.
 // Therefore, this function must be called by a thread running in the I/O cluster.
-// As this TXT0 chdev supports only the TXT_SYNC_WRITE command,  we don't create
-// a server thread,  we don't allocate a WTI, and we don't initialize the waiting queue.
+// As this TXT0 chdev supports only the TXT_SYNC_WRITE command, we don't create
+// a server thread, we don't allocate a WTI, and we don't initialize the waiting queue.
 ///////////////////////////////////////////////////////////////////////////////////////////
 // @ info    : pointer on the local boot-info structure.
@@ -156,20 +156,20 @@
 {
     boot_device_t * dev_tbl;         // pointer on array of devices in boot_info
-	uint32_t        dev_nr;          // actual number of devices in this cluster
-	xptr_t          base;            // remote pointer on segment base
+    uint32_t        dev_nr;          // actual number of devices in this cluster
+    xptr_t          base;            // remote pointer on segment base
     uint32_t        type;            // peripheral type
-    uint32_t        func;            // device functionnal index
+    uint32_t        func;            // device functional index
     uint32_t        impl;            // device implementation index
-	uint32_t        i;               // device index in dev_tbl
-	uint32_t        x;               // X cluster coordinate
-	uint32_t        y;               // Y cluster coordinate
+    uint32_t        i;               // device index in dev_tbl
+    uint32_t        x;               // X cluster coordinate
+    uint32_t        y;               // Y cluster coordinate
 
     // get number of peripherals and base of devices array from boot_info
-	dev_nr	    = info->ext_dev_nr;
+    dev_nr      = info->ext_dev_nr;
     dev_tbl     = info->ext_dev;
 
     // loop on external peripherals to find TXT device
-	for( i = 0 ; i < dev_nr ; i++ )
-	{
+    for( i = 0 ; i < dev_nr ; i++ )
+    {
         base        = dev_tbl[i].base;
         type        = dev_tbl[i].type;
@@ -177,5 +177,5 @@
         impl        = IMPL_FROM_TYPE( type );
 
-        if (func == DEV_FUNC_TXT ) 
+        if (func == DEV_FUNC_TXT )
         {
             // initialize basic fields
@@ -210,13 +210,11 @@
             }
 
-		    kinit_dmsg("\n[INFO] %s : core[%x][0] created TXT0 chdev"
+            kinit_dmsg("\n[INFO] %s : core[%x][0] created TXT0 chdev"
                        " / paddr = %l at cycle %d\n",
                        __FUNCTION__ , local_cxy , chdev_func_str( func ),
                        XPTR(local_cxy , &txt0_chdev) , hal_get_cycles() );
         }
-
-	} // end loop on devices
-
-}  // end txt0_device_init()
+    }
+}
 
 ///////////////////////////////////////////////////////////////////////////////////////////
@@ -233,7 +231,7 @@
 {
     boot_device_t * dev;             // pointer on boot_info device (ICU/MMC/DMA)
-	uint32_t        x;               // X cluster coordinate
-	uint32_t        y;               // Y cluster coordinate
-	chdev_t       * chdev_ptr;       // local pointer on chdev descriptor
+    uint32_t        x;               // X cluster coordinate
+    uint32_t        y;               // Y cluster coordinate
+    chdev_t       * chdev_ptr;       // local pointer on chdev descriptor
     xptr_t          chdev_xp;        // extended pointer on chdev descriptor
 
@@ -244,5 +242,5 @@
     assert( ((info->cores_nr == 0) || (dev->channels != 0)) , __FUNCTION__ ,
             "ICU device must exist in cluster containing cores" );
-        
+
     assert( (dev->channels == 1) , __FUNCTION__ ,
             "channels number must be 1 for ICU device" );
@@ -259,15 +257,15 @@
 
     assert( (chdev_ptr != NULL) , __FUNCTION__ , "cannot allocate ICU chdev" );
-            
-    // get extended pointer on chdev descriptor 
+
+    // get extended pointer on chdev descriptor
     chdev_xp = XPTR( local_cxy , chdev_ptr );
 
-    // make ICU specific initialisation 
+    // make ICU specific initialisation
     // TODO remove these three parameters
     dev_icu_init( chdev_ptr , dev->param0 , dev->param1 , dev->param2 );
 
     // initialize the ICU field in the chdev_dir[x][y] structures
-    // replicated in all clusters, and containing extended pointers 
-    // on all remotely accessible devices 
+    // replicated in all clusters, and containing extended pointers
+    // on all remotely accessible devices
     for( x = 0 ; x < info->x_size ; x++ )
     {
@@ -280,5 +278,5 @@
 
     // initialize the entries of the local chdev_icu_input structure
-    // defining how internal peripherals are connected to ICU 
+    // defining how internal peripherals are connected to ICU
     uint32_t   id;
     uint8_t    valid;
@@ -304,5 +302,5 @@
                __FUNCTION__ , local_cxy , hal_get_cycles() );
 
-    /////////// MMC internal chdev ///////////  
+    /////////// MMC internal chdev ///////////
 
     dev = &info->dev_mmc;
@@ -310,5 +308,5 @@
     if( dev->channels != 0 )   // MMC device is defined
     {
-        assert( (dev->channels == 1) , __FUNCTION__ , 
+        assert( (dev->channels == 1) , __FUNCTION__ ,
             "channels number must be 1 for MMC device" );
 
@@ -324,14 +322,14 @@
 
         assert( (chdev_ptr != NULL) , __FUNCTION__ , "cannot allocate MMC chdev" );
-            
-        // get extended pointer on chdev descriptor 
+
+        // get extended pointer on chdev descriptor
         chdev_xp = XPTR( local_cxy , chdev_ptr );
 
         // make MMC specific initialisation
-        dev_mmc_init( chdev_ptr );     
+        dev_mmc_init( chdev_ptr );
 
         // initialize the MMC field in the chdev_dir[x][y] structures
-        // replicated in all clusters, and containing extended pointers 
-        // on all remotely accessible devices 
+        // replicated in all clusters, and containing extended pointers
+        // on all remotely accessible devices
         for( x = 0 ; x < info->x_size ; x++ )
         {
@@ -359,5 +357,5 @@
         uint32_t channel;
         for( channel = 0 ; channel < dev->channels ; channel++ )
-        { 
+        {
             chdev_ptr = chdev_create( FUNC_FROM_TYPE( dev->type ),
                                       IMPL_FROM_TYPE( dev->type ),
@@ -367,10 +365,10 @@
 
             assert( (chdev_ptr != NULL) , __FUNCTION__ , "cannot allocate DMA chdev" );
-            
-            // get extended pointer on channel descriptor 
+
+            // get extended pointer on channel descriptor
             chdev_xp = XPTR( local_cxy , chdev_ptr );
 
             // make DMA specific initialisation
-            dev_dma_init( chdev_ptr );     
+            dev_dma_init( chdev_ptr );
 
             // initialize only the DMA[channel] field in the local chdev_dir[x][y]
@@ -381,17 +379,17 @@
                        __FUNCTION__ , local_cxy , channel , hal_get_cycles() );
         }
-    } 
+    }
 }  // end internal_devices_init()
 
 ///////////////////////////////////////////////////////////////////////////////////////////
-// This static function allocates memory for the chdev descriptors associated 
+// This static function allocates memory for the chdev descriptors associated
 // to the external (shared) peripherals contained in the local cluster. These external
-// devices (IOB, IOC, TXT, NIC, etc ) are distributed on all clusters. 
+// devices (IOB, IOC, TXT, NIC, etc ) are distributed on all clusters.
 // It initialises these device descriptors as specified by the boot_info_t structure,
 // including the dynamic linking with the driver for the specified implementation.
 // Finally, all copies of the devices directory are initialised.
 //
-// The number of channel_devices depends on the device functionnal type.
-// There is three nested loops to build the full set of external channel_devices:
+// The number of channel_devices depends on the device functional type.
+// There are three nested loops to build the full set of external channel_devices:
 // - loop on external devices.
 // - loop on channels for multi-channels devices.
@@ -400,5 +398,5 @@
 // to select the cluster containing a given chdev[func,channel,direction].
 // All clusters scan the full set of chdevs, but only the cluster matching
-// (chdev_gid % (x_size*y_size)) create the corresponding chdev. 
+// (chdev_gid % (x_size*y_size)) create the corresponding chdev.
 //
 // TODO check that cluster IO contains a PIC [AG]
@@ -410,33 +408,33 @@
 {
     boot_device_t * dev_tbl;         // pointer on array of devices in boot_info
-	uint32_t        dev_nr;          // actual number of devices in this cluster
-	xptr_t          base;            // remote pointer on segment base
+    uint32_t        dev_nr;          // actual number of devices in this cluster
+    xptr_t          base;            // remote pointer on segment base
     uint32_t        type;            // peripheral type
     uint32_t        func;            // device functionnal index
     uint32_t        impl;            // device implementation index
-	uint32_t        i;               // device index in dev_tbl
-	uint32_t        x;               // X cluster coordinate
-	uint32_t        y;               // Y cluster coordinate
-	uint32_t        channels_nr;     // number of channels
-	uint32_t        channel;         // channel index
-	uint32_t        directions_nr;   // number of directions 
-	uint32_t        direction;       // direction index
-	uint32_t        p0;              // device parameter 0
-	uint32_t        p1;              // device parameter 1
-	uint32_t        p2;              // device parameter 2
-	uint32_t        p3;              // device parameter 3
+    uint32_t        i;               // device index in dev_tbl
+    uint32_t        x;               // X cluster coordinate
+    uint32_t        y;               // Y cluster coordinate
+    uint32_t        channels_nr;     // number of channels
+    uint32_t        channel;         // channel index
+    uint32_t        directions_nr;   // number of directions
+    uint32_t        direction;       // direction index
+    uint32_t        p0;              // device parameter 0
+    uint32_t        p1;              // device parameter 1
+    uint32_t        p2;              // device parameter 2
+    uint32_t        p3;              // device parameter 3
     uint32_t        first_channel;   // used in loop on channels
 
-	chdev_t       * chdev;           // local pointer on one channel_device descriptor
+    chdev_t       * chdev;           // local pointer on one channel_device descriptor
     xptr_t          chdev_xp;        // extended pointer on channel_device descriptor
     uint32_t        chdev_gid = 0;   // global index of channel_device descriptor
 
     // get number of peripherals and base of devices array from boot_info
-	dev_nr	    = info->ext_dev_nr;
+    dev_nr      = info->ext_dev_nr;
     dev_tbl     = info->ext_dev;
 
     // loop on external peripherals
-	for( i = 0 ; i < dev_nr ; i++ )
-	{
+    for( i = 0 ; i < dev_nr ; i++ )
+    {
         base        = dev_tbl[i].base;
         type        = dev_tbl[i].type;
@@ -461,5 +459,5 @@
         if( func == DEV_FUNC_ROM ) continue;
 
-        // check external device functionnal type
+        // check external device functional type
         if( (func != DEV_FUNC_IOB) &&
             (func != DEV_FUNC_PIC) &&
@@ -467,12 +465,12 @@
             (func != DEV_FUNC_TXT) &&
             (func != DEV_FUNC_NIC) &&
-            (func != DEV_FUNC_FBF) ) 
+            (func != DEV_FUNC_FBF) )
         {
             assert( false , __FUNCTION__ , "undefined external peripheral type" );
         }
 
-        // loops on channels 
+        // loops on channels
         for( channel = first_channel ; channel < channels_nr ; channel++ )
-        { 
+        {
             // loop on directions
             for( direction = 0 ; direction < directions_nr ; direction++ )
@@ -494,5 +492,5 @@
                                           base );
 
-                    assert( (chdev != NULL), __FUNCTION__ , 
+                    assert( (chdev != NULL), __FUNCTION__ ,
                             "cannot allocate external device" );
 
@@ -514,9 +512,9 @@
                     }
 
-                    // all external (shared) devices are remotely accessible 
+                    // all external (shared) devices are remotely accessible
                     // initialize the replicated chdev_dir[x][y] structures
-                    // defining the extended pointers on chdev descriptors 
-                    xptr_t * entry;    
-                
+                    // defining the extended pointers on chdev descriptors
+                    xptr_t * entry;
+
                     if( func == DEV_FUNC_IOB ) entry  = &chdev_dir.iob;
                     if( func == DEV_FUNC_PIC ) entry  = &chdev_dir.pic;
@@ -525,5 +523,5 @@
                     if( func == DEV_FUNC_FBF ) entry  = &chdev_dir.fbf[channel];
                     if( func == DEV_FUNC_NIC ) entry  = &chdev_dir.nic_tx[channel];
-  
+
                     for( x = 0 ; x < info->x_size ; x++ )
                     {
@@ -535,5 +533,5 @@
                     }
 
-		            kinit_dmsg("\n[INFO] %s : core[%x][0] create chdev %s[%d] at cycle %d\n",
+                    kinit_dmsg("\n[INFO] %s : core[%x][0] create chdev %s[%d] at cycle %d\n",
                                __FUNCTION__ , local_cxy , chdev_func_str( func ),
                                channel , hal_get_cycles() );
@@ -549,6 +547,6 @@
 
         // initialize the entries of the local chdev_pic_input structure
-        // defining how external peripherals are connected to PIC 
-        if( func == DEV_FUNC_PIC )  
+        // defining how external peripherals are connected to PIC
+        if( func == DEV_FUNC_PIC )
         {
             uint32_t   id;
@@ -577,25 +575,25 @@
                     else if( dev_func == DEV_FUNC_IOC )
                     {
-                        index = &chdev_pic_input.ioc[channel]; 
+                        index = &chdev_pic_input.ioc[channel];
                     }
                     else if( (dev_func == DEV_FUNC_NIC) && (is_rx == 0) )
                     {
-                        index = &chdev_pic_input.nic_tx[channel]; 
+                        index = &chdev_pic_input.nic_tx[channel];
                     }
                     else if( (dev_func == DEV_FUNC_NIC) && (is_rx != 0) )
                     {
-                        index = &chdev_pic_input.nic_rx[channel]; 
+                        index = &chdev_pic_input.nic_rx[channel];
                     }
                     else
                     {
                         assert( false , __FUNCTION__ , "illegal source device for PIC input" );
-                    }                   
+                    }
 
                     // set entry in local structure
-                    *index = id; 
+                    *index = id;
                 }
             } // end loop on PIC inputs
         } // end PIC
-	} // end loop on devices
+    } // end loop on devices
 }  // end external_devices_init()
 
@@ -615,9 +613,9 @@
                                      gid_t       * gid )
 {
-	uint32_t   i;
+    uint32_t   i;
     gid_t      global_id;
 
     // get global identifier from hardware register
-    global_id = hal_get_gid(); 
+    global_id = hal_get_gid();
 
     // makes an associative search in boot_info to get (cxy,lid) from global_id
@@ -649,5 +647,5 @@
     lid_t        core_lid = -1;      // running core local index
     cxy_t        core_cxy = -1;      // running core cluster identifier
-    gid_t        core_gid;           // running core hardware identifier 
+    gid_t        core_gid;           // running core hardware identifier
     cluster_t  * cluster;            // pointer on local cluster manager
     core_t     * core;               // pointer on running core descriptor
@@ -661,11 +659,11 @@
                                   &core_gid );
 
-    // CP0 initialise cluster identifier
+    // CP0 initializes cluster identifier
     if( core_lid == 0 ) local_cxy = info->cxy;
 
-    // each core get pointer on its private idle thread descriptor
- 	thread = (thread_t *)( idle_threads + (core_lid * CONFIG_THREAD_DESC_SIZE) );
-
-    // each core registers this thread pointer in hardware register 
+    // each core gets a pointer on its private idle thread descriptor
+    thread = (thread_t *)( idle_threads + (core_lid * CONFIG_THREAD_DESC_SIZE) );
+
+    // each core registers this thread pointer in hardware register
     hal_set_current_thread( thread );
 
@@ -673,15 +671,15 @@
     xlist_root_init( XPTR( local_cxy, &thread->xlocks_root ) );
 
-    // CP0 in I/O cluster initialises TXT0 chdev descriptor
+    // CP0 in I/O cluster initializes TXT0 chdev descriptor
     if( (core_lid == 0) && (core_cxy == info->io_cxy) ) txt0_device_init( info );
 
     /////////////////////////////////////////////////////////////////////////////////
     // global & local synchro to protect access to TXT0 terminal
-    if( core_lid == 0 ) remote_barrier( XPTR( info->io_cxy , &global_barrier ), 
+    if( core_lid == 0 ) remote_barrier( XPTR( info->io_cxy , &global_barrier ),
                                         (info->x_size * info->y_size) );
     barrier_wait( &local_barrier , info->cores_nr );
     /////////////////////////////////////////////////////////////////////////////////
 
-    if( (core_lid ==  0) && (local_cxy == info->io_cxy) ) 
+    if( (core_lid ==  0) && (local_cxy == info->io_cxy) )
     {
         kinit_dmsg("\n[INFO] %s : core[%x][%d] exit barrier 0 at cycle %d\n",
@@ -713,10 +711,10 @@
     /////////////////////////////////////////////////////////////////////////////////
     // global & local synchro, to protect access to cluster manager
-    if( core_lid == 0 ) remote_barrier( XPTR( info->io_cxy , &global_barrier ), 
+    if( core_lid == 0 ) remote_barrier( XPTR( info->io_cxy , &global_barrier ),
                                         (info->x_size * info->y_size) );
     barrier_wait( &local_barrier , info->cores_nr );
     /////////////////////////////////////////////////////////////////////////////////
 
-    if( (core_lid ==  0) && (local_cxy == info->io_cxy) ) 
+    if( (core_lid ==  0) && (local_cxy == info->io_cxy) )
     {
         kinit_dmsg("\n[INFO] %s : core[%x][%d] exit barrier 1 at cycle %d\n",
@@ -726,5 +724,5 @@
     // all cores get pointer on local cluster manager and on core descriptor
     cluster = &cluster_manager;
-  	core    = &cluster->core_tbl[core_lid];
+    core    = &cluster->core_tbl[core_lid];
 
     // CP0 initializes the process_zero descriptor
@@ -735,10 +733,10 @@
 #endif
 
-    // CP0 allocates and initialises the internal peripheral chdev descriptors.
+    // CP0 allocates and initializes the internal peripheral chdev descriptors.
     // Each CP0[cxy] scan the set of its internal (private) peripherals,
-    // and allocate memory for the corresponding chdev descriptors.
+    // and allocates memory for the corresponding chdev descriptors.
     if( core_lid == 0 ) internal_devices_init( info );
-        
-    // CP0 allocates one WTI mailbbox per core for Inter Processor Interrupt
+
+    // CP0 allocates one WTI mailbox per core for Inter Processor Interrupt
     // this must be done after ICU chdev initialisation, by CP0 only, and before
     // external devices initialisation to enforce the rule :
@@ -766,23 +764,23 @@
     // Each CP0[cxy] scan the set of external (shared) peripherals (but the TXT0),
     // and allocates memory for the chdev descriptors that must be placed
-    // on the (cxy) cluster according to the global index value.  
+    // on the (cxy) cluster according to the global index value.
     if( core_lid == 0 ) external_devices_init( info );
 
     /////////////////////////////////////////////////////////////////////////////////
     // global &local synchro to protect access to peripherals
-    if( core_lid == 0 ) remote_barrier( XPTR( info->io_cxy , &global_barrier ), 
+    if( core_lid == 0 ) remote_barrier( XPTR( info->io_cxy , &global_barrier ),
                                         (info->x_size * info->y_size) );
     barrier_wait( &local_barrier , info->cores_nr );
     /////////////////////////////////////////////////////////////////////////////////
 
-    if( (core_lid ==  0) && (local_cxy == info->io_cxy) ) 
-    {
-        kinit_dmsg("\n[INFO] %s : core[%x][%d] exit barrier 2 at cycle %d\n", 
+    if( (core_lid ==  0) && (local_cxy == info->io_cxy) )
+    {
+        kinit_dmsg("\n[INFO] %s : core[%x][%d] exit barrier 2 at cycle %d\n",
                    __FUNCTION__ , core_cxy , core_lid , hal_get_cycles() );
     }
 
     error = thread_kernel_init( thread,
-                                THREAD_IDLE, 
-                                &thread_idle_func, 
+                                THREAD_IDLE,
+                                &thread_idle_func,
                                 NULL,
                                 core_lid );
@@ -800,5 +798,5 @@
     thread_unblock( XPTR( local_cxy , thread ) , THREAD_BLOCKED_GLOBAL );
 
-    if( (core_lid ==  0) && (local_cxy == info->io_cxy) ) 
+    if( (core_lid ==  0) && (local_cxy == info->io_cxy) )
     {
         kinit_dmsg("\n[INFO] %s : core[%x][%d] created idle thread %x at cycle %d\n",
@@ -806,5 +804,5 @@
     }
 
-    // CP0 in all clusters initializes cooperatively VFS and DEVFS 
+    // CP0 in all clusters initializes cooperatively VFS and DEVFS
     if( (core_lid == 0)  )
     {
@@ -834,10 +832,10 @@
 
         // mount the DEVFS File system
-	    devfs_mount( root_inode_xp , "dev" );
+        devfs_mount( root_inode_xp , "dev" );
     }
 
 
     // CP0 in I/O cluster creates the process_init and print banner
-    if( (core_lid ==  0) && (local_cxy == info->io_cxy) ) 
+    if( (core_lid ==  0) && (local_cxy == info->io_cxy) )
     {
         process_init_create();
@@ -866,5 +864,5 @@
                    " - rwlock             : %d bytes\n"
                    " - remote rwlock      : %d bytes\n",
-                   sizeof( thread_t          ), 
+                   sizeof( thread_t          ),
                    sizeof( process_t         ),
                    sizeof( cluster_t         ),
@@ -895,11 +893,11 @@
     /////////////////////////////////////////////////////////////////////////////////
 
-    if( (core_lid ==  0) && (local_cxy == info->io_cxy) ) 
-    {
-        kinit_dmsg("\n[INFO] %s : core[%x][%d] exit barrier 3 at cycle %d\n", 
+    if( (core_lid ==  0) && (local_cxy == info->io_cxy) )
+    {
+        kinit_dmsg("\n[INFO] %s : core[%x][%d] exit barrier 3 at cycle %d\n",
                    __FUNCTION__ , core_cxy , core_lid , hal_get_cycles() );
     }
 
-    // each core activates its private PTI IRQ 
+    // each core activates its private PTI IRQ
     dev_icu_set_period( core_lid , CONFIG_SCHED_TICK_PERIOD );
     dev_icu_enable_irq( core_lid , PTI_TYPE , core_lid , NULL );
@@ -918,5 +916,4 @@
     // each core jump to idle thread
     thread_idle_func();
-
-} // end kernel_init()
-
+}
+
