Index: /soft/giet_vm/boot/boot.ld
===================================================================
--- /soft/giet_vm/boot/boot.ld	(revision 166)
+++ /soft/giet_vm/boot/boot.ld	(revision 167)
@@ -12,5 +12,6 @@
 seg_mapping_base      	= 0xBFC0C000;	/* boot mapping_info */
 
-seg_kernel_init_base    = 0x80030000;	/* system init entry */ 
+seg_kernel_init_base    = 0x80090000;	/* system init entry */ 
+
 seg_tty_base        	= 0x90000000;   /* TTY device: for debug purpose! */
 
Index: /soft/giet_vm/boot/boot_handler.c
===================================================================
--- /soft/giet_vm/boot/boot_handler.c	(revision 166)
+++ /soft/giet_vm/boot/boot_handler.c	(revision 167)
@@ -31,19 +31,20 @@
 // As most applications use only a limited number of segments, the number of PT2s 
 // actually used by a given virtual space is generally smaller than 2048, and is
-// defined in the MAPPING_INFO_BINARY data structure (using the length field). 
-// The value is calculated and put in _max_pt2 indexed by the vspace_id.
-// The physical alignment constraints, is ensured by the align flag in the MAPPING_INFO 
-// structure.
+// defined by the (GIET_NB_PT2_MAX) configuration parameter.
 // The max number of virtual spaces (GIET_NB_VSPACE_MAX) is a configuration parameter.
 //
-// Each page table (one page table per virtual space) is monolithic:
-// - a first 8K aligned PT1[2148] array, indexed by the (ix1) field of VPN. 
+// Each page table (one page table per virtual space) is monolithic, and
+// contains one PT1 and (GIET_NB_PT2_MAX) PT2s. The PT1 is addressed using the ix1 field
+// (11 bits) of the VPN, and the selected PT2 is addressed using the ix2 field (9 bits).
+// - PT1[2048] : a first 8K aligned array of unsigned int, indexed by the (ix1) field of VPN. 
+//   Each entry in the PT1 contains a 32 bits PTD. The MSB bit PTD[31] is 
+//   the PTD valid bit, and LSB bits PTD[19:0] are the 20 MSB bits of the physical base
+//   address of the selected PT2.
 //   The PT1 contains 2048 PTD of 4 bytes => 8K bytes.
-// - an aray of array PT2[1024][_max_pt2[vspace_id]], indexed by
-//   the (ix2) field of the VPN, and by the PT2 index (pt2_id).
-//   Each PT2 contains 512 PTE2 of 8bytes => 4Kbytes * _max_pt2[vspace_id]
-// The size of each page table is 8K + (_max_pt2[vspace_id])*4K bytes.
-// All page tables must be stored in the seg_kernel_pt segment (at address
-// seg_kernel_pt_base) 
+// - PT2[1024][GIET_NB_PT2_MAX] : an array of array of unsigned int. 
+//   Each PT2[1024] must be 4K aligned,  and each entry in a PT2 contains two unsigned int: 
+//   the first word contains the protection flags, and the second word contains the PPN.
+//   Each PT2 contains 512 PTE2 of 8bytes => 4K bytes.
+// The total size of a page table is finally = 8K + (GIET_NB_PT2_MAX)*4K bytes.
 ////////////////////////////////////////////////////////////////////////////////////
 
@@ -55,9 +56,12 @@
 #include <stdarg.h>
 
-
 #if !defined(GIET_NB_VSPACE_MAX) 
 # error The GIET_NB_VSPACE_MAX value must be defined in the 'giet_config.h' file !
 #endif
 
+#if !defined(GIET_NB_PT2_MAX) 
+# error The GIET_NB_PT2_MAX value must be defined in the 'giet_config.h' file !
+#endif
+
 ////////////////////////////////////////////////////////////////////////////
 //  Page Tables global variables
@@ -66,8 +70,4 @@
 // Next free PT2 index array
 unsigned int  _next_free_pt2[GIET_NB_VSPACE_MAX] =
-                         { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };
-
-// Max number of PT2 array
-unsigned int  _max_pt2[GIET_NB_VSPACE_MAX] =
                          { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };
 
@@ -439,5 +439,5 @@
 // allocation), this function checks a possible overflow of the PT2 array.
 //
-// The parametre global is a boolean taht indicate wether a global vseg is
+// The global parameter is a boolean indicating wether a global vseg is
 // being mapped.
 //////////////////////////////////////////////////////////////////////////////
@@ -445,6 +445,5 @@
                    unsigned int    vpn,           
                    unsigned int    flags,
-                   unsigned int    ppn,
-                   unsigned char   global )
+                   unsigned int    ppn )
 {
     unsigned int    ix1;
@@ -458,19 +457,9 @@
     ix2 = vpn  & 0x1FF;         //  9 bits
 
-        
-    unsigned int max_pt2   = _max_pt2[vspace_id];
-    if(max_pt2 == 0)
-    {
-        boot_puts("Unfound page table for vspace ");
-        boot_putw(vspace_id);
-        boot_puts("\n");
-        boot_exit();
-    }
-
-    page_table_t* pt    = (page_table_t *)_ptabs[vspace_id];
+    page_table_t* pt = (page_table_t *)_ptabs[vspace_id];
     if ( (pt->pt1[ix1] & PTE_V) == 0 )   // set a new PTD in PT1 
     {
         pt2_id = _next_free_pt2[vspace_id];
-        if ( pt2_id == max_pt2 )
+        if ( pt2_id == GIET_NB_PT2_MAX )
         {
             boot_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
@@ -557,6 +546,5 @@
                           vpn,
                           flags,
-                          ppn,
-                          0 );
+                          ppn );
             vpn++;
             ppn++;
@@ -593,6 +581,5 @@
                           vpn,
                           flags,
-                          ppn,
-                          1 );
+                          ppn );
             vpn++;
             ppn++;
