Index: soft/giet_vm/libs/stdio.c
===================================================================
--- soft/giet_vm/libs/stdio.c	(revision 218)
+++ soft/giet_vm/libs/stdio.c	(revision 228)
@@ -21,4 +21,5 @@
 #define SYSCALL_GCD_WRITE       0x06
 #define SYSCALL_GCD_READ        0x07
+#define SYSCALL_TASK_ID         0x09
 #define SYSCALL_CTX_SWITCH      0x0D
 #define SYSCALL_EXIT            0x0E
@@ -32,5 +33,5 @@
 #define SYSCALL_IOC_READ        0x16
 #define SYSCALL_IOC_COMPLETED   0x17
-#define SYSCALL_VOBJ_GET_VBASE	0x1A
+#define SYSCALL_VOBJ_GET_VBASE  0x1A
 #define SYSCALL_NIC_WRITE       0x1B
 #define SYSCALL_NIC_READ        0x1C
@@ -43,15 +44,14 @@
 // and tells GCC what has been modified by system call execution.
 //////////////////////////////////////////////////////////////////////////////////
-static inline unsigned int sys_call( unsigned int call_no,
-                                     unsigned int arg_0, 
-                                     unsigned int arg_1, 
-                                     unsigned int arg_2, 
-                                     unsigned int arg_3)
-{
+static inline unsigned int sys_call(unsigned int call_no,
+        unsigned int arg_0, 
+        unsigned int arg_1, 
+        unsigned int arg_2, 
+        unsigned int arg_3) {
     register unsigned int reg_no_and_output asm("v0") = call_no;
-    register unsigned int reg_a0            asm("a0") = arg_0;
-    register unsigned int reg_a1            asm("a1") = arg_1;
-    register unsigned int reg_a2            asm("a2") = arg_2;
-    register unsigned int reg_a3            asm("a3") = arg_3;
+    register unsigned int reg_a0 asm("a0") = arg_0;
+    register unsigned int reg_a1 asm("a1") = arg_1;
+    register unsigned int reg_a2 asm("a2") = arg_2;
+    register unsigned int reg_a3 asm("a3") = arg_3;
 
     asm volatile(
@@ -59,8 +59,8 @@
             : "=r" (reg_no_and_output)  /* output argument */
             : "r" (reg_a0),             /* input arguments */
-              "r" (reg_a1),
-              "r" (reg_a2),
-              "r" (reg_a3),
-              "r" (reg_no_and_output)
+            "r" (reg_a1),
+            "r" (reg_a2),
+            "r" (reg_a3),
+            "r" (reg_no_and_output)
             : "memory",
             /* These persistant registers will be saved on the stack by the
@@ -83,5 +83,5 @@
 }
 
-///// 	 MIPS32 related system calls  /////
+/////      MIPS32 related system calls  /////
 
 ////////////////////////////////////////////////////////////////////////////////////
@@ -90,9 +90,9 @@
 // This function returns the processor identifier.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_procid()
-{
-    return sys_call(SYSCALL_PROCID, 
-                    0, 0, 0, 0);
-}
+unsigned int giet_procid() {
+    return sys_call(SYSCALL_PROCID, 0, 0, 0, 0);
+}
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_proctime()
@@ -100,11 +100,10 @@
 // This function returns the local processor time (clock cycles since boot)
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_proctime()
-{
-    return sys_call(SYSCALL_PROCTIME, 
-                    0, 0, 0, 0);
-}
-
-////// 	TTY device related system calls /////
+unsigned int giet_proctime() {
+    return sys_call(SYSCALL_PROCTIME, 0, 0, 0, 0);
+}
+
+
+//////     TTY device related system calls /////
 
 ////////////////////////////////////////////////////////////////////////////////////
@@ -116,11 +115,9 @@
 // - Returns 1 if the character has been written, 0 otherwise.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_putc(char byte)
-{
-    return sys_call(SYSCALL_TTY_WRITE,
-                    (unsigned int)(&byte),
-                    1,
-                    0,0);
-}
+unsigned int giet_tty_putc(char byte) {
+    return sys_call(SYSCALL_TTY_WRITE, (unsigned int) (&byte), 1, 0, 0);
+}
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_tty_puts()
@@ -132,16 +129,13 @@
 // - Returns the number of written characters.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_puts(char *buf)
-{
+unsigned int giet_tty_puts(char * buf) {
     unsigned int length = 0;
-    while (buf[length] != 0)
-    {
+    while (buf[length] != 0) {
         length++;
     }
-    return sys_call(SYSCALL_TTY_WRITE,
-                    (unsigned int)buf,
-                    length,
-                    0,0);
-}
+    return sys_call(SYSCALL_TTY_WRITE, (unsigned int) buf, length, 0, 0);
+}
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_tty_putw()
@@ -152,18 +146,15 @@
 // Returns the number of written characters (should be equal to ten).
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_putw(unsigned int val)
-{
+unsigned int giet_tty_putw(unsigned int val) {
     char buf[10];
     unsigned int i;
-    for (i = 0; i < 10; i++)
-    {
-        buf[9-i] = (val % 10) + 0x30;
+    for (i = 0; i < 10; i++) {
+        buf[9 - i] = (val % 10) + 0x30;
         val = val / 10;
     }
-    return sys_call(SYSCALL_TTY_WRITE,
-                    (unsigned int)buf,
-                    10,
-                    0,0);
-}
+    return sys_call(SYSCALL_TTY_WRITE, (unsigned int) buf, 10, 0, 0);
+}
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_tty_getc()
@@ -174,16 +165,13 @@
 // - Returns 0 when completed.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_getc(char *byte)
-{
+unsigned int giet_tty_getc(char * byte) {
     unsigned int ret = 0;
-    while (ret == 0)
-    {
-        ret = sys_call(SYSCALL_TTY_READ,
-                       (unsigned int)byte,
-                       1,
-                       0,0);
+    while (ret == 0) {
+        ret = sys_call(SYSCALL_TTY_READ, (unsigned int)byte, 1, 0, 0);
     }
     return 0;
 }
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_tty_gets()
@@ -201,26 +189,21 @@
 //   removed from the target buffer.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_gets( char*			buf, 
-                            unsigned int	bufsize )
-{
+unsigned int giet_tty_gets(char * buf, unsigned int bufsize) {
     unsigned int ret;
     unsigned char byte;
     unsigned int index = 0;
 
-    while (index < (bufsize - 1))
-    {
+    while (index < (bufsize - 1)) {
         do {
-            ret = sys_call(SYSCALL_TTY_READ,
-                           (unsigned int)(&byte),
-                           1,
-                           0,0);
+            ret = sys_call(SYSCALL_TTY_READ, (unsigned int) (&byte), 1, 0, 0);
         } while (ret != 1);
 
-        if ( byte == 0x0A )
+        if (byte == 0x0A) {
             break; /* LF */
-        else if ((byte == 0x7F) && (index > 0))
+        }
+        else if ((byte == 0x7F) && (index > 0)) {
             index--; /* DEL */
-        else
-        {
+        }
+        else {
             buf[index] = byte;
             index++;
@@ -230,4 +213,6 @@
     return 0;
 }
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_tty_getw()
@@ -248,6 +233,5 @@
 //   bits range, the zero value is returned.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_getw(unsigned int *val)
-{
+unsigned int giet_tty_getw(unsigned int * val) {
     unsigned char buf[32];
     unsigned char byte;
@@ -260,27 +244,22 @@
     unsigned int ret;
 
-    while (done == 0)
-    {
+    while (done == 0) {
         do {
-            ret = sys_call(SYSCALL_TTY_READ,
-                           (unsigned int)(&byte),
-                           1,
-                           0,0);
+            ret = sys_call(SYSCALL_TTY_READ, (unsigned int) (&byte), 1, 0, 0);
         } while (ret != 1);
 
-        if ((byte > 0x2F) && (byte < 0x3A)) /* decimal character */
-        {
+        if ((byte > 0x2F) && (byte < 0x3A)) {
+            /* decimal character */
             buf[max] = byte;
             max++;
             giet_tty_putc(byte);
         }
-        else if ((byte == 0x0A) || (byte == 0x0D)) /* LF or CR character */
-        {
+        else if ((byte == 0x0A) || (byte == 0x0D)) {
+            /* LF or CR character */
             done = 1;
         }
-        else if (byte == 0x7F) /* DEL character */
-        {
-            if (max > 0)
-            {
+        else if (byte == 0x7F) {
+            /* DEL character */
+            if (max > 0) {
                 max--; /* cancel the character */
                 giet_tty_putc(0x08);
@@ -289,8 +268,8 @@
             }
         }
-        if (max == 32) /* decimal string overflow */
-        {
-            for (i = 0; i < max; i++) /* cancel the string */
-            {
+        if (max == 32) {
+            /* decimal string overflow */
+            for (i = 0; i < max; i++) {
+                /* cancel the string */
                 giet_tty_putc(0x08);
                 giet_tty_putc(0x20);
@@ -304,21 +283,19 @@
 
     /* string conversion */
-    for (i = 0; i < max; i++)
-    {
+    for (i = 0; i < max; i++) {
         dec = dec * 10 + (buf[i] - 0x30);
-        if (dec < save)
+        if (dec < save) {
             overflow = 1;
+        }
         save = dec;
     }
 
     /* check overflow */
-    if (overflow == 0)
-    {
+    if (overflow == 0) {
         *val = dec; /* return decimal value */
     }
-    else
-    {
-        for (i = 0; i < max; i++) /* cancel the string */
-        {
+    else {
+        for (i = 0; i < max; i++) {
+            /* cancel the string */
             giet_tty_putc(0x08);
             giet_tty_putc(0x20);
@@ -330,4 +307,6 @@
     return 0;
 }
+
+
 ////////////////////////////////////////////////////////////////////////////////////
 // giet_tty_printf()
@@ -344,6 +323,5 @@
 // - Returns 0 if success, > 0 if error.
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_tty_printf(char *format, ...)
-{
+unsigned int giet_tty_printf(char * format, ...) {
     va_list ap;
     va_start(ap, format);
@@ -354,13 +332,10 @@
     while (*format) {
         unsigned int i;
-        for (i = 0; format[i] && format[i] != '%'; i++)
-            ;
+        for (i = 0; format[i] && format[i] != '%'; i++);
         if (i) {
-            ret = sys_call(SYSCALL_TTY_WRITE,
-                    (unsigned int)format,
-                    i,
-                    0,0);
-            if (ret != i)
+            ret = sys_call(SYSCALL_TTY_WRITE, (unsigned int) format, i, 0, 0);
+            if (ret != i) {
                 return 1; /* return error */
+            }
             format += i;
         }
@@ -377,10 +352,10 @@
 
     {
-        int         val = va_arg(ap, long);
-        char            buf[20];
-        char*           pbuf;
-        unsigned int        len = 0;
-        static const char   HexaTab[] = "0123456789ABCDEF";
-        unsigned int        i;
+        int val = va_arg(ap, long);
+        char buf[20];
+        char * pbuf;
+        unsigned int len = 0;
+        static const char HexaTab[] = "0123456789ABCDEF";
+        unsigned int i;
 
         switch (*format++) {
@@ -393,38 +368,40 @@
                 if (val < 0) {
                     val = -val;
-                    ret = sys_call(SYSCALL_TTY_WRITE,
-                            (unsigned int)"-",
-                            1,
-                            0,0);
-                    if (ret != 1)
+                    ret = sys_call(SYSCALL_TTY_WRITE, (unsigned int)"-", 1, 0, 0);
+                    if (ret != 1) {
                         return 1; /* return error */
+                    }
                 }
             case ('u'):             /* decimal unsigned integer */
-                for( i=0 ; i<10 ; i++) {
-                    buf[9-i] = HexaTab[val % 10];
-                    if (!(val /= 10)) break;
+                for(i = 0; i < 10; i++) {
+                    buf[9 - i] = HexaTab[val % 10];
+                    if (!(val /= 10)) {
+                        break;
+                    }
                 }
-                len =  i+1;
-                pbuf = &buf[9-i];
+                len =  i + 1;
+                pbuf = &buf[9 - i];
                 break;
             case ('x'):             /* hexadecimal integer */
-                ret = sys_call(SYSCALL_TTY_WRITE,
-                        (unsigned int)"0x",
-                        2,
-                        0,0);
-                if (ret != 2)
+                ret = sys_call(SYSCALL_TTY_WRITE, (unsigned int) "0x", 2, 0, 0);
+                if (ret != 2) {
                     return 1; /* return error */
-                for( i=0 ; i<8 ; i++) {
-                    buf[7-i] = HexaTab[val % 16U];
-                    if (!(val /= 16U)) break;
                 }
-                len =  i+1;
-                pbuf = &buf[7-i];
+                for(i = 0; i < 8; i++) {
+                    buf[7 - i] = HexaTab[val % 16U];
+                    if (!(val /= 16U)) {
+                        break;
+                    }
+                }
+                len =  i + 1;
+                pbuf = &buf[7 - i];
                 break;
             case ('s'):             /* string */
                 {
-                    char *str = (char*)val;
-                    while ( str[len] ) len++;
-                    pbuf = (char*)val;
+                    char * str = (char *) val;
+                    while (str[len]) {
+                        len++;
+                    }
+                    pbuf = (char *) val;
                 }
                 break;
@@ -433,10 +410,8 @@
         }
 
-        ret = sys_call(SYSCALL_TTY_WRITE,
-                (unsigned int)pbuf,
-                len,
-                0,0);
-        if (ret != len)
+        ret = sys_call(SYSCALL_TTY_WRITE, (unsigned int) pbuf, len, 0, 0);
+        if (ret != len) {
             return 1;
+        }
         goto printf_text;
     }
@@ -453,9 +428,9 @@
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_timer_start()
-{
-    return sys_call(SYSCALL_TIMER_START,
-                   0,0,0,0);
-}
+unsigned int giet_timer_start() {
+    return sys_call(SYSCALL_TIMER_START, 0, 0, 0, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_timer_stop()
@@ -464,9 +439,8 @@
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_timer_stop()
-{
-    return sys_call(SYSCALL_TIMER_STOP,
-                   0,0,0,0);
-}
+unsigned int giet_timer_stop() {
+    return sys_call(SYSCALL_TIMER_STOP, 0, 0, 0, 0);
+}
+
 
 /////  GCD (Greatest Common Divider) related system calls
@@ -483,66 +457,56 @@
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_gcd_set_opa(unsigned int val)
-{
-    return sys_call(SYSCALL_GCD_WRITE,
-                    GCD_OPA,
-                    val,
-                    0, 0);
-}
-//////////////////////////////////////////////////////////////////////////////////
-// 	giet_gcd_set_opb()
+unsigned int giet_gcd_set_opa(unsigned int val) {
+    return sys_call(SYSCALL_GCD_WRITE, GCD_OPA, val, 0, 0);
+}
+
+
+//////////////////////////////////////////////////////////////////////////////////
+//     giet_gcd_set_opb()
 //////////////////////////////////////////////////////////////////////////////////
 // This function sets operand B in the GCD coprocessor.
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_gcd_set_opb(unsigned int val)
-{
-    return sys_call(SYSCALL_GCD_WRITE,
-                    GCD_OPB,
-                    val,
-                    0, 0);
-}
-//////////////////////////////////////////////////////////////////////////////////
-// 	giet_gcd_start()
+unsigned int giet_gcd_set_opb(unsigned int val) {
+    return sys_call(SYSCALL_GCD_WRITE, GCD_OPB, val, 0, 0);
+}
+
+
+//////////////////////////////////////////////////////////////////////////////////
+//     giet_gcd_start()
 //////////////////////////////////////////////////////////////////////////////////
 // This function starts the computation in the GCD coprocessor.
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_gcd_start()
-{
-    return sys_call(SYSCALL_GCD_WRITE,
-                    GCD_START,
-                    0, 0, 0);
-}
-//////////////////////////////////////////////////////////////////////////////////
-// 	giet_gcd_get_status()
+unsigned int giet_gcd_start() {
+    return sys_call(SYSCALL_GCD_WRITE, GCD_START, 0, 0, 0);
+}
+
+
+//////////////////////////////////////////////////////////////////////////////////
+//     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 giet_gcd_get_status(unsigned int *val)
-{
-    return sys_call(SYSCALL_GCD_READ,
-            GCD_STATUS,
-            (unsigned int)val,
-            0, 0);
-}
-//////////////////////////////////////////////////////////////////////////////////
-// 	giet_gcd_get_result()
+unsigned int giet_gcd_get_status(unsigned int * val) {
+    return sys_call(SYSCALL_GCD_READ, GCD_STATUS, (unsigned int) val, 0, 0);
+}
+
+
+//////////////////////////////////////////////////////////////////////////////////
+//     giet_gcd_get_result()
 //////////////////////////////////////////////////////////////////////////////////
 // This function gets the result of the computation from the GCD coprocessor.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_gcd_get_result(unsigned int *val)
-{
-    return sys_call(SYSCALL_GCD_READ,
-            GCD_OPA,
-            (unsigned int)val,
-            0, 0);
-}
+unsigned int giet_gcd_get_result(unsigned int * val) {
+    return sys_call(SYSCALL_GCD_READ, GCD_OPA, (unsigned int) val, 0, 0);
+}
+
 
 ///// Block device related system calls  /////
 
 //////////////////////////////////////////////////////////////////////////////////
-// 	giet_ioc_write()
+//     giet_ioc_write()
 //////////////////////////////////////////////////////////////////////////////////
 // Transfer data from a memory buffer to a file on the block_device.
@@ -552,14 +516,9 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_ioc_write( unsigned int	lba, 
-                             void*			buffer, 
-                             unsigned int	count)
-{
-    return sys_call(SYSCALL_IOC_WRITE,
-            lba,
-            (unsigned int)buffer,
-            count,
-            0);
-}
+unsigned int giet_ioc_write( unsigned int lba, void * buffer, unsigned int count) {
+    return sys_call(SYSCALL_IOC_WRITE, lba, (unsigned int) buffer, count, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_ioc_read()
@@ -571,14 +530,9 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_ioc_read( unsigned int		lba, 
-                            void*				buffer, 
-                            unsigned int		count )
-{
-    return sys_call(SYSCALL_IOC_READ,
-            lba,
-            (unsigned int)buffer,
-            count,
-            0);
-}
+unsigned int giet_ioc_read(unsigned int lba, void * buffer, unsigned int count) {
+    return sys_call(SYSCALL_IOC_READ, lba, (unsigned int) buffer, count, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_ioc_completed()
@@ -587,9 +541,8 @@
 // successfully completed, and returns 1 if an address error has been detected.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_ioc_completed()
-{
-    return sys_call(SYSCALL_IOC_COMPLETED,
-            0, 0, 0, 0);
-}
+unsigned int giet_ioc_completed() {
+    return sys_call(SYSCALL_IOC_COMPLETED, 0, 0, 0, 0);
+}
+
 
 /////  Frame buffer device related system calls  /////
@@ -605,14 +558,9 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_fb_sync_write( unsigned int	offset, 
-                                 void*			buffer, 
-                                 unsigned int	length )
-{
-    return sys_call(SYSCALL_FB_SYNC_WRITE,
-            offset,
-            (unsigned int)buffer,
-            length,
-            0);
-}
+unsigned int giet_fb_sync_write(unsigned int offset, void * buffer, unsigned int length) {
+    return sys_call(SYSCALL_FB_SYNC_WRITE, offset, (unsigned int) buffer, length, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_fb_sync_read()
@@ -625,14 +573,9 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_fb_sync_read( unsigned int	offset, 
-                                void*			buffer, 
-                                unsigned int	length )
-{
-    return sys_call(SYSCALL_FB_SYNC_READ,
-            offset,
-            (unsigned int)buffer,
-            length,
-            0);
-}
+unsigned int giet_fb_sync_read(unsigned int offset, void * buffer, unsigned int length) {
+    return sys_call(SYSCALL_FB_SYNC_READ, offset, (unsigned int) buffer, length, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_fb_write()
@@ -647,14 +590,9 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_fb_write( unsigned int	offset, 
-                            void*		buffer, 
-                            unsigned int	length )
-{
-    return sys_call(SYSCALL_FB_WRITE,
-            offset,
-            (unsigned int)buffer,
-            length,
-            0);
-}
+unsigned int giet_fb_write(unsigned int offset, void * buffer, unsigned int length) {
+    return sys_call(SYSCALL_FB_WRITE, offset, (unsigned int) buffer, length, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_fb_read()
@@ -669,14 +607,9 @@
 // - Returns 0 if success, > 0 if error (e.g. memory buffer not in user space).
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_fb_read( unsigned int		offset, 
-                           void*		buffer, 
-                           unsigned int		length )
-{
-    return sys_call(SYSCALL_FB_READ,
-                    offset,
-                    (unsigned int)buffer,
-                    length,
-                    0);
-}
+unsigned int giet_fb_read(unsigned int offset, void * buffer, unsigned int length) {
+    return sys_call(SYSCALL_FB_READ, offset, (unsigned int) buffer, length, 0);
+}
+
+
 //////////////////////////////////////////////////////////////////////////////////
 // giet_fb_completed()
@@ -685,9 +618,8 @@
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_fb_completed()
-{
-    return sys_call(SYSCALL_FB_COMPLETED,
-                    0, 0, 0, 0);
-}
+unsigned int giet_fb_completed() {
+    return sys_call(SYSCALL_FB_COMPLETED, 0, 0, 0, 0);
+}
+
 
 //////////////////////////////////////////////////////////////////////////////////
@@ -704,14 +636,8 @@
 //////////////////////////////////////////////////////////////////////////////////
 
-unsigned int giet_nic_write( unsigned int	offset, 
-                             void*		buffer, 
-                             unsigned int	length )
-{
-    return sys_call(SYSCALL_NIC_WRITE,
-            offset,
-            (unsigned int)buffer,
-            length,
-            0);
-}
+unsigned int giet_nic_write(unsigned int offset, void * buffer, unsigned int length) {
+    return sys_call(SYSCALL_NIC_WRITE, offset, (unsigned int) buffer, length, 0);
+}
+
 
 //////////////////////////////////////////////////////////////////////////////////
@@ -728,14 +654,8 @@
 //////////////////////////////////////////////////////////////////////////////////
 
-unsigned int giet_nic_read( unsigned int	offset, 
-                            void*		    buffer, 
-                            unsigned int	length )
-{
-    return sys_call(SYSCALL_NIC_READ,
-            offset,
-            (unsigned int)buffer,
-            length,
-            0);
-}
+unsigned int giet_nic_read(unsigned int offset, void * buffer, unsigned int length) {
+    return sys_call(SYSCALL_NIC_READ, offset, (unsigned int) buffer, length, 0);
+}
+
 
 //////////////////////////////////////////////////////////////////////////////////
@@ -745,9 +665,8 @@
 // - Returns 0 if success, > 0 if error.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_nic_completed()
-{
-    return sys_call(SYSCALL_NIC_COMPLETED,
-                    0, 0, 0, 0);
-}
+unsigned int giet_nic_completed() {
+    return sys_call(SYSCALL_NIC_COMPLETED, 0, 0, 0, 0);
+}
+
 
 ///// Miscellaneous related system calls /////
@@ -762,15 +681,12 @@
 // - 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 )
-{
+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, 
-                    (unsigned int)vspace_name,
-                    (unsigned int)vobj_name,
-                    (unsigned int)vobj_type,
-                    (unsigned int)vobj_vaddr);
-}
+            (unsigned int) vspace_name,
+            (unsigned int) vobj_name,
+            (unsigned int) vobj_type,
+            (unsigned int) vobj_vaddr);
+}
+
 
 ////////////////////////////////////////////////////////////////////////////////////
@@ -781,12 +697,8 @@
 // - Returns 0 if success, > 0 if error ( cluster index too large )
 ////////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_proc_number( unsigned int		cluster_id,
-                               unsigned int*	buffer )
-{
-    return sys_call(SYSCALL_PROC_NUMBER, 
-                    cluster_id,
-                    (unsigned int)buffer,
-                    0, 0);
-}
+unsigned int giet_proc_number(unsigned int cluster_id, unsigned int * buffer) {
+    return sys_call(SYSCALL_PROC_NUMBER, cluster_id, (unsigned int) buffer, 0, 0);
+}
+
 
 /////  Miscellaneous system calls /////
@@ -799,9 +711,9 @@
 // The task is blocked, but it still consume processor cycles ...
 //////////////////////////////////////////////////////////////////////////////////
-void giet_exit()
-{
-    sys_call(SYSCALL_EXIT, 
-             0, 0, 0, 0);
-}
+void giet_exit() {
+    sys_call(SYSCALL_EXIT, 0, 0, 0, 0);
+}
+
+
 ///////////////////////////////////////////////////////////////////////////////////
 // giet_rand()
@@ -809,23 +721,40 @@
 // count. This value is comprised between 0 & 65535.
 ///////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_rand()
-{
-    unsigned int x = sys_call(SYSCALL_PROCTIME, 
-                              0, 0, 0, 0);
-    if((x & 0xF) > 7)
+unsigned int giet_rand() {
+    unsigned int x = sys_call(SYSCALL_PROCTIME, 0, 0, 0, 0);
+    if ((x & 0xF) > 7) {
         return (x*x & 0xFFFF);
-    else
+    }
+    else {
         return (x*x*x & 0xFFFF);
-}
-//////////////////////////////////////////////////////////////////////////////////
-// giet_ctx_switch()
+    }
+}
+
+
+//////////////////////////////////////////////////////////////////////////////////
+// giet_context_switch()
 // The user task calling this function is descheduled and
 // the processor is allocated to another task.
 //////////////////////////////////////////////////////////////////////////////////
-unsigned int giet_ctx_switch()
-{
-    return sys_call(SYSCALL_CTX_SWITCH, 
-                    0, 0, 0, 0);
-}
-
-
+unsigned int giet_context_switch() {
+    return sys_call(SYSCALL_CTX_SWITCH, 0, 0, 0, 0);
+}
+
+//////////////////////////////////////////////////////////////////////////////////
+// giet_get_task_id()
+// The user task calling this function is descheduled and
+// the processor is allocated to another task.
+//////////////////////////////////////////////////////////////////////////////////
+unsigned int giet_task_id() {
+    return sys_call(SYSCALL_TASK_ID, 0, 0, 0, 0);
+}
+
+
+// Local Variables:
+// tab-width: 4
+// c-basic-offset: 4
+// c-file-offsets:((innamespace . 0)(inline-open . 0))
+// indent-tabs-mode: nil
+// End:
+// vim: filetype=c:expandtab:shiftwidth=4:tabstop=4:softtabstop=4
+
