Index: /soft/giet_vm/giet_boot/boot.c
===================================================================
--- /soft/giet_vm/giet_boot/boot.c	(revision 741)
+++ /soft/giet_vm/giet_boot/boot.c	(revision 742)
@@ -1952,5 +1952,5 @@
 
     // Each processor get kernel entry virtual address
-    unsigned int kernel_entry = (unsigned int)&kernel_init_vbase;
+    unsigned int kernel_entry = 0x80000000;
 
 #if BOOT_DEBUG_ELF
Index: /soft/giet_vm/giet_kernel/giet.s
===================================================================
--- /soft/giet_vm/giet_kernel/giet.s	(revision 741)
+++ /soft/giet_vm/giet_kernel/giet.s	(revision 742)
@@ -1,10 +1,9 @@
 /************************************************************************************
-* GIET: Interruption/Exception/Trap Handler for MIPS32 processor
+* This file contains the two entry points in the GIET_VM code:
+* - the _init entry point (from the boot code)      is 0x80000000 
+* - the _giet entry point (from user applications)  is 0x80000180 
+* => The base address of the segment containing this code MUST be 0x80000000.
 *
-* The base address of the segment containing this code MUST be 0x80000000, in
-* order to have the entry point at address 0x80000180!!! All messages are
-* printed on the TTY corresponding to the task&processor identifiers.
-*
-* It uses two arrays of functions:
+* The _giet uses two arrays of functions:
 * - the _cause_vector[16] array defines the 16 causes to enter the GIET
 *   it is initialized in th exc_handler.c file
@@ -14,5 +13,20 @@
 
     .section .giet, "ax", @progbits
-    .space 0x180
+
+/*
+ * INIT entry point (at address 0x80000000)
+ */
+
+    .func   _init
+    .type   _init, %function
+
+_init:
+    la      $26,    _kernel_init
+    jr      $26                        /* jump to _kernel_init */
+
+    .endfunc
+    .size _init, .-_init
+
+    .space  0x170                      /* the _entry function occupies 16 bytes */
 
 /*
@@ -29,5 +43,5 @@
     addu    $26,    $26,    $27		    /* $26 <= &_cause_vector[XCODE] */
     lw      $26,    ($26)               /* $26 <=  _cause_vector[XCODE] */
-    jr      $26                         /* Jump indexed by XCODE */
+    jr      $26                         /* Jump to handler indexed by XCODE */
 
     .endfunc
@@ -35,5 +49,5 @@
 
 /*
- * *** System Call Handler ***
+ * *** Syscall Handler ***
  *
  * A system call is handled as a special function call.
Index: /soft/giet_vm/giet_kernel/kernel.ld
===================================================================
--- /soft/giet_vm/giet_kernel/kernel.ld	(revision 741)
+++ /soft/giet_vm/giet_kernel/kernel.ld	(revision 742)
@@ -16,4 +16,5 @@
     {
         *(.giet)
+        *(.kinit)
         *(.text)
     }
@@ -24,10 +25,4 @@
         *(.kdata)
     }
-
-    . = kernel_init_vbase;
-    seg_kernel_init : 
-    {
-        *(.kinit)
-    }
 }
 
Index: /soft/giet_vm/giet_kernel/kernel_init.c
===================================================================
--- /soft/giet_vm/giet_kernel/kernel_init.c	(revision 741)
+++ /soft/giet_vm/giet_kernel/kernel_init.c	(revision 742)
@@ -137,5 +137,5 @@
 
 ////////////////////////////////////////////////////////////////////////////////
-// This kernel_init() function completes the kernel initialisation in 5 steps:
+// This _kernel_init() function completes the kernel initialisation in 5 steps:
 // Step 0 is done by processor[0,0,0]. Steps 1 to 4 are executed in parallel
 // by all processors.
@@ -146,5 +146,5 @@
 // - step 4 : Each processor set sp, sr, ptpr, epc registers values. 
 ////////////////////////////////////////////////////////////////////////////////
-__attribute__((section (".kinit"))) void kernel_init() 
+__attribute__((section (".kinit"))) void _kernel_init() 
 {
     // gpid  : hardware processor index (fixed format: X_WIDTH|Y_WIDTH|P_WIDTH)
Index: /soft/giet_vm/giet_python/mapping.py
===================================================================
--- /soft/giet_vm/giet_python/mapping.py	(revision 741)
+++ /soft/giet_vm/giet_python/mapping.py	(revision 742)
@@ -623,5 +623,4 @@
         kernel_data_found    = False
         kernel_code_found    = False
-        kernel_init_found    = False
         for vseg in self.globs:
 
@@ -645,9 +644,4 @@
                 kernel_code_size     = vseg.length
                 kernel_code_found    = True
-
-            if ( vseg.name[0:15] == 'seg_kernel_init' ):
-                kernel_init_vbase    = vseg.vbase
-                kernel_init_size     = vseg.length
-                kernel_init_found    = True
 
         # check if all required vsegs have been found
@@ -672,9 +666,4 @@
              sys.exit()
 
-        if ( kernel_init_found    == False ):
-             print '[genmap error] in giet_vsegs()'
-             print '    seg_kernel_init vseg missing'
-             sys.exit()
-
         # build string
         s =  '/* Generated by genmap for %s */\n'  % self.name
@@ -692,7 +681,4 @@
         s += 'kernel_data_vbase    = 0x%x;\n'   % kernel_data_vbase
         s += 'kernel_data_size     = 0x%x;\n'   % kernel_data_size
-        s += '\n'
-        s += 'kernel_init_vbase    = 0x%x;\n'   % kernel_init_vbase
-        s += 'kernel_init_size     = 0x%x;\n'   % kernel_init_size
         s += '\n'