@@ -616,7 +603,8 @@
 // This function compute the physical base address for a vseg
 // as specified in the mapping info data structure.
-// It updates the pbase field of the vseg.
-// It updates the page allocator (nextfreepage field of the pseg),
-// and checks a possible pseg overflow.
+// It updates the pbase and the length fields of the vseg.
+// It updates the pbase and vbase fields of all vobjs in the vseg.
+// It updates the next_base field of the pseg.
+// It checks a possible pseg overflow.
 // It is a global vseg if vspace_id = (-1) 
 ///////////////////////////////////////////////////////////////////////////
@@ -641,10 +629,17 @@
     else                                // unconstrained mapping
     {
-        vseg->pbase = pseg->base + (pseg->next_free_page<<12);
+        vseg->pbase = pseg->next_base;
+
+        // test alignment constraint
+        if ( vobj[vseg->vobj_offset].align )
+        {
+            vseg->pbase = align_to( vseg->pbase, vobj[vseg->vobj_offset].align );
+        }
     }
     
-    // loop on vobjs to computes the length of the vseg,
-    // initialise the vaddr and paddr fields of all vobjs,
-    // and initialise the page table pointers array 
+    // loop on vobjs to (1) computes the length of the vseg,
+    // (2) initialise the vaddr and paddr fields of all vobjs,
+    // (3) initialise the page table pointers array 
+
     cur_vaddr = vseg->vbase;
     cur_paddr = vseg->pbase;
@@ -659,5 +654,5 @@
         }
 
-        // set vaddr/paddr
+        // set vaddr/paddr for current vobj
         vobj[vobj_id].vaddr = cur_vaddr;        
         vobj[vobj_id].paddr = cur_paddr;  
@@ -667,8 +662,8 @@
         cur_paddr += vobj[vobj_id].length; 
 
-        // initialise _ptabs[] and _max_pt2[]
+        // initialise _ptabs[] if current vobj is a PTAB
         if ( vobj[vobj_id].type == VOBJ_TYPE_PTAB )
         {
-            if(vobj[vobj_id].length < (PT1_SIZE + PT2_SIZE) ) // max_pt2 >= 1
+            if(vobj[vobj_id].length < (PT1_SIZE + PT2_SIZE*GIET_NB_PT2_MAX) ) 
             {
                 boot_puts( "\n[BOOT ERROR] in boot_vseg_map() function: " );
@@ -684,20 +679,17 @@
                 boot_exit();
             }
-            _ptabs[vspace_id]   = (page_table_t*)vobj[vobj_id].paddr;
-            _max_pt2[vspace_id] = (vobj[vobj_id].length - PT1_SIZE) / PT2_SIZE;
-        }
-    } 
+            _ptabs[vspace_id] = (page_table_t*)vobj[vobj_id].paddr;
+        }
+    } // end for vobjs
     
     //set the vseg length
-    unsigned int plength = pseg->length;
-    unsigned int vlength = cur_paddr - vseg->pbase;
-    vseg->length = align_to(vlength, 12);
+    vseg->length = align_to( (cur_paddr - vseg->pbase), 12);
 
     // checking pseg overflow
     if ( (vseg->pbase < pseg->base) || 
-         ((vseg->pbase + vlength) > (pseg->base + plength)) )
+         ((vseg->pbase + vseg->length) > (pseg->base + pseg->length)) )
     {
         boot_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
-        boot_puts("impossible identity mapping for virtual segment: ");
+        boot_puts("impossible mapping for virtual segment: ");
         boot_puts( vseg->name ); 
         boot_puts("\n"); 
@@ -717,18 +709,13 @@
     }
 
-    // computes number of pages
-    pages = vseg->length >> 12;
-    if ( (vseg->length & 0xFFF) != 0 ) pages++;
-
-    // set the next free physical address
-    if ( vseg->ident != 0 )
-            ;            // nothing to do
-    else                                
-        pseg->next_free_page = pseg->next_free_page + pages;
+    // set the next_base field in vseg
+    if ( vseg->ident == 0 )
+        pseg->next_base = vseg->pbase + vseg->length;
 
 #if BOOT_DEBUG_PT
-boot_puts("- vseg ");
 boot_puts( vseg->name );
-boot_puts(" : vbase = ");
+boot_puts(" : len = ");
+boot_putw( vseg->length );
+boot_puts(" / vbase = ");
 boot_putw( vseg->vbase );
 boot_puts(" / pbase = ");
@@ -816,5 +803,5 @@
     for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
     {
-        pseg[pseg_id].next_free_page = 0;
+        pseg[pseg_id].next_base = pseg[pseg_id].base;
     }
 
@@ -860,6 +847,6 @@
 
 #if BOOT_DEBUG_PT
-boot_puts(">>> page table physical address = ");
-boot_putw((unsigned)_ptabs[vspace_id]);
+boot_puts("\n>>> page table physical address = ");
+boot_putw((unsigned int)_ptabs[vspace_id]);
 boot_puts("\n");
 #endif
Index: /soft/giet_vm/boot/boot_handler.h
===================================================================
--- /soft/giet_vm/boot/boot_handler.h	(revision 166)
+++ /soft/giet_vm/boot/boot_handler.h	(revision 167)
@@ -53,6 +53,6 @@
 typedef struct PageTable 
 {
-	unsigned int    pt1[2048];                    // PT1 (index is ix1)
-	unsigned int    pt2[GIET_NB_PT2_MAX][1024];   // PT2s (index is ix2)
+	unsigned int    pt1[PT1_SIZE];                    // PT1 (index is ix1)
+	unsigned int    pt2[GIET_NB_PT2_MAX][PT2_SIZE];   // PT2s (index is 2*ix2)
 } page_table_t;
 
Index: /soft/giet_vm/giet_config.h
===================================================================
--- /soft/giet_vm/giet_config.h	(revision 166)
+++ /soft/giet_vm/giet_config.h	(revision 167)
@@ -14,5 +14,5 @@
 #define BOOT_DEBUG_VIEW		0	    /* display the mapping_info on system TTY */
 #define BOOT_DEBUG_PT		0	    /* display the page tables after mapping */
-#define INIT_DEBUG			0	    /* display the task contexts after mapping */
+#define INIT_DEBUG_CTX		0	    /* display the task contexts after mapping */
 #define GIET_DEBUG_SWITCH	0	    /* Trace context switchs */
 
@@ -27,14 +27,14 @@
 #define NB_TIMERS		    4	    /* number of timers per cluster */
 #define NB_DMAS			    1	    /* total number of DMA channels */
-#define NB_TTYS			    7	    /* total number of TTY terminals */
+#define NB_TTYS			    8	    /* total number of TTY terminals */
 
 /* software parameters */
 
 #define GIET_NB_TASKS_MAX 	4	    /* max number of tasks per processor */
-#define GIET_NB_VSPACE_MAX	3	    /* max number of virtual spaces */
+#define GIET_NB_VSPACE_MAX	4	    /* max number of virtual spaces */
 #define GIET_NB_PT2_MAX  	16	    /* max number of level 2 page tables per vspace */
-#define GIET_TICK_VALUE	    65536   /* context switch period (number of cycles) */
+#define GIET_TICK_VALUE	    16384   /* context switch period (number of cycles) */
 #define GIET_IOMMU_ACTIVE   0		/* The IOMMU vspace is defined */
-#define GIET_IOMMU_CHANNELS 1		/* number of 2Mbytes segments in IOMMU vspace */
+
 #endif
 
Index: /soft/giet_vm/map.xml
===================================================================
--- /soft/giet_vm/map.xml	(revision 166)
+++ /soft/giet_vm/map.xml	(revision 167)
@@ -5,7 +5,7 @@
                 clusters = "1"
                 psegs    = "9"
-                ttys     = "7"
+                ttys     = "8"
                 fbs      = "0"
-                vspaces  = "3" 
+                vspaces  = "4" 
                 globals  = "13" >
 
@@ -30,17 +30,17 @@
                 <pseg    name   = "PSEG_TTY"
                          base   = "0x90000000" 
-                         length = "0x00000200" />
+                         length = "0x00001000" />
 
                 <pseg    name   = "PSEG_TIM" 
                          base   = "0x91000000" 
-                         length = "0x00000080" />
+                         length = "0x00001000" />
 
                 <pseg    name   = "PSEG_IOC" 
                          base   = "0x92000000" 
-                         length = "0x00000020" />
+                         length = "0x00001000" />
 
                 <pseg    name   = "PSEG_DMA" 
                          base   = "0x93000000" 
-                         length = "0x00000100" />
+                         length = "0x00001000" />
 
                 <pseg    name   = "PSEG_FBF" 
@@ -50,5 +50,5 @@
                 <pseg    name   = "PSEG_ICU" 
                          base   = "0x9F000000" 
-                         length = "0x00000100" />
+                         length = "0x00001000" />
         </psegset> 
 
@@ -105,10 +105,10 @@
     					<vobj   name	= "seg_kernel_data"
     							type	= "ELF"
-    							length  = "0x00010000" 
+    							length  = "0x00040000" 
     							binpath	= "build/sys.elf" />
 				</vseg>
 
                 <vseg   name      = "seg_kernel_uncdata"
-                        vbase     = "0x80020000" 
+                        vbase     = "0x80080000" 
                         mode      = "__W_"
                         psegname  = "PSEG_RAK"
@@ -121,5 +121,5 @@
 
                 <vseg   name      = "seg_kernel_init"
-                        vbase     = "0x80030000" 
+                        vbase     = "0x80090000" 
                         mode      = "CX__"
                         psegname  = "PSEG_RAK"
@@ -139,5 +139,5 @@
     					<vobj   name	= "tty"
 	    						type	= "PERI"
-		    					length  = "0x00000100" />
+		    					length  = "0x00001000" />
 				</vseg>
 
@@ -149,5 +149,5 @@
     					<vobj   name	= "timer"
 	    						type	= "PERI"
-		    					length  = "0x00000080" />
+		    					length  = "0x00001000" />
 				</vseg>
 
@@ -169,5 +169,5 @@
     					<vobj   name	= "dma"
 	    						type	= "PERI"
-		    					length  = "0x00000100" />
+		    					length  = "0x00001000" />
 				</vseg>
 
@@ -223,5 +223,5 @@
                                 <vobj   name	= "ptab_router"
                                         type	= "PTAB"
-                                        length  = "0x00010000" 
+                                        length  = "0x00012000" 
                                         align   = "13" />
                         </vseg>
@@ -333,5 +333,5 @@
                                 <vobj   name	= "ptab"
                                         type	= "PTAB"
