Index: soft/giet_vm/sys/kernel_init.c
===================================================================
--- soft/giet_vm/sys/kernel_init.c	(revision 171)
+++ soft/giet_vm/sys/kernel_init.c	(revision 175)
@@ -5,4 +5,5 @@
 // Copyright (c) UPMC-LIP6
 ////////////////////////////////////////////////////////////////////////////////////
+// FIXME
 // The kernel_init.c files is part of the GIET-VM nano-kernel.
 // It contains the kernel entry point for the second phase of system initialisation: 
@@ -42,4 +43,5 @@
 ///////////////////////////////////////////////////////////////////////////////////
 
+void    _kernel_ptabs_init(void);
 void    _kernel_vobjs_init(void);
 void    _kernel_tasks_init(void);
@@ -64,4 +66,6 @@
     if ( pid == 0 )
     {
+        _kernel_ptabs_init();
+        /* must be called after the initialisation of ptabs */
         _kernel_vobjs_init();
         _kernel_tasks_init();
@@ -150,4 +154,236 @@
                  "nop");
 }
+
+///////////////////////////////////////////////////////////////////////////////
+// used to access user space
+///////////////////////////////////////////////////////////////////////////////
+void _set_ptpr(unsigned int vspace_id)
+{
+	unsigned int ptpr = ((unsigned int)_kernel_ptabs_paddr[vspace_id]) >> 13;
+	asm volatile("mtc2 %0, $0"::"r"(ptpr));
+}
+
+///////////////////////////////////////////////////////////////////////////////
+// This function initialises the _kernel_ptabs_paddr[] array indexed by the vspace_id,
+// and containing the base addresses of all page tables. 
+// This _kernel_ptabs_paddr[] array is used to initialise the task contexts.
+///////////////////////////////////////////////////////////////////////////////
+in_kinit void _kernel_ptabs_init()
+{
+    mapping_header_t*   header  = (mapping_header_t*)&seg_mapping_base;  
+    mapping_vspace_t*   vspace  = _get_vspace_base( header );     
+    mapping_vobj_t*     vobj    = _get_vobj_base( header );
+
+    unsigned int        vspace_id;  
+    unsigned int        vobj_id;
+
+    // loop on the vspaces 
+    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
+    {
+        char ptab_found = 0;
+
+#if INIT_DEBUG_CTX
+_puts("[INIT] --- vobjs initialisation in vspace "); 
+_puts(vspace[vspace_id].name);
+_puts("\n");
+#endif
+        // loop on the vobjs and get the ptpr
+	    for(vobj_id= vspace[vspace_id].vobj_offset; 
+			vobj_id < (vspace[vspace_id].vobj_offset+ vspace[vspace_id].vobjs);
+			vobj_id++)
+	    {
+            if(vobj[vobj_id].type == VOBJ_TYPE_PTAB)
+            {
+                if( ptab_found )
+                {
+                    _puts("\n[INIT ERROR] Only one PTAB for by vspace ");
+                    _putw( vspace_id );
+                    _exit();
+                }
+
+                ptab_found = 1;
+                _kernel_ptabs_paddr[vspace_id] = vobj[vobj_id].paddr;
+                _kernel_ptabs_vaddr[vspace_id] = vobj[vobj_id].vaddr;
+
+#if INIT_DEBUG_CTX
+_puts("[INIT]   PTAB address = "); 
+_putw(_kernel_ptabs_paddr[vspace_id]); 
+_puts("\n");
+#endif
+            }
+
+        }
+
+        if( !ptab_found )
+        {
+            _puts("\n[INIT ERROR] Missing PTAB for vspace ");
+            _putw( vspace_id );
+            _exit();
+        }
+    }
+        
+    _puts("\n[INIT] Ptabss initialisation completed at cycle : ");
+    _putw( _proctime() );
+    _puts("\n");
+
+} // end kernel_ptabs_init()
+
+///////////////////////////////////////////////////////////////////////////////
+// This function initializes all private vobjs defined in the vspaces,
+// such as mwmr channels, barriers and locks, depending on the vobj type. 
+// (Most of the vobjs are not known, and not initialised by the compiler).
+///////////////////////////////////////////////////////////////////////////////
+in_kinit void _kernel_vobjs_init()
+{
+    mapping_header_t*   header  = (mapping_header_t*)&seg_mapping_base;  
+    mapping_vspace_t*   vspace  = _get_vspace_base( header );     
+    mapping_vobj_t*     vobj    = _get_vobj_base( header );
+
+    unsigned int        vspace_id;  
+    unsigned int        vobj_id;
+
+    // loop on the vspaces 
+    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
+    {
+        char ptab_found = 0;
+
+#if INIT_DEBUG_CTX
+_puts("[INIT] --- vobjs initialisation in vspace "); 
+_puts(vspace[vspace_id].name);
+_puts("\n");
+#endif
+        // loop on the vobjs and get the ptpr
+	    for(vobj_id= vspace[vspace_id].vobj_offset; 
+			vobj_id < (vspace[vspace_id].vobj_offset+ vspace[vspace_id].vobjs);
+			vobj_id++)
+	    {
+            if(vobj[vobj_id].type == VOBJ_TYPE_PTAB)
+            {
+                if( ptab_found )
+                {
+                    _puts("\n[INIT ERROR] Only one PTAB for by vspace ");
+                    _putw( vspace_id );
+                    _exit();
+                }
+
+                ptab_found = 1;
+                _kernel_ptabs_paddr[vspace_id] = vobj[vobj_id].paddr;
+                _kernel_ptabs_vaddr[vspace_id] = vobj[vobj_id].vaddr;
+
+#if INIT_DEBUG_CTX
+_puts("[INIT]   PTAB address = "); 
+_putw(_kernel_ptabs_paddr[vspace_id]); 
+_puts("\n");
+#endif
+            }
+
+        }
+
+        if( !ptab_found )
+        {
+            _puts("\n[INIT ERROR] Missing PTAB for vspace ");
+            _putw( vspace_id );
+            _exit();
+        }
+        
+        /** Set the current vspace ptpr to initialise the vobjs */
+		_set_ptpr(vspace_id);
+
+        // loop on the vobjs and get the ptpr
+	    for(vobj_id= vspace[vspace_id].vobj_offset; 
+			vobj_id < (vspace[vspace_id].vobj_offset+ vspace[vspace_id].vobjs);
+			vobj_id++)
+	    {
+            switch( vobj[vobj_id].type )
+            {
+                case VOBJ_TYPE_PTAB:	// initialise page table pointers array
+                {
+                    break;//already handled
+                }
+                case VOBJ_TYPE_MWMR:	// storage capacity is (vobj.length/4 - 5) words
+		        {
+                    mwmr_channel_t* mwmr = (mwmr_channel_t*)(vobj[vobj_id].vaddr);
+                    mwmr->ptw   = 0;
+                    mwmr->ptr   = 0;
+                    mwmr->sts   = 0;
+                    mwmr->depth = (vobj[vobj_id].length>>2) - 5;
+                    mwmr->width = vobj[vobj_id].init;
+                    mwmr->lock  = 0;
+#if INIT_DEBUG_CTX
+_puts("[INIT]   MWMR channel ");
+_puts( vobj->name);
+_puts(" / depth = ");
+_putw( mwmr->depth );
+_puts("\n");
+#endif
+                    break;
+                }
+                case VOBJ_TYPE_ELF:		// initialisation done by the loader 
+                {
+
+#if INIT_DEBUG_CTX
+_puts("[INIT]   ELF section "); 
+_puts( vobj->name);
+_puts(" / length = ");
+_putw( vobj->length ); 
+_puts("\n");
+#endif
+                     break;
+                }
+                case VOBJ_TYPE_BARRIER:	// init is the number of participants
+                {
+                    giet_barrier_t* barrier = (giet_barrier_t*)(vobj[vobj_id].vaddr);
+                    barrier->count = 0;
+                    barrier->init  = vobj[vobj_id].init;
+#if INIT_DEBUG_CTX
+_puts("   BARRIER "); 
+_puts( vobj->name);
+_puts(" / init_value = ");
+_putw( barrier->init );
+_puts("\n");
+#endif
+                    break;
+                }
+                case VOBJ_TYPE_LOCK:	// init is "not taken"
+                {
+                    unsigned int* lock = (unsigned int*)(vobj[vobj_id].vaddr);
+                    *lock = 0;
+#if INIT_DEBUG_CTX
+_puts("   LOCK "); 
+_puts( vobj->name);
+_puts("\n");
+#endif
+                    break;
+                }
+                case VOBJ_TYPE_BUFFER:	// nothing to do
+                {
+
+#if INIT_DEBUG_CTX
+_puts("   BUFFER "); 
+_puts( vobj->name);
+_puts(" / length = ");
+_putw( vobj->length ); 
+_puts("\n");
+#endif
+                    break;
+                }
+                default:
+                {
+                    _puts("\n[INIT ERROR] illegal vobj of name ");
+                    _puts(vobj->name);
+                    _puts(" / in vspace = ");
+                    _puts(vobj->name);
+                    _puts("\n ");
+                    _exit();
+                }
+            } // end switch type
+        } // end loop on vobjs
+    } // end loop on vspaces
+
+    _puts("\n[INIT] Vobjs initialisation completed at cycle : ");
+    _putw( _proctime() );
+    _puts("\n");
+
+} // end kernel_vobjs_init()
 
 ///////////////////////////////////////////////////////////////////////////////
