Index: soft/giet_vm/sys/kernel_init.c
===================================================================
--- soft/giet_vm/sys/kernel_init.c	(revision 166)
+++ soft/giet_vm/sys/kernel_init.c	(revision 167)
@@ -31,9 +31,17 @@
  
 ///////////////////////////////////////////////////////////////////////////////////
+// array of pointers on the page tables 
+// (both physical and virtual addresses)
+///////////////////////////////////////////////////////////////////////////////////
+
+__attribute__((section (".kdata"))) unsigned int _kernel_ptabs_paddr[GIET_NB_VSPACE_MAX]; 
+__attribute__((section (".kdata"))) unsigned int _kernel_ptabs_vaddr[GIET_NB_VSPACE_MAX]; 
+
+///////////////////////////////////////////////////////////////////////////////////
 // declarations required to avoid forward references
 ///////////////////////////////////////////////////////////////////////////////////
 
-void    _kernel_vobjs_init(unsigned int*);
-void    _kernel_tasks_init(unsigned int*);
+void    _kernel_vobjs_init(void);
+void    _kernel_tasks_init(void);
 void    _kernel_peripherals_init(void);
 void    _kernel_interrupt_vector_init(void);
@@ -45,7 +53,4 @@
 in_kinit void _kernel_init()
 {
-    // array of pointers on the page tables (used for task context initialisation)
-    unsigned int	kernel_ptabs[GIET_NB_VSPACE_MAX]; 
-
     // values to be written in registers
     unsigned int	sp_value;
@@ -59,6 +64,6 @@
     if ( pid == 0 )
     {
-        _kernel_vobjs_init(kernel_ptabs);
-        _kernel_tasks_init(kernel_ptabs);
+        _kernel_vobjs_init();
+        _kernel_tasks_init();
         _kernel_interrupt_vector_init();
         _kernel_peripherals_init();
@@ -163,10 +168,10 @@
 // - ptpr   page table base address / 8K
 // - mode   mmu_mode = 0xF (TLBs and caches activated)
+// - ptab   page table virtual address 
 ////////////////////////////////////////////////////////////////////////////////
 in_kinit void _task_map( unsigned int   task_id,    // global index
 				         unsigned int   vspace_id,  // global index
                          unsigned int   tty_id,		// TTY index
-                         unsigned int   fb_id, 		// FB index
-                         unsigned int   pt_base )   // page table base adddress
+                         unsigned int   fbdma_id )  // FBDMA index
 {
     mapping_header_t*   header = (mapping_header_t*)&seg_mapping_base;  
@@ -176,17 +181,18 @@
     mapping_vobj_t*     vobj   = _get_vobj_base( header );
 
+    
     // values to be initialised in task context
-    unsigned int		ra = (unsigned int)&_eret;
+    unsigned int		ra   = (unsigned int)&_eret;
     unsigned int		sr   = 0x0000FF13; 
     unsigned int		tty  = tty_id; 
-    unsigned int		fb   = fb_id;	 
-    unsigned int		ptpr = pt_base >> 13;
+    unsigned int		fb   = fbdma_id;	 
+    unsigned int		ptpr = _kernel_ptabs_paddr[vspace_id] >> 13;
+    unsigned int		ptab = _kernel_ptabs_vaddr[vspace_id];
     unsigned int		mode = 0xF;
     unsigned int		sp;
     unsigned int		epc;	 
 
-    // compute epc value
-    // Get the (virtual) base address of the start_vector that
-    // contains the start addresses for all tasks defined in a vspace.
+    // EPC : Get the (virtual) base address of the start_vector containing
+    // the start addresses for all tasks defined in a vspace.
     mapping_vobj_t* vobj_data = &vobj[vspace[vspace_id].vobj_offset + 
                                       vspace[vspace_id].start_offset]; 
@@ -194,6 +200,5 @@
     epc  = start_vector[task[task_id].startid];
 
-    // compute sp value
-    // Get the vobj containing the stack 
+    // SP :  Get the vobj containing the stack 
     unsigned int vobj_id = task[task_id].vobjlocid + vspace[vspace_id].vobj_offset;
     sp = vobj[vobj_id].vaddr + vobj[vobj_id].length;
@@ -220,11 +225,12 @@
     _scheduler[proc_id].context[ltid][CTX_RA_ID]    = ra;
     _scheduler[proc_id].context[ltid][CTX_EPC_ID]   = epc;
+    _scheduler[proc_id].context[ltid][CTX_PTPR_ID]  = ptpr;
+    _scheduler[proc_id].context[ltid][CTX_MODE_ID]  = mode;
     _scheduler[proc_id].context[ltid][CTX_TTY_ID]   = tty;
 	_scheduler[proc_id].context[ltid][CTX_FBDMA_ID] = fb;
-    _scheduler[proc_id].context[ltid][CTX_PTPR_ID]  = ptpr;
-    _scheduler[proc_id].context[ltid][CTX_MODE_ID]  = mode;
+    _scheduler[proc_id].context[ltid][CTX_PTAB_ID]  = ptab;
     _scheduler[proc_id].context[ltid][CTX_TASK_ID]  = task_id;
     
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("Task ");
 _puts( task[task_id].name );
@@ -259,4 +265,10 @@
 _puts("\n");
 
+_puts("  - PTPR        = ");
+_putw( ptpr<<13 );
+_puts("  saved at ");
+_putw( (unsigned int)&_scheduler[proc_id].context[ltid][CTX_PTPR_ID] );
+_puts("\n");
+
 _puts("  - TTY         = ");
 _putw( tty );
@@ -271,8 +283,8 @@
 _puts("\n");
 
-_puts("  - PTPR        = ");
-_putw( ptpr<<13 );
-_puts("  saved at ");
-_putw( (unsigned int)&_scheduler[proc_id].context[ltid][CTX_PTPR_ID] );
+_puts("  - PTAB        = ");
+_putw( ptab );
+_puts("  saved at ");
+_putw( (unsigned int)&_scheduler[proc_id].context[ltid][CTX_PTAB_ID] );
 _puts("\n");
 #endif
@@ -284,9 +296,9 @@
 // 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[] array indexed by the vspace_id,
-// and containint the base addresses of all page tables. 
-// This kernel_ptabs[] array is used to initialise the task contexts.
+// 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( unsigned int* kernel_ptabs )
+in_kinit void _kernel_vobjs_init()
 {
     mapping_header_t*   header  = (mapping_header_t*)&seg_mapping_base;  
@@ -302,5 +314,5 @@
         char ptab_found = 0;
 
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("[INIT] --- vobjs initialisation in vspace "); 
 _puts(vspace[vspace_id].name);
@@ -317,9 +329,10 @@
                 {
                     ptab_found = 1;
-                    kernel_ptabs[vspace_id] = vobj[vobj_id].paddr;
-
-#if INIT_DEBUG
+                    _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[vspace_id]); 
+_putw(_kernel_ptabs_paddr[vspace_id]); 
 _puts("\n");
 #endif
@@ -334,5 +347,5 @@
                     mwmr->depth = (vobj[vobj_id].length>>2) - 5;
                     mwmr->lock  = 0;
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("[INIT]   MWMR channel ");
 _puts( vobj->name);
@@ -346,5 +359,5 @@
                 {
 
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("[INIT]   ELF section "); 
 _puts( vobj->name);
@@ -360,5 +373,5 @@
                     barrier->count = 0;
                     barrier->init  = vobj[vobj_id].init;
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("   BARRIER "); 
 _puts( vobj->name);
@@ -373,5 +386,5 @@
                     unsigned int* lock = (unsigned int*)(vobj[vobj_id].vaddr);
                     *lock = 0;
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("   LOCK "); 
 _puts( vobj->name);
@@ -383,5 +396,5 @@
                 {
 
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("   BUFFER "); 
 _puts( vobj->name);
@@ -425,5 +438,5 @@
 // TTY[0] is reserved for the kernel.
 ///////////////////////////////////////////////////////////////////////////////
-in_kinit void _kernel_tasks_init(unsigned int* ptabs)
+in_kinit void _kernel_tasks_init()
 {
     mapping_header_t*   header  = (mapping_header_t*)&seg_mapping_base;  
@@ -461,5 +474,5 @@
     {
 
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 _puts("\n[INIT] mapping tasks in vspace ");
 _puts(vspace[vspace_id].name);
@@ -486,6 +499,5 @@
                        vspace_id,			// vspace index
                        tty_id,				// global tty index
-                       fb_id,				// global fbdma index
-                       ptabs[vspace_id] );	// page table pointer
+                       fb_id );				// global fbdma index
         } // end loop on tasks
     } // end oop on vspaces
@@ -495,5 +507,5 @@
     _puts("\n");
 
-#if INIT_DEBUG
+#if INIT_DEBUG_CTX
 for ( cluster_id = 0 ; cluster_id < header->clusters ; cluster_id++ )
 {
@@ -540,5 +552,4 @@
     {
         unsigned int*	iob_address = (unsigned int*)&seg_iob_base;
-        unsigned int	icu_address = (unsigned int)&seg_icu_base;
 
         // define IPI address mapping the IOC interrupt ...TODO...