-                                        length  = "0x00010000" 
+                                        length  = "0x00012000" 
                                         align   = "13" />
                         </vseg>
@@ -374,5 +374,5 @@
                                 <vobj   name	= "ptab"
                                         type	= "PTAB"
-                                        length  = "0x00010000" 
+                                        length  = "0x00012000" 
                                         align   = "13" />
                         </vseg>
@@ -404,4 +404,55 @@
                                 usetty    = "1" />
                 </vspace>
+
+                <vspace name      = "display" 
+                        startname = "seg_data_display" >
+
+                        <vseg   name      = "seg_data_display"
+                                vbase     = "0x00800000" 
+                                mode      = "C_WU"
+                                psegname  = "PSEG_RAU" >
+							    <vobj   name	= "seg_data_display"
+								    	type	= "ELF"
+									    length  = "0x00010000" 
+                                        binpath = "build/display.elf" />
+						</vseg>
+
+                        <vseg   name      = "seg_ptab_display"
+                                vbase     = "0x00300000" 
+                                mode      = "C___"
+                                psegname  = "PSEG_RAU" >
+                                <vobj   name	= "ptab"
+                                        type	= "PTAB"
+                                        length  = "0x00012000" 
+                                        align   = "13" />
+                        </vseg>
+
+                        <vseg   name      = "seg_code_display"
+                                vbase     = "0x00400000" 
+                                mode      = "CX_U"
+                                psegname  = "PSEG_RAU" >
+							    <vobj   name	= "seg_code_display"
+								    	type	= "ELF"
+									    length  = "0x00010000" 
+                                        binpath = "build/display.elf" />
+						</vseg>
+
+                        <vseg   name      = "seg_stack_display"
+                                vbase     = "0x00000000" 
+                                mode      = "C_WU"
+                                psegname  = "PSEG_RAU" >
+							    <vobj   name	= "stack_display"
+								    	type	= "BUFFER"
+									    length  = "0x00010000" />
+						</vseg>
+
+                        <task   name      = "main_display"
+                                clusterid = "0"
+                                proclocid = "3"
+                                stackname = "stack_display"
+                                startid   = "0" 
+                                usetty    = "1" />
+                </vspace>
+
           </vspaceset>
 </mapping_info>
Index: /soft/giet_vm/sys/ctx_handler.c
===================================================================
--- /soft/giet_vm/sys/ctx_handler.c	(revision 166)
+++ /soft/giet_vm/sys/ctx_handler.c	(revision 167)
@@ -15,17 +15,20 @@
 // It contains copies of processor registers, when the task is not running,
 // and some general informations associated to the task.
+//
 // - It contains GPR[i], generally stored in slot (i). $0, *26 & $27 are not saved.
 // - It contains HI & LO registers.
 // - It contains CP0 registers: EPC, SR, CR.
 // - It contains CP2 registers : PTPR and MODE.
-// - It contains the TTY index for the terminal allocated to the task.
-// ctx[0] <- SR   ctx[8] <- $8    ctx[16]<- $16   ctx[24]<- $24   ctx[32]<- EPC
-// ctx[1] <- $1   ctx[9] <- $9    ctx[17]<- $17   ctx[25]<- $25   ctx[33]<- CR
-// ctx[2] <- $2   ctx[10]<- $10   ctx[18]<- $18   ctx[26]<- LO    ctx[34]<- TTY
-// ctx[3] <- $3   ctx[11]<- $11   ctx[19]<- $19   ctx[27]<- HI    ctx[35]<- PTPR
-// ctx[4] <- $4   ctx[12]<- $12   ctx[20]<- $20   ctx[28]<- $28   ctx[36]<- MODE
-// ctx[5] <- $5   ctx[13]<- $13   ctx[21]<- $21   ctx[29]<- $29   ctx[37]<- FBDMA
-// ctx[6] <- $6   ctx[14]<- $14   ctx[22]<- $22   ctx[30]<- $30   ctx[38]<- reserved
-// ctx[7] <- $7   ctx[15]<- $15   ctx[23]<- $23   ctx[31]<- $31   ctx[39]<- reserved
+// - It contains the TTY global index, the FBDMA global index, the virtual base 
+//   address of the page table (PTAB), and the task global index (TASK).
+//
+// ctx[0]<- SR|ctx[8] <- $8 |ctx[16]<- $16|ctx[24]<- $24|ctx[32]<- EPC |ctx[40]<- TTY
+// ctx[1]<- $1|ctx[9] <- $9 |ctx[17]<- $17|ctx[25]<- $25|ctx[33]<- CR  |ctx[41]<- FBDMA
+// ctx[2]<- $2|ctx[10]<- $10|ctx[18]<- $18|ctx[26]<- LO |ctx[34]<- *** |ctx[42]<- PTAB
+// ctx[3]<- $3|ctx[11]<- $11|ctx[19]<- $19|ctx[27]<- HI |ctx[35]<- PTPR|ctx[43]<- TASK
+// ctx[4]<- $4|ctx[12]<- $12|ctx[20]<- $20|ctx[28]<- $28|ctx[36]<- MODE|ctx[44]<- ***
+// ctx[5]<- $5|ctx[13]<- $13|ctx[21]<- $21|ctx[29]<- SP |ctx[37]<- *** |ctx[45]<- ***
+// ctx[6]<- $6|ctx[14]<- $14|ctx[22]<- $22|ctx[30]<- $30|ctx[38]<- *** |ctx[46]<- ***
+// ctx[7]<- $7|ctx[15]<- $15|ctx[23]<- $23|ctx[31]<- RA |ctx[39]<- *** |ctx[47]<- ***
 /////////////////////////////////////////////////////////////////////////////////////
 
