Index: soft/giet_vm/libs/stdio.c
===================================================================
--- soft/giet_vm/libs/stdio.c	(revision 160)
+++ soft/giet_vm/libs/stdio.c	(revision 165)
@@ -17,6 +17,4 @@
 #define SYSCALL_TTY_WRITE       0x02
 #define SYSCALL_TTY_READ        0x03
-#define SYSCALL_TIMER_WRITE     0x04
-#define SYSCALL_TIMER_READ      0x05
 #define SYSCALL_GCD_WRITE       0x06
 #define SYSCALL_GCD_READ        0x07
@@ -37,6 +35,8 @@
 
 //////////////////////////////////////////////////////////////////////////////////
-// 	sys_call()
+// sys_call()
 // This generic C function is used to implement all system calls.
+// It writes the system call arguments in the proper registers,
+// and tells GCC what has been modified by system call execution.
 //////////////////////////////////////////////////////////////////////////////////
 static inline unsigned int sys_call( unsigned int call_no,
@@ -83,8 +83,9 @@
 
 ////////////////////////////////////////////////////////////////////////////////////
-// 	procid()
+// giet_procid()
+////////////////////////////////////////////////////////////////////////////////////
 // This function returns the processor identifier.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int procid()
+unsigned int giet_procid()
 {
     return sys_call(SYSCALL_PROCID, 
@@ -92,8 +93,9 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-// 	proctime()
+// giet_proctime()
+////////////////////////////////////////////////////////////////////////////////////
 // This function returns the local processor time (clock cycles since boot)
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int proctime()
+unsigned int giet_proctime()
 {
     return sys_call(SYSCALL_PROCTIME, 
@@ -104,5 +106,6 @@
 
 ////////////////////////////////////////////////////////////////////////////////////
-// 	tty_putc()
+// giet_tty_putc()
+////////////////////////////////////////////////////////////////////////////////////
 // This function displays a single ascii character on a terminal.
 // The terminal index must be defined in the task context in the boot phase.
@@ -110,5 +113,5 @@
 // - Returns 1 if the character has been written, 0 otherwise.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_putc(char byte)
+unsigned int giet_tty_putc(char byte)
 {
     return sys_call(SYSCALL_TTY_WRITE,
@@ -118,5 +121,6 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-// 	 tty_puts()
+// giet_tty_puts()
+////////////////////////////////////////////////////////////////////////////////////
 // This function displays a string on a terminal.
 // The terminal index must be defined in the task context in the boot phase.
@@ -125,5 +129,5 @@
 // - Returns the number of written characters.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_puts(char *buf)
+unsigned int giet_tty_puts(char *buf)
 {
     unsigned int length = 0;
@@ -138,5 +142,6 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-//  	tty_putw()
+// giet_tty_putw()
+////////////////////////////////////////////////////////////////////////////////////
 // This function displays the value of a 32-bit word with decimal characters.
 // The terminal index must be defined in the task context in the boot phase.
@@ -144,5 +149,5 @@
 // Returns the number of written characters (should be equal to ten).
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_putw(unsigned int val)
+unsigned int giet_tty_putw(unsigned int val)
 {
     char buf[10];
@@ -160,5 +165,6 @@
 
 ////////////////////////////////////////////////////////////////////////////////////
-// tty_getc()
+// giet_tty_getc_no_irq()
+////////////////////////////////////////////////////////////////////////////////////
 // This blocking function fetches a single ascii character from a terminal.
 // The terminal index must be defined in the task context in the boot phase.
@@ -166,5 +172,5 @@
 // - Returns necessarily 0 when completed.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_getc(char *byte)
+unsigned int giet_tty_getc_no_irq(char *byte)
 {
     unsigned int ret = 0;
@@ -179,5 +185,6 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-// 	 tty_getc_irq()
+// giet_tty_getc()
+////////////////////////////////////////////////////////////////////////////////////
 // This blocking function fetches a single ascii character from a terminal.
 // The terminal index must be defined in the task context in the boot phase.
@@ -185,5 +192,5 @@
 // - Returns 0 when completed.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_getc_irq(char *byte)
+unsigned int giet_tty_getc(char *byte)
 {
     unsigned int ret = 0;
@@ -198,5 +205,6 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-// 	tty_gets_irq()
+// giet_tty_gets()
+////////////////////////////////////////////////////////////////////////////////////
 // This blocking function fetches a string from a terminal to a fixed length buffer.
 // The terminal index must be defined in the task context in the boot phase.
@@ -211,5 +219,6 @@
 //   removed from the target buffer.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_gets_irq(char *buf, unsigned int bufsize)
+unsigned int giet_tty_gets( char*			buf, 
+                            unsigned int	bufsize )
 {
     unsigned int ret;
@@ -240,5 +249,6 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-// 	tty_getw_irq()
+// giet_tty_getw()
+////////////////////////////////////////////////////////////////////////////////////
 // This blocking function fetches a string of decimal characters (most
 // significant digit first) to build a 32-bit unsigned integer.
@@ -256,5 +266,5 @@
 //   bits range, the zero value is returned.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_getw_irq(unsigned int *val)
+unsigned int giet_tty_getw(unsigned int *val)
 {
     unsigned char buf[32];
@@ -281,5 +291,5 @@
             buf[max] = byte;
             max++;
-            tty_putc(byte);
+            giet_tty_putc(byte);
         }
         else if ((byte == 0x0A) || (byte == 0x0D)) /* LF or CR character */
@@ -292,7 +302,7 @@
             {
                 max--; /* cancel the character */
-                tty_putc(0x08);
-                tty_putc(0x20);
-                tty_putc(0x08);
+                giet_tty_putc(0x08);
+                giet_tty_putc(0x20);
+                giet_tty_putc(0x08);
             }
         }
@@ -301,9 +311,9 @@
             for (i = 0; i < max; i++) /* cancel the string */
             {
-                tty_putc(0x08);
-                tty_putc(0x20);
-                tty_putc(0x08);
+                giet_tty_putc(0x08);
+                giet_tty_putc(0x20);
+                giet_tty_putc(0x08);
             }
-            tty_putc(0x30);
+            giet_tty_putc(0x30);
             *val = 0; /* return 0 value */
             return 0;
@@ -329,9 +339,9 @@
         for (i = 0; i < max; i++) /* cancel the string */
         {
-            tty_putc(0x08);
-            tty_putc(0x20);
-            tty_putc(0x08);
-        }
-        tty_putc(0x30);
+            giet_tty_putc(0x08);
+            giet_tty_putc(0x20);
+            giet_tty_putc(0x08);
+        }
+        giet_tty_putc(0x30);
         *val = 0; /* return 0 value */
     }
@@ -339,5 +349,6 @@
 }
 ////////////////////////////////////////////////////////////////////////////////////
-// tty_printf()
+// giet_tty_printf()
+////////////////////////////////////////////////////////////////////////////////////
 // This function is a simplified version of the mutek_printf() function.
 // The terminal index must be defined in the calling task context.
@@ -351,5 +362,5 @@
 // - Returns 0 if success, > 0 if error.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int tty_printf(char *format, ...)
+unsigned int giet_tty_printf(char *format, ...)
 {
     va_list ap;
@@ -450,73 +461,5 @@
 }
 
-/////  Timer device related system calls /////
-
-#define TIMER_VALUE     0
-#define TIMER_MODE      1
-#define TIMER_PERIOD    2
-#define TIMER_RESETIRQ  3
-
-/*
- * timer_set_mode()
- *
- * This function defines the operation mode of a timer. The possible values for
- * this mode are:
- * - 0x0 : Timer not activated
- * - 0x1 : Timer activated, but no interrupt is generated
- * - 0x3 : Timer activarted and periodic interrupts generated
- *
- * - Returns 0 if success, > 0 if error.
- */
-unsigned int timer_set_mode(unsigned int val)
-{
-    return sys_call(SYSCALL_TIMER_WRITE,
-            TIMER_MODE,
-            val,
-            0, 0);
-}
-
-/*
- * timer_set_period()
- *
- * This function defines the period value of a timer to enable a periodic
- * interrupt.
- * - Returns 0 if success, > 0 if error.
- */
-unsigned int timer_set_period(unsigned int val)
-{
-    return sys_call(SYSCALL_TIMER_WRITE,
-            TIMER_PERIOD,
-            val,
-            0, 0);
-}
-
-/*
- * timer_reset_irq()
- *
- * This function resets the interrupt signal issued by a timer.
- * - Returns 0 if success, > 0 if error.
- */
-unsigned int timer_reset_irq()
-{
-    return sys_call(SYSCALL_TIMER_WRITE,
-            TIMER_RESETIRQ,
-            0, 0, 0);
-}
-
-/*
- * timer_get_time()
- *
- * This function returns the current timing value of a timer.
- * - Returns 0 if success, > 0 if error.
- */
-unsigned int timer_get_time(unsigned int *time)
-{
-    return sys_call(SYSCALL_TIMER_READ,
-            TIMER_VALUE,
-            (unsigned int)time,
-            0, 0);
-}
-
-/////  GCD (Greatest Common Divider) device related system calls
+/////  GCD (Greatest Common Divider) related system calls
 
 #define GCD_OPA     0
@@ -526,9 +469,10 @@
 
 //////////////////////////////////////////////////////////////////////////////////
-// 	gcd_set_opa()
+// giet_gcd_set_opa()
+//////////////////////////////////////////////////////////////////////////////////
 // This function sets the operand A in the GCD coprocessor.
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int gcd_set_opa(unsigned int val)
+unsigned int giet_gcd_set_opa(unsigned int val)
 {
     return sys_call(SYSCALL_GCD_WRITE,
@@ -538,9 +482,10 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	gcd_set_opb()
+// 	giet_gcd_set_opb()
+//////////////////////////////////////////////////////////////////////////////////
 // This function sets operand B in the GCD coprocessor.
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int gcd_set_opb(unsigned int val)
+unsigned int giet_gcd_set_opb(unsigned int val)
 {
     return sys_call(SYSCALL_GCD_WRITE,
@@ -550,9 +495,10 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	gcd_start()
+// 	giet_gcd_start()
+//////////////////////////////////////////////////////////////////////////////////
 // This function starts the computation in the GCD coprocessor.
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int gcd_start()
+unsigned int giet_gcd_start()
 {
     return sys_call(SYSCALL_GCD_WRITE,
@@ -561,9 +507,10 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	gcd_get_status()
+// 	giet_gcd_get_status()
+//////////////////////////////////////////////////////////////////////////////////
 // This function gets the status fromn the GCD coprocessor.
 // - The value is 0 when the coprocessor is idle (computation completed).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int gcd_get_status(unsigned int *val)
+unsigned int giet_gcd_get_status(unsigned int *val)
 {
     return sys_call(SYSCALL_GCD_READ,
@@ -573,8 +520,9 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	gcd_get_result()
+// 	giet_gcd_get_result()
+//////////////////////////////////////////////////////////////////////////////////
 // This function gets the result of the computation from the GCD coprocessor.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int gcd_get_result(unsigned int *val)
+unsigned int giet_gcd_get_result(unsigned int *val)
 {
     return sys_call(SYSCALL_GCD_READ,
@@ -587,5 +535,6 @@
 
 //////////////////////////////////////////////////////////////////////////////////
-// 	ioc_write()
+// 	giet_ioc_write()
+//////////////////////////////////////////////////////////////////////////////////
 // Transfer data from a memory buffer to a file on the block_device.
 //     lba    : Logical Block Address (first block index)
@@ -594,5 +543,7 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int ioc_write(unsigned int lba, void *buffer, unsigned int count)
+unsigned int giet_ioc_write( unsigned int	lba, 
+                             void*			buffer, 
+                             unsigned int	count)
 {
     return sys_call(SYSCALL_IOC_WRITE,
@@ -603,5 +554,6 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	ioc_read()
+// giet_ioc_read()
+//////////////////////////////////////////////////////////////////////////////////
 // Transfer data from a file on the block_device to a memory buffer.
 //     lba    : Logical Block Address (first block index)
@@ -610,5 +562,7 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int ioc_read(unsigned int lba, void *buffer, unsigned int count)
+unsigned int giet_ioc_read( unsigned int		lba, 
+                            void*				buffer, 
+                            unsigned int		count )
 {
     return sys_call(SYSCALL_IOC_READ,
@@ -619,9 +573,10 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	ioc_completed()
+// giet_ioc_completed()
+//////////////////////////////////////////////////////////////////////////////////
 // This blocking function returns 0 when the I/O transfer is
 // successfully completed, and returns 1 if an address error has been detected.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int ioc_completed()
+unsigned int giet_ioc_completed()
 {
     return sys_call(SYSCALL_IOC_COMPLETED,
@@ -632,5 +587,6 @@
 
 //////////////////////////////////////////////////////////////////////////////////
-// 	fb_sync_write()
+// giet_fb_sync_write()
+//////////////////////////////////////////////////////////////////////////////////
 // This blocking function use a memory copy strategy to transfer data from a
 // user buffer to the frame buffer device in kernel space.
@@ -640,5 +596,7 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int fb_sync_write(unsigned int offset, void *buffer, unsigned int length)
+unsigned int giet_fb_sync_write( unsigned int	offset, 
+                                 void*			buffer, 
+                                 unsigned int	length )
 {
     return sys_call(SYSCALL_FB_SYNC_WRITE,
@@ -649,5 +607,6 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	fb_sync_read()
+// giet_fb_sync_read()
+//////////////////////////////////////////////////////////////////////////////////
 // This blocking function use a memory copy strategy to transfer data from the
 // frame buffer device in kernel space to an user buffer.
@@ -657,5 +616,7 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int fb_sync_read(unsigned int offset, void *buffer, unsigned int length)
+unsigned int giet_fb_sync_read( unsigned int	offset, 
+                                void*			buffer, 
+                                unsigned int	length )
 {
     return sys_call(SYSCALL_FB_SYNC_READ,
@@ -666,5 +627,6 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	fb_write()
+// giet_fb_write()
+//////////////////////////////////////////////////////////////////////////////////
 // This non-blocking function use the DMA coprocessor to transfer data from a
 // user buffer to the frame buffer device in kernel space.
@@ -676,5 +638,7 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int fb_write(unsigned int offset, void *buffer, unsigned int length)
+unsigned int giet_fb_write( unsigned int	offset, 
+                            void*			buffer, 
+                            unsigned int	length )
 {
     return sys_call(SYSCALL_FB_WRITE,
@@ -685,5 +649,6 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-//	 fb_read()
+// giet_fb_read()
+//////////////////////////////////////////////////////////////////////////////////
 // This non-blocking function use the DMA coprocessor to transfer data from the
 // frame buffer device in kernel space to an user buffer.
@@ -695,7 +660,7 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int fb_read( unsigned int offset, 
-                      void *buffer, 
-                      unsigned int length )
+unsigned int giet_fb_read( unsigned int		offset, 
+                           void*			buffer, 
+                           unsigned int		length )
 {
     return sys_call(SYSCALL_FB_READ,
@@ -706,9 +671,10 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	fb_completed()
+// giet_fb_completed()
+//////////////////////////////////////////////////////////////////////////////////
 // This blocking function returns when the transfer is completed.
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int fb_completed()
+unsigned int giet_fb_completed()
 {
     return sys_call(SYSCALL_FB_COMPLETED,
@@ -716,19 +682,19 @@
 }
 
-///// Platform or mapping related system calls /////
-
-//////////////////////////////////////////////////////////////////////////////////
-// 	mwmr_base()
-// 	TODO!
-// This function returns in argument buffer the virtual base address 
-// of a MWMR communication channel, identified by the two arguments
-// vspace_name and channel_name.
-// As the GIET does not support dynamic allocation, the MWMR channel
-// must be declared in the mapping_info data structure to be initialised
-// in the boot phase.
-// - Returns the address if success,  0 if error ( channel not defined )
-//////////////////////////////////////////////////////////////////////////////////
-unsigned int vobj_get_vbase( char* vspace_name, char* vobj_name,
-                        unsigned int vobj_type, unsigned int* vobj_buffer)
+///// Miscellaneous related system calls /////
+
+//////////////////////////////////////////////////////////////////////////////////
+// giet_vobj_get_vbase()
+//////////////////////////////////////////////////////////////////////////////////
+// This function writes in argument (vobj_vaddr) the virtual base address 
+// of a vobj (defined in the mapping_info data structure), identified by 
+// the two arguments (vspace_name and vobj_name).
+// The (vobj_type) argument is redundant, and used for coherence checking.
+// - Returns the address if success,  0 if error ( not defined or wrong type )
+//////////////////////////////////////////////////////////////////////////////////
+unsigned int giet_vobj_get_vbase( char*			vspace_name, 
+                                  char*			vobj_name,
+                                  unsigned int	vobj_type, 
+                                  unsigned int* vobj_vaddr )
 {
     return sys_call(SYSCALL_VOBJ_GET_VBASE, 
@@ -736,14 +702,16 @@
                     (unsigned int)vobj_name,
                     (unsigned int)vobj_type,
-                    (unsigned int)vobj_buffer);
-}
-////////////////////////////////////////////////////////////////////////////////////
-// 	proc_number()
+                    (unsigned int)vobj_vaddr);
+}
+
+////////////////////////////////////////////////////////////////////////////////////
+// giet_proc_number()
+////////////////////////////////////////////////////////////////////////////////////
 // This function returns in the buffer argument the number of processors 
 // in the cluster specified by the cluster_id argument.
 // - Returns 0 if success, > 0 if error ( cluster index too large )
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int proc_number( unsigned int cluster_id,
-                          unsigned int* buffer )
+unsigned int giet_proc_number( unsigned int		cluster_id,
+                               unsigned int*	buffer )
 {
     return sys_call(SYSCALL_PROC_NUMBER, 
@@ -756,22 +724,21 @@
 
 //////////////////////////////////////////////////////////////////////////////////
-// exit()
+// giet_task_exit()
+//////////////////////////////////////////////////////////////////////////////////
 // This function stops execution of the calling task with a TTY message, 
 // and enter an infinite loop.
 // The task is blocked, but it still consume processor cycles ...
 //////////////////////////////////////////////////////////////////////////////////
-void exit()
-{
-    unsigned int proc_index = procid();
+void giet_exit()
+{
     sys_call(SYSCALL_EXIT, 
-             proc_index, 
-             0, 0, 0);
+             0, 0, 0, 0);
 }
 ///////////////////////////////////////////////////////////////////////////////////
-// 	rand()
+// giet_rand()
 // This function returns a pseudo-random value derived from the processor cycle
 // count. This value is comprised between 0 & 65535.
 ///////////////////////////////////////////////////////////////////////////////////
-unsigned int rand()
+unsigned int giet_rand()
 {
     unsigned int x = sys_call(SYSCALL_PROCTIME, 
@@ -783,9 +750,9 @@
 }
 //////////////////////////////////////////////////////////////////////////////////
-// 	ctx_switch()
+// giet_ctx_switch()
 // The user task calling this function is descheduled and
 // the processor is allocated to another task.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int ctx_switch()
+unsigned int giet_ctx_switch()
 {
     return sys_call(SYSCALL_CTX_SWITCH, 
