Index: soft/giet_vm/giet_common/utils.c
===================================================================
--- soft/giet_vm/giet_common/utils.c	(revision 399)
+++ soft/giet_vm/giet_common/utils.c	(revision 408)
@@ -22,13 +22,9 @@
 extern static_scheduler_t* _schedulers[NB_PROCS_MAX<<(X_WIDTH+Y_WIDTH)];
 
-
 ///////////////////////////////////////////////////////////////////////////////////
 //         CP0 registers access functions
 ///////////////////////////////////////////////////////////////////////////////////
 
-///////////////////////////////////////////////////////////////////////////////////
-// Returns the value contained in CP0 SCHED register
-// (virtual base address of the processor scheduler).
-///////////////////////////////////////////////////////////////////////////////////
+/////////////////////////
 unsigned int _get_sched() 
 {
@@ -38,7 +34,5 @@
     return ret;
 }
-///////////////////////////////////////////////////////////////////////////////////
-// Returns EPC register content.
-///////////////////////////////////////////////////////////////////////////////////
+///////////////////////
 unsigned int _get_epc() 
 {
@@ -48,7 +42,5 @@
     return ret;
 }
-///////////////////////////////////////////////////////////////////////////////////
-// Returns BVAR register content.
-///////////////////////////////////////////////////////////////////////////////////
+////////////////////////
 unsigned int _get_bvar() 
 {
@@ -58,7 +50,5 @@
     return ret;
 }
-///////////////////////////////////////////////////////////////////////////////////
-// Returns CR register content.
-///////////////////////////////////////////////////////////////////////////////////
+//////////////////////
 unsigned int _get_cr() 
 {
@@ -68,7 +58,5 @@
     return ret;
 }
-///////////////////////////////////////////////////////////////////////////////////
-// Returns SR register content
-///////////////////////////////////////////////////////////////////////////////////
+//////////////////////
 unsigned int _get_sr() 
 {
@@ -78,16 +66,5 @@
     return ret;
 }
-//////////////////////////////////////////////////////////////////////////////
-// This function set a new value for the CP0 status register.
-//////////////////////////////////////////////////////////////////////////////
-void _set_sr(unsigned int val) 
-{
-    asm volatile( "mtc0      %0,     $12    \n"
-                  :
-                  :"r" (val) );
-}
-//////////////////////////////////////////////////////////////////////////////
-// Returns processor index
-//////////////////////////////////////////////////////////////////////////////
+//////////////////////////
 unsigned int _get_procid() 
 {
@@ -97,8 +74,5 @@
     return (ret & 0x3FF);
 }
-//////////////////////////////////////////////////////////////////////////////
-// Returns local time (32 bits value)
-// boot_proctime() 
-//////////////////////////////////////////////////////////////////////////////
+////////////////////////////
 unsigned int _get_proctime() 
 {
@@ -108,7 +82,6 @@
     return ret;
 }
-//////////////////////////////////////////////////////////////////////////////
-// Save SR value into save_sr_ptr variable and disable IRQs. 
-//////////////////////////////////////////////////////////////////////////////
+
+/////////////////////////////////////////////
 void _it_disable( unsigned int * save_sr_ptr) 
 {
@@ -123,8 +96,5 @@
     *save_sr_ptr = sr;
 }
-
-//////////////////////////////////////////////////////////////////////////////
-// Restores previous SR value.
-//////////////////////////////////////////////////////////////////////////////
+//////////////////////////////////////////////
 void _it_restore( unsigned int * save_sr_ptr ) 
 {
@@ -136,8 +106,5 @@
 }
 
-//////////////////////////////////////////////////////////////////////////////
-// This function set a new value in CP0 SCHED register.
-// (virtual base address of the processor scheduler).
-//////////////////////////////////////////////////////////////////////////////
+/////////////////////////////////
 void _set_sched(unsigned int val) 
 {
@@ -146,4 +113,12 @@
                    :"r" (val) );
 }