@@ -40,8 +43,8 @@
 
 /////////////////////////////////////////////////////////////////////////////////
-//	Global variables
+//	Global variables : array of schedulers (one scheduler per processor)
 /////////////////////////////////////////////////////////////////////////////////
 
-static_scheduler_t _scheduler[NB_CLUSTERS * NB_PROCS];
+__attribute__((section (".kdata"))) static_scheduler_t _scheduler[NB_CLUSTERS * NB_PROCS];
 
 /////////////////////////////////////////////////////////////////////////////////
@@ -64,7 +67,6 @@
     unsigned int *next_context;
 
-    unsigned int pid   = _procid();
-    unsigned int time  = _proctime();
-    unsigned int tasks = _scheduler[pid].tasks;
+    unsigned int proc_id   = _procid();
+    unsigned int tasks     = _scheduler[proc_id].tasks;
 
     // return if only one task  */
@@ -72,6 +74,6 @@
  
     // compute the task context base address for the current task
-    curr_task_id = _scheduler[pid].current;
-    curr_context = &(_scheduler[pid].context[curr_task_id][0]);
+    curr_task_id = _scheduler[proc_id].current;
+    curr_context = &(_scheduler[proc_id].context[curr_task_id][0]);
     
     // select the next task using a round-robin scheduling policy
@@ -79,12 +81,12 @@
     
     // compute the task context base address for the next task
-    next_context = &(_scheduler[pid].context[next_task_id][0]);
+    next_context = &(_scheduler[proc_id].context[next_task_id][0]);
 
 #if GIET_DEBUG_SWITCH
 _get_lock( &_tty_put_lock );
 _puts( "\n[GIET] Context switch for processor ");
-_putw( pid );
+_putw( proc_id );
 _puts( " at cycle ");
-_putw( time );
+_putw( _proctime() );
 _puts("\n");
 _puts( " - tasks        = ");
@@ -101,5 +103,5 @@
 
     //  update the scheduler state, and makes the task switch
-    _scheduler[pid].current = next_task_id;
+    _scheduler[proc_id].current = next_task_id;
     _task_switch( curr_context, next_context );
 
Index: /soft/giet_vm/sys/ctx_handler.h
===================================================================
--- /soft/giet_vm/sys/ctx_handler.h	(revision 166)
+++ /soft/giet_vm/sys/ctx_handler.h	(revision 167)
@@ -15,4 +15,23 @@
 } static_scheduler_t;
 
+/////////////////////////////////////////////////////////////////////////////////
+//	Definition of the task context slots indexes
+/////////////////////////////////////////////////////////////////////////////////
+
+#define CTX_SR_ID		0
+#define CTX_SP_ID		29
+#define CTX_RA_ID		31
+
+#define CTX_EPC_ID		32
+#define CTX_CR_ID		33
+#define CTX_PTPR_ID		35
+#define CTX_MODE_ID		36
+
+#define CTX_TTY_ID		40
+#define CTX_FBDMA_ID	41
+#define CTX_PTAB_ID		42
+#define CTX_TASK_ID		43
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // 	Prototype of the context switch function
Index: /soft/giet_vm/sys/drivers.c
===================================================================
--- /soft/giet_vm/sys/drivers.c	(revision 166)
+++ /soft/giet_vm/sys/drivers.c	(revision 167)
@@ -491,14 +491,16 @@
                           unsigned int 	count )
 {
-    unsigned int	user_vpn_min;
-    unsigned int	user_vpn_max;
-    unsigned int	vpn;			// virtual page number in user space
-    unsigned int	ppn;			// physical page number
-    unsigned int	flags;			// page protection flags
-    unsigned int	ix2;			// Page index (for IOMMU page table)
-    unsigned int	addr;			// buffer address for IOC 
-    page_table_t*	user_ptp;		// user page table pointer
-    unsigned int	ko;				// bool returned by _v2p_translate()
-    unsigned int	ppn_first;		// first physical page number for user buffer
+    unsigned int		user_vpn_min;	// first virtuel page index in user space
+    unsigned int		user_vpn_max;	// last virtual page index in user space
+    unsigned int		vpn;			// current virtual page index in user space
+    unsigned int		ppn;			// physical page number
+    unsigned int		flags;			// page protection flags
+    unsigned int		ix2;			// page index in IOMMU PT1 page table
+    unsigned int		addr;			// buffer address for IOC peripheral
+    unsigned int		user_ptp;		// page table pointer in user space
+    unsigned int		ko;				// bool returned by _v2p_translate()
+    unsigned int		ppn_first;		// first physical page number for user buffer
+    unsigned int		ltid;			// current task local index
+    static_scheduler_t*	psched;			// pointer on the current task scheduler
         
     // check buffer alignment
@@ -509,6 +511,8 @@
     unsigned int	length       = count*block_size;
 
-    // get user space page table base address
-    user_ptp     = (page_table_t*)(_get_ptpr() << 13);
+    // get user space page table virtual address
+    psched   = &_scheduler[_procid()];
+    ltid     = psched->current;
+    user_ptp = psched->context[ltid][CTX_PTAB_ID];
     
     user_vpn_min = user_vaddr >> 12;
@@ -520,8 +524,8 @@
     {
         // get ppn and flags for each vpn
-        ko = _v2p_translate( user_ptp,	// user page table pointer
-                             vpn,		// virtual page number
-                             &ppn,		// physical page number
-                             &flags );	// protection flags
+        ko = _v2p_translate( (page_table_t*)user_ptp,
+                             vpn,
+                             &ppn,
+                             &flags );
 
         // check access rights
@@ -543,6 +547,4 @@
 					         ppn,				// Physical page number	
                              flags );			// Protection flags
-
-            // buffer base address for IOC with IOMMU
         }
         else			// no IOMMU : check that physical pages are contiguous