@@ -181,4 +417,6 @@
     mapping_vobj_t*     vobj   = _get_vobj_base( header );
 
+    /** Set the current vspace ptpr before acessing the memory */
+    _set_ptpr(vspace_id);
     
     // values to be initialised in task context
@@ -291,142 +529,4 @@
 
 } // end _task_map()
-
-///////////////////////////////////////////////////////////////////////////////
-// This function initializes all private vobjs defined in the vspaces,
-// such as mwmr channels, barriers and locks, depending on the vobj type. 
-// (Most of the vobjs are not known, and not initialised by the compiler).
-// This function initialises the _kernel_ptabs_paddr[] array indexed by the vspace_id,
-// and containing the base addresses of all page tables. 
-// This _kernel_ptabs_paddr[] array is used to initialise the task contexts.
-///////////////////////////////////////////////////////////////////////////////
-in_kinit void _kernel_vobjs_init()
-{
-    mapping_header_t*   header  = (mapping_header_t*)&seg_mapping_base;  
-    mapping_vspace_t*   vspace  = _get_vspace_base( header );     
-    mapping_vobj_t*     vobj    = _get_vobj_base( header );
-
-    unsigned int        vspace_id;  
-    unsigned int        vobj_id;
-
-    // loop on the vspaces 
-    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
-    {
-        char ptab_found = 0;
-
-#if INIT_DEBUG_CTX
-_puts("[INIT] --- vobjs initialisation in vspace "); 
-_puts(vspace[vspace_id].name);
-_puts("\n");
-#endif
-        // loop on the vobjs
-	    for(vobj_id= vspace[vspace_id].vobj_offset; 
-			vobj_id < (vspace[vspace_id].vobj_offset+ vspace[vspace_id].vobjs);
-			vobj_id++)
-	    {
-            switch( vobj[vobj_id].type )
-            {
-                case VOBJ_TYPE_PTAB:	// initialise page table pointers array
-                {
-                    ptab_found = 1;
-                    _kernel_ptabs_paddr[vspace_id] = vobj[vobj_id].paddr;
-                    _kernel_ptabs_vaddr[vspace_id] = vobj[vobj_id].vaddr;
-
-#if INIT_DEBUG_CTX
-_puts("[INIT]   PTAB address = "); 
-_putw(_kernel_ptabs_paddr[vspace_id]); 
-_puts("\n");
-#endif
-                    break;
-                }
-                case VOBJ_TYPE_MWMR:	// storage capacity is (vobj.length/4 - 5) words
-		        {
-                    mwmr_channel_t* mwmr = (mwmr_channel_t*)(vobj[vobj_id].vaddr);
-                    mwmr->ptw   = 0;
-                    mwmr->ptr   = 0;
-                    mwmr->sts   = 0;
-                    mwmr->depth = (vobj[vobj_id].length>>2) - 5;
-                    mwmr->lock  = 0;
-#if INIT_DEBUG_CTX
-_puts("[INIT]   MWMR channel ");
-_puts( vobj->name);
-_puts(" / depth = ");
-_putw( mwmr->depth );
-_puts("\n");
-#endif
-                    break;
-                }
-                case VOBJ_TYPE_ELF:		// initialisation done by the loader 
-                {
-
-#if INIT_DEBUG_CTX
-_puts("[INIT]   ELF section "); 
-_puts( vobj->name);
-_puts(" / length = ");
-_putw( vobj->length ); 
-_puts("\n");
-#endif
-                     break;
-                }
-                case VOBJ_TYPE_BARRIER:	// init is the number of participants
-                {
-                    giet_barrier_t* barrier = (giet_barrier_t*)(vobj[vobj_id].vaddr);
-                    barrier->count = 0;
-                    barrier->init  = vobj[vobj_id].init;
-#if INIT_DEBUG_CTX
-_puts("   BARRIER "); 
-_puts( vobj->name);
-_puts(" / init_value = ");
-_putw( barrier->init );
-_puts("\n");
-#endif
-                    break;
-                }
-                case VOBJ_TYPE_LOCK:	// init is "not taken"
-                {
-                    unsigned int* lock = (unsigned int*)(vobj[vobj_id].vaddr);
-                    *lock = 0;
-#if INIT_DEBUG_CTX
-_puts("   LOCK "); 
-_puts( vobj->name);
-_puts("\n");
-#endif
-                    break;
-                }
-                case VOBJ_TYPE_BUFFER:	// nothing to do
-                {
-
-#if INIT_DEBUG_CTX
-_puts("   BUFFER "); 
-_puts( vobj->name);
-_puts(" / length = ");
-_putw( vobj->length ); 
-_puts("\n");
-#endif
-                    break;
-                }
-                default:
-                {
-                    _puts("\n[INIT ERROR] illegal vobj of name ");
-                    _puts(vobj->name);
-                    _puts(" / in vspace = ");
-                    _puts(vobj->name);
-                    _puts("\n ");
-                    _exit();
-                }
-            } // end switch type
-        } // end loop on vobjs
-        if( !ptab_found )
-        {
-            _puts("\n[INIT ERROR] Missing PTAB for vspace ");
-            _putw( vspace_id );
-            _exit();
-        }
-    } // end loop on vspaces
-
-    _puts("\n[INIT] Vobjs initialisation completed at cycle : ");
-    _putw( _proctime() );
-    _puts("\n");
-
-} // end _vobjs_init()
 
 ///////////////////////////////////////////////////////////////////////////////