Index: soft/giet_vm/giet_kernel/sys_handler.c
===================================================================
--- soft/giet_vm/giet_kernel/sys_handler.c	(revision 629)
+++ soft/giet_vm/giet_kernel/sys_handler.c	(revision 648)
@@ -206,4 +206,163 @@
 };
 
+
+//////////////////////////////////////////////////////////////////////////////
+//           Applications related syscall handlers 
+//////////////////////////////////////////////////////////////////////////////
+
+///////////////////////////////////////
+int _sys_kill_application( char* name )
+{
+    mapping_header_t * header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
+    mapping_vspace_t * vspace  = _get_vspace_base(header);
+    mapping_task_t   * task    = _get_task_base(header);
+
+    unsigned int vspace_id;
+    unsigned int task_id;
+    unsigned int y_size = header->y_size;
+
+#if GIET_DEBUG_EXEC
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] enters _sys_kill_application() for %s\n", name );
+#endif
+
+    // scan vspaces
+    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
+    {
+        if ( _strcmp( vspace[vspace_id].name, name ) == 0 ) 
+        {
+            // check if pplication can be killed
+            if ( vspace[vspace_id].active ) return -2;
+
+            // scan tasks in vspace
+            for (task_id = vspace[vspace_id].task_offset; 
+                 task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks); 
+                 task_id++) 
+            {
+                unsigned int cid   = task[task_id].clusterid;
+                unsigned int x     = cid / y_size;
+                unsigned int y     = cid % y_size;
+                unsigned int p     = task[task_id].proclocid;
+                unsigned int ltid  = task[task_id].ltid;
+
+                // get scheduler pointer for processor running the task
+                static_scheduler_t* psched  = (static_scheduler_t*)_schedulers[x][y][p];
+
+                // release private TTY peripheral if required
+                if ( psched->context[ltid][CTX_TTY_ID] < NB_TTY_CHANNELS ) 
+                {
+                    psched->context[ltid][CTX_TTY_ID] = 0xFFFFFFFF;
+                    _atomic_increment( &_tty_channel_allocator , 0xFFFFFFFF );
+                }
+
+                // set NORUN_MASK_TASK bit
+                unsigned int*       ptr     = &psched->context[ltid][CTX_NORUN_ID];
+                _atomic_or( ptr , NORUN_MASK_TASK );
+            } 
+
+#if GIET_DEBUG_EXEC 
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] exit _sys_kill_application() : %s desactivated\n", name );
+#endif
+
+            return 0;
+        }
+    } 
+
+#if GIET_DEBUG_EXEC 
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] exit _sys_kill_application() : %s not found\n", name );
+#endif
+
+    return -1;    // not found 
+
+}  // end _sys_kill_application()
+    
+///////////////////////////////////////
+int _sys_exec_application( char* name )
+{
+    mapping_header_t * header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
+    mapping_vspace_t * vspace  = _get_vspace_base(header);
+    mapping_task_t   * task    = _get_task_base(header);
+    mapping_vseg_t   * vseg    = _get_vseg_base(header);
+
+    unsigned int vspace_id;
+    unsigned int task_id;
+    unsigned int vseg_id;
+
+    unsigned int y_size = header->y_size;
+
+#if GIET_DEBUG_EXEC 
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] enters _sys_exec_application() at cycle %d for %s\n",
+         _get_proctime() , name );
+#endif
+
+    // scan vspaces
+    for (vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++) 
+    {
+        if ( _strcmp( vspace[vspace_id].name, name ) == 0 ) 
+        {
+            // scan tasks in vspace
+            for (task_id = vspace[vspace_id].task_offset; 
+                 task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks); 
+                 task_id++) 
+            {
+                unsigned int cid   = task[task_id].clusterid;
+                unsigned int x     = cid / y_size;
+                unsigned int y     = cid % y_size;
+                unsigned int p     = task[task_id].proclocid;
+                unsigned int ltid  = task[task_id].ltid;
+
+                // get scheduler pointer for the processor running the task
+                static_scheduler_t* psched  = (static_scheduler_t*)_schedulers[x][y][p];
+
+                // sp_value : initial stack pointer 
+                vseg_id = task[task_id].stack_vseg_id;
+                unsigned int sp_value = vseg[vseg_id].vbase + vseg[vseg_id].length;
+
+                // epc value : task entry point
+                unsigned int  epc_value = psched->context[ltid][CTX_ENTRY_ID];
+
+                // ra_value : initial return address
+                unsigned int ra_value = (unsigned int)(&_ctx_eret);
+
+                // initialise task context: RA / SR / EPC / SP / NORUN slots
+                psched->context[ltid][CTX_RA_ID]    = ra_value;
+                psched->context[ltid][CTX_SR_ID]    = GIET_SR_INIT_VALUE;
+                psched->context[ltid][CTX_SP_ID]    = sp_value;
+                psched->context[ltid][CTX_EPC_ID]   = epc_value;
+                psched->context[ltid][CTX_NORUN_ID] = 0;
+
+#if GIET_DEBUG_EXEC 
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] _sys_exec_application() start task %d on P[%d,%d,%d]\n"
+        " - ctx_ra    = %x\n"
+        " - ctx_sp    = %x\n"
+        " - ctx_epc   = %x\n",
+        task_id , x , y , p , ra_value , sp_value , epc_value );
+#endif
+            } 
+
+#if GIET_DEBUG_EXEC 
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] exit _sys_exec_application() at cycle %d : %s activated\n",
+        _get_proctime() , name );
+#endif
+
+            return 0;   // application found and activated
+        }
+    }
+
+#if GIET_DEBUG_EXEC 
+if ( _get_proctime() > GIET_DEBUG_EXEC )
+_printf("\n[DEBUG EXEC] exit _sys_exec_application() at cycle %d : %s not found\n",
+         _get_proctime() , name );
+#endif
+
+    return -1;    // not found 
+
+}  // end _sys_exec_application()
+    
 
 //////////////////////////////////////////////////////////////////////////////
@@ -624,10 +783,11 @@
     if ( channel >= NB_TTY_CHANNELS )
     {
+        _atomic_increment( &_tty_channel_allocator , 0xFFFFFFFF );
         _printf("\n[GIET_ERROR] in _sys_tty_alloc() : not enough TTY channels\n");
         return -1;
     }
-    else
-    {
-    }
+
+    // reset kernel buffer for allocated TTY channel
+    _tty_rx_full[channel] = 0;
 
     // allocate a WTI mailbox to the calling proc if external IRQ
@@ -1425,9 +1585,9 @@
 
 
-////////////////////////
-int _sys_fbf_cma_init_buf(void*        buf0_vbase, 
-                          void*        buf1_vbase, 
-                          void*        sts0_vaddr,
-                          void*        sts1_vaddr )
+///////////////////////////////////////////////////
+int _sys_fbf_cma_init_buf( void*        buf0_vbase, 
+                           void*        buf1_vbase, 
+                           void*        sts0_vaddr,
+                           void*        sts1_vaddr )
 {
 #if NB_CMA_CHANNELS > 0
@@ -1447,5 +1607,5 @@
     if ( channel >= NB_CMA_CHANNELS )
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_init_buf() : CMA channel index too large\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : CMA channel index too large\n");
         return -1;
     }
@@ -1469,5 +1629,5 @@
          ((unsigned int)buf1_vbase & 0x3F) ) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_inti_buf() : user buffer not aligned\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : user buffer not aligned\n");
         return -1;
     }
@@ -1477,5 +1637,5 @@
          ((unsigned int)sts1_vaddr & 0x3F) )
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_init_buf() : user buffer status not aligned\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : user status not aligned\n");
         return -1;
     }
@@ -1496,5 +1656,5 @@
     if ((flags & PTE_U) == 0) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : buf0 not in user space\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : buf0 not in user space\n");
         return -1;
     }
@@ -1504,5 +1664,5 @@
     if ((flags & PTE_U) == 0) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : sts0 not in user space\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : sts0 not in user space\n");
         return -1;
     }
@@ -1517,5 +1677,5 @@
     if ((flags & PTE_U) == 0) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : buf1 not in user space\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : buf1 not in user space\n");
         return -1;
     }
@@ -1525,5 +1685,5 @@
     if ((flags & PTE_U) == 0) 
     {
-        _printf("\n[GIET ERROR] in _fbf_cma_start() : sts1 not in user space\n");
+        _printf("\n[GIET ERROR] in _sys_fbf_cma_init_buf() : sts1 not in user space\n");
         return -1;
     }