@@ -563,5 +565,5 @@
     // compute buffer base address for IOC depending on IOMMU activation
     if ( GIET_IOMMU_ACTIVE ) addr = (_ioc_iommu_ix1) << 21 | (user_vaddr & 0xFFF);
-    else                     addr = ppn_first | (user_vaddr & 0xFFF);
+    else                     addr = (ppn_first << 12) | (user_vaddr & 0xFFF);
 
     // get the lock on ioc device 
Index: /soft/giet_vm/sys/irq_handler.c
===================================================================
--- /soft/giet_vm/sys/irq_handler.c	(revision 166)
+++ /soft/giet_vm/sys/irq_handler.c	(revision 167)
@@ -23,5 +23,6 @@
 ///////////////////////////////////////////////////////////////////////////////////
 
-_isr_func_t _interrupt_vector[32] = { [0 ... 31] = &_isr_default };
+__attribute__((section (".kdata"))) _isr_func_t _interrupt_vector[32] = 
+                                                  { [0 ... 31] = &_isr_default };
 
 ///////////////////////////////////////////////////////////////////////////////////
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...
Index: /soft/giet_vm/sys/mips32_registers.h
===================================================================
--- /soft/giet_vm/sys/mips32_registers.h	(revision 166)
+++ /soft/giet_vm/sys/mips32_registers.h	(revision 167)
@@ -78,16 +78,3 @@
 #define CP2_DCACHE_INVAL_PA 	$20 
 
-/* Context index */
-
-#define CTX_SR_ID		0
-#define CTX_SP_ID		29
-#define CTX_RA_ID		31
-#define CTX_EPC_ID		32
-#define CTX_TTY_ID		34
-#define CTX_PTPR_ID		35
-#define CTX_MODE_ID		36
-#define CTX_FBDMA_ID	37
-#define CTX_TASK_ID		63
-
-
 #endif
Index: /soft/giet_vm/sys/sys.ld
===================================================================
--- /soft/giet_vm/sys/sys.ld	(revision 166)
+++ /soft/giet_vm/sys/sys.ld	(revision 167)
@@ -3,11 +3,11 @@
 *****************************************************************************/
 
-/* The vsegs used by the system are replicated in all virtual spaces 
+/* The vsegs used by the system are mapped in all virtual spaces 
    They can be identity mapping... or not */
 
 seg_kernel_code_base    = 0x80000000;	/* system code */
 seg_kernel_data_base    = 0x80010000;	/* system cacheable data */
-seg_kernel_uncdata_base = 0x80020000;	/* system uncacheable data */
-seg_kernel_init_base    = 0x80030000;	/* system page table */ 
+seg_kernel_uncdata_base = 0x80080000;	/* system uncacheable data */
+seg_kernel_init_base    = 0x80090000;	/* system page table */ 
 seg_mapping_base  	    = 0xBFC0C000;	/* boot mapping_info */
 
@@ -16,12 +16,12 @@
    must be defined, even if the peripherals are not used in the architecture */
 
-seg_tty_base      	= 0x90000000;   /* TTY device */
-seg_timer_base    	= 0x91000000;   /* Timer device */
-seg_ioc_base      	= 0x92000000;   /* Block device */
-seg_dma_base      	= 0x93000000;   /* DMA device */
-seg_gcd_base      	= 0x95000000;   /* GCD device */
-seg_fb_base       	= 0x96000000;   /* FrameBuffer device */
-seg_icu_base      	= 0x9F000000;   /* ICU or XICU device */
-seg_iob_base      	= 0x9E000000;   /* IOB device */
+seg_tty_base      	    = 0x90000000;   /* TTY device */
+seg_timer_base    	    = 0x91000000;   /* Timer device */
+seg_ioc_base      	    = 0x92000000;   /* Block device */
+seg_dma_base      	    = 0x93000000;   /* DMA device */
+seg_gcd_base      	    = 0x95000000;   /* GCD device */
+seg_fb_base       	    = 0x96000000;   /* FrameBuffer device */
+seg_iob_base      	    = 0x9E000000;   /* IOB device */
+seg_icu_base      	    = 0x9F000000;   /* ICU or XICU device */
 
 /*
@@ -40,14 +40,12 @@
     seg_kernel_data : 
     {
+        *(.iommu)
+        *(.kdata)
         *(.rodata)
-        /* . = ALIGN(4); */
         *(.rodata.*)
-        /* . = ALIGN(4); */
         *(.data)
-        /* . = ALIGN(4); */
         *(.lit8)
         *(.lit4)
         *(.sdata)
-        /* . = ALIGN(4); */
         *(.bss)
         *(COMMON)