+//////////////////////////////
+void _set_sr(unsigned int val) 
+{
+    asm volatile ( "mtc0     %0,     $12            \n"
+                   :
+                   :"r" (val) );
+}
+
 
 ///////////////////////////////////////////////////////////////////////////////////
@@ -151,7 +126,5 @@
 ///////////////////////////////////////////////////////////////////////////////////
 
-///////////////////////////////////////////////////////////////////////////////////
-// Returns PTPR register content.
-///////////////////////////////////////////////////////////////////////////////////
+////////////////////////////
 unsigned int _get_mmu_ptpr() 
 {
@@ -161,7 +134,5 @@
     return ret;
 }
-///////////////////////////////////////////////////////////////////////////////////
-// Returns MODE register content.
-///////////////////////////////////////////////////////////////////////////////////
+////////////////////////////
 unsigned int _get_mmu_mode() 
 {
@@ -171,24 +142,29 @@
     return ret;
 }
-//////////////////////////////////////////////////////////////////////////////
-// This function set a new value for the MMU PTPR register.
-//////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////
 void _set_mmu_ptpr(unsigned int val) 
 {
-    asm volatile ( "mtc2     %0,     $0            \n"
+    asm volatile ( "mtc2     %0,     $0      \n"
                    :
                    :"r" (val)
                    :"memory" );
 }
-//////////////////////////////////////////////////////////////////////////////
-// This function set a new value for the MMU MODE register.
-//////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////
 void _set_mmu_mode(unsigned int val) 
 {
-    asm volatile ( "mtc2     %0,     $1             \n"
+    asm volatile ( "mtc2     %0,     $1      \n"
                    :
                    :"r" (val)
                    :"memory" );
 }
+////////////////////////////////////////////
+void _set_mmu_dcache_inval(unsigned int val) 
+{
+    asm volatile ( "mtc2     %0,     $7      \n"
+                   :
+                   :"r" (val)
+                   :"memory" );
+}
+
 
 ////////////////////////////////////////////////////////////////////////////
@@ -1033,14 +1009,12 @@
 ///////////////////////////////////////////////////////////////////////////////////
 // Invalidate all data cache lines corresponding to a memory 
-// buffer (identified by an address and a size).
-// TODO This should be replaced by a write to the CP2 MMU_DCACHE_INVAL
-// register, to be more processor independant.
-///////////////////////////////////////////////////////////////////////////////////
-void _dcache_buf_invalidate( void * buffer, 
-                             unsigned int size) 
-{
-    unsigned int i;
+// buffer (identified by virtual base address and size).
+///////////////////////////////////////////////////////////////////////////////////
+void _dcache_buf_invalidate( unsigned int buf_vbase, 
+                             unsigned int buf_size ) 
+{
+    unsigned int offset;
     unsigned int tmp;
-    unsigned int line_size;
+    unsigned int line_size;   // bytes
 
     // compute data cache line size based on config register (bits 12:10)
@@ -1048,13 +1022,12 @@
                  "mfc0 %0, $16, 1" 
                  : "=r" (tmp) );
+
     tmp = ((tmp >> 10) & 0x7);
     line_size = 2 << tmp;
 
     // iterate on cache lines 
-    for (i = 0; i < size; i += line_size) 
-    {
-        asm volatile(
-                " cache %0, %1"
-                : :"i" (0x11), "R" (*((unsigned char *) buffer + i)) );
+    for ( offset = 0; offset < buf_size; offset += line_size) 
+    {
+        _set_mmu_dcache_inval( buf_vbase + offset );
     }
 }
@@ -1110,5 +1083,5 @@
     if ( vobj_id != 0xFFFFFFFF ) 
     {
-        *vaddr  = vobjs[vobj_id].vaddr;
+        *vaddr  = vobjs[vobj_id].vbase;
         *length = vobjs[vobj_id].length;
         return 0;