@@ -1696,5 +1856,5 @@
     while ( full )
     {  
-        // INVAL L2 cache copy of user buffer descriptor,
+        // INVAL L2 cache copy of user buffer status     
         // because it has been modified in RAM by the CMA component 
         _mmc_inval( buf_sts_paddr , 4 );        
@@ -1810,101 +1970,4 @@
 } 
 
-///////////////////////////////////////
-int _sys_kill_application( char* name )
-{
-    mapping_header_t * header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
-    mapping_vspace_t * vspace  = _get_vspace_base(header);
-    mapping_task_t   * task    = _get_task_base(header);
-
-    unsigned int vspace_id;
-    unsigned int task_id;
-    unsigned int y_size = header->y_size;
-
-    // scan vspaces
-    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
-    {
-        if ( _strcmp( vspace[vspace_id].name, name ) == 0 ) 
-        {
-            // scan tasks in vspace
-            for (task_id = vspace[vspace_id].task_offset; 
-                 task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks); 
-                 task_id++) 
-            {
-                unsigned int cid   = task[task_id].clusterid;
-                unsigned int x     = cid / y_size;
-                unsigned int y     = cid % y_size;
-                unsigned int p     = task[task_id].proclocid;
-                unsigned int ltid  = task[task_id].ltid;
-
-                // set NORUN_MASK_TASK bit
-                static_scheduler_t* psched  = (static_scheduler_t*)_schedulers[x][y][p];
-                unsigned int*       ptr     = &psched->context[ltid][CTX_NORUN_ID];
-                _atomic_or( ptr , NORUN_MASK_TASK );
-            } 
-            return 0;
-        }
-    } 
-    return -1;    // not found 
-}
-    
-///////////////////////////////////////
-int _sys_exec_application( char* name )
-{
-    mapping_header_t * header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
-    mapping_vspace_t * vspace  = _get_vspace_base(header);
-    mapping_task_t   * task    = _get_task_base(header);
-    mapping_vseg_t   * vseg    = _get_vseg_base(header);
-
-    unsigned int vspace_id;
-    unsigned int task_id;
-    unsigned int vseg_id;
-
-    unsigned int y_size = header->y_size;
-
-    // scan vspaces
-    for (vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++) 
-    {
-        if ( _strcmp( vspace[vspace_id].name, name ) == 0 ) 
-        {
-            // scan tasks in vspace
-            for (task_id = vspace[vspace_id].task_offset; 
-                 task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks); 
-                 task_id++) 
-            {
-                unsigned int cid   = task[task_id].clusterid;
-                unsigned int x     = cid / y_size;
-                unsigned int y     = cid % y_size;
-                unsigned int p     = task[task_id].proclocid;
-                unsigned int ltid  = task[task_id].ltid;
-
-                // compute stack pointer value (sp_value)
-                vseg_id = task[task_id].stack_vseg_id;
-                unsigned int sp_value = vseg[vseg_id].vbase + vseg[vseg_id].length;
-
-                // compute task entry point value (epc_value)
-                vseg_id = vspace[vspace_id].start_vseg_id;     
-                unsigned int* vaddr = (unsigned int*)( vseg[vseg_id].vbase + 
-                                                       ((task[task_id].startid)<<2) );
-                unsigned int  epc_value = *vaddr;
-
-                // compute reurn address value (ra_value)
-                unsigned int ra_value = (unsigned int)(&_ctx_eret);
-
-                // get scheduler pointer 
-                static_scheduler_t* psched  = (static_scheduler_t*)_schedulers[x][y][p];
-
-                // initialise task context: RA / SR / EPC / SP / NORUN slots
-                psched->context[ltid][CTX_RA_ID]    = ra_value;
-                psched->context[ltid][CTX_SR_ID]    = GIET_SR_INIT_VALUE;
-                psched->context[ltid][CTX_SP_ID]    = sp_value;
-                psched->context[ltid][CTX_EPC_ID]   = epc_value;
-                psched->context[ltid][CTX_NORUN_ID] = 0;
-            } 
-            return 0;
-        }
-    }
-    return -1;    // not found 
-}
-    
 /////////////////////////
 int _sys_context_switch() 