Index: /soft/giet_vm/sys/sys_handler.c
===================================================================
--- /soft/giet_vm/sys/sys_handler.c	(revision 166)
+++ /soft/giet_vm/sys/sys_handler.c	(revision 167)
@@ -75,4 +75,5 @@
 void _exit()
 {
+    unsigned int date    = _proctime();
     unsigned int proc_id = _procid();
     unsigned int task_id = _scheduler[proc_id].current;
@@ -83,4 +84,6 @@
     _puts(" on processor ");
     _putw( proc_id );
+    _puts(" at cycle ");
+    _putw( date );
     _puts("\n\n");
 
Index: /soft/giet_vm/sys/vm_handler.c
===================================================================
--- /soft/giet_vm/sys/vm_handler.c	(revision 167)
+++ /soft/giet_vm/sys/vm_handler.c	(revision 167)
@@ -0,0 +1,150 @@
+///////////////////////////////////////////////////////////////////////////////////
+// File     : vm_handler.c
+// Date     : 01/07/2012
+// Author   : alain greiner
+// Copyright (c) UPMC-LIP6
+///////////////////////////////////////////////////////////////////////////////////
+// The vm_handler.c and vm_handler.h files are part ot the GIET nano kernel.
+// They contains the kernel data structures and functions used to dynamically
+// handle the iommu page table.
+// 
+// TODO : We must transfer here the functions used to statically build
+// the page tables associated to the various vspaces (now in boot_handler.c)
+// 
+///////////////////////////////////////////////////////////////////////////////////
+
+#include <vm_handler.h>
+#include <sys_handler.h>
+#include <common.h>
+#include <giet_config.h>
+
+/////////////////////////////////////////////////////////////////////////////
+// 	Global variable : IOMMU page table
+/////////////////////////////////////////////////////////////////////////////
+
+__attribute__((section (".iommu"))) page_table_t	_iommu_ptab;
+
+//////////////////////////////////////////////////////////////////////////////
+// _iommu_add_pte2()
+//////////////////////////////////////////////////////////////////////////////
+void _iommu_add_pte2( unsigned int	ix1,
+                      unsigned int	ix2,
+                      unsigned int	ppn,
+                      unsigned int	flags )
+{
+    unsigned int	ptba;
+    unsigned int*	pt_ppn;
+    unsigned int*	pt_flags;
+
+    // get pointer on iommu page table
+    page_table_t* pt = &_iommu_ptab;
+
+    // get ptba and update PT2
+    if ( (pt->pt1[ix1] & PTE_V) == 0 )
+    {
+        _puts("\n[GIET ERROR] in iommu_add_pte2 function\n");
+        _puts("the IOMMU PT1 entry is not mapped / ix1 = ");
+        _putw( ix1 );
+        _puts("\n");
+        _exit();
+    }
+    else
+    {
+        ptba      = pt->pt1[ix1] << 12;
+        pt_flags  = (unsigned int*)(ptba + 8*ix2);
+        pt_ppn    = (unsigned int*)(ptba + 8*ix2 + 4);
+        *pt_flags = flags;
+        *pt_ppn   = ppn;
+    }
+} // end _iommu_add_pte2()
+
+//////////////////////////////////////////////////////////////////////////////
+// _iommu_inval_pte2()
+//////////////////////////////////////////////////////////////////////////////
+void _iommu_inval_pte2( unsigned int	ix1,
+                        unsigned int	ix2 )
+{
+    unsigned int	ptba;
+    unsigned int*	pt_flags;
+
+    // get pointer on iommu page table
+    page_table_t* pt = &_iommu_ptab;
+
+    // get ptba and inval PTE2
+    if ( (pt->pt1[ix1] & PTE_V) == 0 )
+    {
+        _puts("\n[GIET ERROR] in iommu_inval_pte2 function\n");
+        _puts("the IOMMU PT1 entry is not mapped / ix1 = ");
+        _putw( ix1 );
+        _puts("\n");
+        _exit();
+    }
+    else
+    {
+        ptba      = pt->pt1[ix1] << 12;
+        pt_flags  = (unsigned int*)(ptba + 8*ix2);
+        *pt_flags = 0;
+    }   
+} // end _iommu_inval_pte2()
+
+//////////////////////////////////////////////////////////////////////////////
+// _v2p_translate()
+// Returns 0 if success, 1 if PTE1 or PTE2 unmapped
+//////////////////////////////////////////////////////////////////////////////
+unsigned int _v2p_translate( page_table_t*	pt,
+                             unsigned int	vpn,
+                             unsigned int*	ppn,		
+                             unsigned int*	flags )	 
+{
+    unsigned int    ptba;
+    unsigned int*   pte2;
+    unsigned int    flags_value;
+    unsigned int    ppn_value;
+
+    unsigned int    ix1 = vpn >> 9;
+    unsigned int    ix2 = vpn & 0x1FF;
+
+    // check PTE1 mapping
+    if ( (pt->pt1[ix1] & PTE_V) == 0 )
+    {
+        return 1;
+    }
+    else
+    {
+        // get physical addresses of pte2 
+        ptba = pt->pt1[ix1] << 12;
+        pte2 = (unsigned int*)(ptba + 8*ix2);
+
+        // gets ppn_value and flags_value, after temporary DTLB desactivation
+        asm volatile ( "li      $26, 0xB    \n"     /* DTLB unactivated */
+                       "mtc2    $26, $1     \n"
+                       "lw      %0,  0(%2)  \n"     /* read flags       */ 
+                       "lw      %1,  4(%2)  \n"     /* read ppn         */
+                       "li      $26, 0xF    \n" 
+                       "mtc2    $26, $1     \n"     /* DTLB activated   */
+                        :"=r"(flags_value), "=r"(ppn_value)
+                        :"r"(pte2)
+                        :"$26" );
+
+        // check PTE2 mapping
+        if ( (flags_value & PTE_V) == 0 )
+        {
+            return 1;
+        }
+
+        // set return values 
+        *ppn      = ppn_value;
+        *flags    = flags_value;
+    }
+    return 0;
+}	// end _v2p_translate()
+
+// Local Variables:
+// tab-width: 4
+// c-basic-offset: 4
+// c-file-offsets:((innamespace . 0)(inline-open . 0))
+// indent-tabs-mode: nil
+// End:
+
+// vim: filetype=cpp:expandtab:shiftwidth=4:tabstop=4:softtabstop=4
+
Index: /soft/giet_vm/sys/vm_handler.h
===================================================================
--- /soft/giet_vm/sys/vm_handler.h	(revision 167)
+++ /soft/giet_vm/sys/vm_handler.h	(revision 167)
@@ -0,0 +1,92 @@
+///////////////////////////////////////////////////////////////////////////////////
+// File     : vm_handler.h
+// Date     : 01/07/2012
+// Author   : alain greiner
+// Copyright (c) UPMC-LIP6
+///////////////////////////////////////////////////////////////////////////////////
+
+#ifndef     _VM_HANDLER_H_
+#define     _VM_HANDLER_H_
+
+#include    <giet_config.h>
+#include    <mapping_info.h>
+
+/////////////////////////////////////////////////////////////////////////////////////
+// Page Table sizes definition
+/////////////////////////////////////////////////////////////////////////////////////
+
+#define     PT1_SIZE    8192
+#define     PT2_SIZE    4096
+
+/////////////////////////////////////////////////////////////////////////////////////
+// PTE flags masks definition 
+/////////////////////////////////////////////////////////////////////////////////////
+
+#define     PTE_V       0x80000000
+#define     PTE_T       0x40000000
+#define     PTE_L       0x20000000
+#define     PTE_R       0x10000000
+#define     PTE_C       0x08000000
+#define     PTE_W       0x04000000
+#define     PTE_X       0x02000000
+#define     PTE_U       0x01000000
+#define     PTE_G       0x00800000
+#define     PTE_D       0x00400000
+
+/////////////////////////////////////////////////////////////////////////////////////
+// MMU error codes definition 
+/////////////////////////////////////////////////////////////////////////////////////
+
+#define	MMU_ERR_PT1_UNMAPPED         0x001 	// Page fault on Table1 (invalid PTE) 
+#define	MMU_ERR_PT2_UNMAPPED         0x002 	// Page fault on Table 2 (invalid PTE) 
+#define	MMU_ERR_PRIVILEGE_VIOLATION  0x004 	// Protected access in user mode 
+#define	MMU_ERR_WRITE_VIOLATION      0x008 	// Write access to a non write page 
+#define	MMU_ERR_EXEC_VIOLATION       0x010 	// Exec access to a non exec page 
+#define	MMU_ERR_UNDEFINED_XTN        0x020 	// Undefined external access address 
+#define	MMU_ERR_PT1_ILLEGAL_ACCESS   0x040 	// Bus Error in Table1 access 
+#define	MMU_ERR_PT2_ILLEGAL_ACCESS   0x080 	// Bus Error in Table2 access 
+#define	MMU_ERR_CACHE_ILLEGAL_ACCESS 0x100 	// Bus Error during the cache access 
+
+/////////////////////////////////////////////////////////////////////////////////////
+// Page table structure definition
+/////////////////////////////////////////////////////////////////////////////////////
+typedef struct PageTable 
+{
+	unsigned int    pt1[PT1_SIZE/4];                      // PT1 (index is ix1)
+	unsigned int    pt2[GIET_NB_PT2_MAX][PT2_SIZE/4];     // PT2s (index is 2*ix2)
+} page_table_t;
+
+
+////////////////////////////////////////////////////////////////////////////////////
+// Global variable
+////////////////////////////////////////////////////////////////////////////////////
+
+extern page_table_t _iommu_ptab;
+
+////////////////////////////////////////////////////////////////////////////////////
+// functions prototypes
+////////////////////////////////////////////////////////////////////////////////////
+
+void _iommu_add_pte2( unsigned int	ix1,
+                      unsigned int	ix2,
+                      unsigned int	ppn,
+                      unsigned int	flags );
+
+void _iommu_inval_pte2( unsigned int	ix1,
+                        unsigned int	ix2 );
+
+unsigned int _v2p_translate( page_table_t*	pt,
+                             unsigned int	vpn,
+                             unsigned int*	ppn,	
+                             unsigned int*	flags );
+
+#endif 
+
+// Local Variables:
+// tab-width: 4
+// c-basic-offset: 4
+// c-file-offsets:((innamespace . 0)(inline-open . 0))
+// indent-tabs-mode: nil
+// End:
+
+// vim: filetype=cpp:expandtab:shiftwidth=4:tabstop=4:softtabstop=4
Index: /soft/giet_vm/xml/mapping_info.h
===================================================================
--- /soft/giet_vm/xml/mapping_info.h	(revision 166)
+++ /soft/giet_vm/xml/mapping_info.h	(revision 167)
@@ -95,5 +95,5 @@
 	unsigned int    base;           // base address in physical space
 	unsigned int	length;         // size (bytes)
-    unsigned int    next_free_page; // physical page allocator
+    unsigned int    next_base;      // first free page base address
 } mapping_pseg_t;
 
Index: /soft/giet_vm/xml/xml_parser.c
===================================================================
--- /soft/giet_vm/xml/xml_parser.c	(revision 166)
+++ /soft/giet_vm/xml/xml_parser.c	(revision 167)
@@ -802,5 +802,4 @@
     }
 
-    pseg[pseg_index]->next_free_page = 0;
     pseg_index++;
 } // end psegNode()