Index: soft/giet_vm/giet_common/vmem.c
===================================================================
--- soft/giet_vm/giet_common/vmem.c	(revision 534)
+++ soft/giet_vm/giet_common/vmem.c	(revision 751)
@@ -10,5 +10,15 @@
 #include <vmem.h>
 #include <ctx_handler.h>
+#include <kernel_locks.h>
 #include <giet_config.h>
+
+//////////////////////////////////////////////////////////////////////////////////
+// Extern global variables (allocated in boot.c or kernel_init.c) 
+//////////////////////////////////////////////////////////////////////////////////
+
+extern  spin_lock_t         _ptabs_spin_lock[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE];
+extern  unsigned long long  _ptabs_paddr[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE];
+extern  unsigned int        _ptabs_next_pt2[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE];
+extern  unsigned int        _ptabs_max_pt2;
 
 ///////////////////////////////////////////////////////
@@ -104,4 +114,215 @@
 
 
+////////////////////////////////////////////
+void _v2p_add_pte1( unsigned int vspace_id,
+                    unsigned int x,
+                    unsigned int y,
+                    unsigned int vpn,        // 20 bits right-justified
+                    unsigned int flags,      // 10 bits left-justified 
+                    unsigned int ppn,        // 28 bits right-justified
+                    unsigned int ident )     // identity mapping if non zero
+{
+    unsigned int   pte1;     // PTE1 value
+    paddr_t        paddr;    // PTE1 physical address
+
+    // compute index in PT1
+    unsigned int    ix1 = vpn >> 9;         // 11 bits for ix1
+
+    // get PT1 physical base address 
+    paddr_t  pt1_base = _ptabs_paddr[vspace_id][x][y];
+
+    if ( pt1_base == 0 )
+    {
+        _printf("\n[GIET ERROR] in _v2p_add_pte1() : no PTAB in cluster[%d,%d]"
+                    " containing processors\n", x , y );
+        _exit();
+    }
+
+    // get lock protecting PTAB[vspace_id][x][y]
+    _spin_lock_acquire( &_ptabs_spin_lock[vspace_id][x][y] );
+
+    // compute pte1 physical address
+    paddr = pt1_base + 4*ix1;
+
+    // check PTE1 not already mapped
+    if ( ident == 0 )
+    {
+        if ( _physical_read( paddr ) & PTE_V )
+        {
+            _printf("\n[GIET ERROR] in _v2p_add_pte1() : vpn %x already mapped "
+                    "in PTAB[%d,%d] for vspace %d\n", vpn , x , y , vspace_id );
+            _spin_lock_release( &_ptabs_spin_lock[vspace_id][x][y] );
+            _exit();
+        }
+    }
+
+    // compute pte1 : 2 bits V T / 8 bits flags / 3 bits RSVD / 19 bits bppi
+    pte1 = PTE_V | (flags & 0x3FC00000) | ((ppn>>9) & 0x0007FFFF);
+
+    // write pte1 in PT1
+    _physical_write( paddr , pte1 );
+
+    // release lock protecting PTAB[vspace_id][x][y]
+    _spin_lock_release( &_ptabs_spin_lock[vspace_id][x][y] );
+
+    asm volatile ("sync");
+
+}   // end _v2p_add_pte1()
+
+
+
+///////////////////////////////////////////
+void _v2p_add_pte2( unsigned int vspace_id,
+                    unsigned int x,
+                    unsigned int y,
+                    unsigned int vpn,        // 20 bits right-justified
+                    unsigned int flags,      // 10 bits left-justified 
+                    unsigned int ppn,        // 28 bits right-justified
+                    unsigned int ident )     // identity mapping if non zero
+{
+    unsigned int ix1;
+    unsigned int ix2;
+    paddr_t      pt2_pbase;     // PT2 physical base address
+    paddr_t      pte2_paddr;    // PTE2 physical address
+    unsigned int pt2_id;        // PT2 index
+    unsigned int ptd;           // PTD : entry in PT1
+
+    ix1 = vpn >> 9;             // 11 bits for ix1
+    ix2 = vpn & 0x1FF;          //  9 bits for ix2
+
+    // get page table physical base address 
+    paddr_t      pt1_pbase = _ptabs_paddr[vspace_id][x][y];
+
+    if ( pt1_pbase == 0 )
+    {
+        _printf("\n[GIET ERROR] in _v2p_add_pte2() : no PTAB for vspace %d "
+                "in cluster[%d,%d]\n", vspace_id , x , y );
+        _exit();
+    }
+
+    // get lock protecting PTAB[vspace_id][x][y]
+    _spin_lock_acquire( &_ptabs_spin_lock[vspace_id][x][y] );
+
+    // get ptd in PT1
+    ptd = _physical_read( pt1_pbase + 4 * ix1 );
+
+    if ((ptd & PTE_V) == 0)    // undefined PTD: compute PT2 base address, 
+                               // and set a new PTD in PT1 
+    {
+        // get a new pt2_id
+        pt2_id = _ptabs_next_pt2[vspace_id][x][y];
+        _ptabs_next_pt2[vspace_id][x][y] = pt2_id + 1;
+
+        // check overflow
+        if (pt2_id == _ptabs_max_pt2) 
+        {
+            _printf("\n[GIET ERROR] in _v2p_add_pte2() : PTAB[%d,%d,%d]"
+                    " contains not enough PT2s\n", vspace_id, x, y );
+            _spin_lock_release( &_ptabs_spin_lock[vspace_id][x][y] );
+            _exit();
+        }
+
+        pt2_pbase = pt1_pbase + PT1_SIZE + PT2_SIZE * pt2_id;
+        ptd = PTE_V | PTE_T | (unsigned int) (pt2_pbase >> 12);
+
+        // set PTD into PT1
+        _physical_write( pt1_pbase + 4*ix1, ptd);
+    }
+    else                       // valid PTD: compute PT2 base address
+    {
+        pt2_pbase = ((paddr_t)(ptd & 0x0FFFFFFF)) << 12;
+    }
+
+    // set PTE in PT2 : flags & PPN in two 32 bits words
+    pte2_paddr  = pt2_pbase + 8 * ix2;
+    _physical_write(pte2_paddr     , (PTE_V | flags) );
+    _physical_write(pte2_paddr + 4 , ppn );
+
+    // release lock protecting PTAB[vspace_id][x][y]
+    _spin_lock_release( &_ptabs_spin_lock[vspace_id][x][y] );
+
+    asm volatile ("sync");
+
+}   // end _v2p_add_pte2()
+
+////////////////////////////////////////////
+void _v2p_del_pte1( unsigned int vspace_id,
+                    unsigned int x,
+                    unsigned int y,
+                    unsigned int vpn )       // 20 bits right-justified
+{
+    unsigned int ix1 = vpn >> 9;             // 11 bits for ix1
+
+    // get page table physical base address 
+    paddr_t pt1_pbase = _ptabs_paddr[vspace_id][x][y];
+
+    // check PTAB defined
+    if ( pt1_pbase == 0 )
+    {
+        _printf("\n[GIET ERROR] in _v2p_del_pte1() : no PTAB for vspace %d "
+                "in cluster[%d,%d]\n", vspace_id , x , y );
+        _exit();
+    }
+
+    // get ptd in PT1
+    paddr_t ptd_paddr = pt2_pbase + 4 * ix1;
+    unsigned int ptd = _physical_read( ptd_paddr );
+
+    // check ptd valid
+    if ((ptd & PTE_V) == 0)    
+    {
+        _printf("\n[GIET ERROR] in _v2p_del_pte1() : vpn %x not mapped in PT1"
+                "for vspace %d in cluster[%d,%d]\n", vpn , vspace_id , x , y );
+        _exit();
+    }
+
+    // invalidate PTD in PT1 
+    _physical_write( ptd_paddr , 0 );
+
+}   // end _v2p_del_pte1()
+ 
+////////////////////////////////////////////
+void _v2p_del_pte2( unsigned int vspace_id,
+                    unsigned int x,
+                    unsigned int y,
+                    unsigned int vpn )       // 20 bits right-justified
+{
+    unsigned int ix1 = vpn >> 9;             // 11 bits for ix1
+    unsigned int ix2 = vpn & 0x1FF;          //  9 bits for ix2
+
+    // get page table physical base address 
+    paddr_t pt1_pbase = _ptabs_paddr[vspace_id][x][y];
+
+    // check PTAB defined
+    if ( pt1_pbase == 0 )
+    {
+        _printf("\n[GIET ERROR] in _v2p_del_pte2() : no PTAB for vspace %d "
+                "in cluster[%d,%d]\n", vspace_id , x , y );
+        _exit();
+    }
+
+    // get ptd in PT1
+    unsigned int ptd = _physical_read( pt1_pbase + 4 * ix1 );
+
+    // check ptd valid
+    if ((ptd & PTE_V) == 0)    
+    {
+        _printf("\n[GIET ERROR] in _v2p_del_pte2() : vpn %x not mapped in PT1"
+                "for vspace %d in cluster[%d,%d]\n", vpn , vspace_id , x , y );
+        _exit();
+    }
+
+    // get PT2 physical base address
+    paddr_t  pt2_pbase = ((paddr_t)(ptd & 0x0FFFFFFF)) << 12;
+
+    // invalidate PTE in PT2 
+    paddr_t pte2_paddr  = pt2_pbase + 8 * ix2;
+    _physical_write( pte2_paddr , 0 );
+
+    asm volatile ("sync");
+
+}  // end _v2p_del_pte2()
+
+
 
 // Local Variables:
