Index: soft/giet_vm/giet_kernel/ctx_handler.c
===================================================================
--- soft/giet_vm/giet_kernel/ctx_handler.c	(revision 706)
+++ soft/giet_vm/giet_kernel/ctx_handler.c	(revision 707)
@@ -13,6 +13,4 @@
 #include <tty0.h>
 #include <xcu_driver.h>
-#include <fat32.h>
-#include <elf-types.h>
 
 /////////////////////////////////////////////////////////////////////////////////
@@ -79,158 +77,4 @@
 
 } // end _ctx_kill_task()
-
-
-
-////////////////////////////////////////////////////////////////////////
-static unsigned int _load_writable_segments( mapping_vspace_t*  vspace )
-{
-
-#if GIET_DEBUG_SWITCH 
-unsigned int gpid       = _get_procid();
-unsigned int cluster_xy = gpid >> P_WIDTH;
-unsigned int p          = gpid & ((1<<P_WIDTH)-1);
-unsigned int x          = cluster_xy >> Y_WIDTH;
-unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
-if ( _get_proctime() > GIET_DEBUG_SWITCH )
-_printf("\n[DEBUG SWITCH] P[%d,%d,%d] _load_writable_segments() : enters for %s\n",
-        x , y , p , vspace->name );
-#endif
-
-    mapping_header_t*  header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
-    mapping_vseg_t*    vseg    = _get_vseg_base(header);
-
-    // buffer to store one cluster
-    char  buf[4096];
-
-    // open the .elf file associated to vspace
-    unsigned int      vseg_id;
-    unsigned int      fd = 0;
-    
-    for (vseg_id = vspace->vseg_offset;
-         vseg_id < (vspace->vseg_offset + vspace->vsegs);
-         vseg_id++) 
-    {
-        if(vseg[vseg_id].type == VSEG_TYPE_ELF) 
-        {   
-            fd = _fat_open( vseg[vseg_id].binpath , O_RDONLY ); 
-
-#if GIET_DEBUG_SWITCH
-if ( _get_proctime() > GIET_DEBUG_SWITCH )
-_printf("\n[DEBUG SWITCH] P[%d,%d,%d] _load_writable_segments() : open %s / fd = %d\n",
-        x , y , p , vseg[vseg_id].binpath , fd );
-#endif
-
-            if ( fd < 0 ) return 1;
-            break;
-        }
-    }
-
-    // load Elf-Header into buffer from .elf file
-    if ( _fat_lseek( fd, 0, SEEK_SET ) < 0 ) return 1;
-    if ( _fat_read( fd, buf, 4096 ) < 0 ) return 1;
-
-#if GIET_DEBUG_SWITCH
-if ( _get_proctime() > GIET_DEBUG_SWITCH )
-_printf("\n[DEBUG SWITCH] P[%d,%d,%d] _load_writable_segments() : load Elf-Header\n",
-        x , y , p );
-#endif
-
-    // get nsegments and Program-Header-Table offset from Elf-Header
-    Elf32_Ehdr*  elf_header_ptr = (Elf32_Ehdr*)buf;
-    unsigned int offset         = elf_header_ptr->e_phoff;
-    unsigned int nsegments      = elf_header_ptr->e_phnum;
-
-    // load Program-Header-Table from .elf file
-    if ( _fat_lseek( fd, offset, SEEK_SET ) < 0 ) return 1;
-    if ( _fat_read( fd, buf, 4096 ) < 0 ) return 1;
-
-#if GIET_DEBUG_SWITCH
-if ( _get_proctime() > GIET_DEBUG_SWITCH )
-_printf("\n[DEBUG SWITCH] P[%d,%d,%d] _load_writable_segments() : "
-        "load Program-Header-Table\n", x , y , p );
-#endif
-
-    // set Program-Header-Table pointer 
-    Elf32_Phdr*  elf_pht_ptr = (Elf32_Phdr*)buf;
-    
-    // scan segments to  load all loadable & writable segments
-    unsigned int seg_id;
-    for (seg_id = 0 ; seg_id < nsegments ; seg_id++)
-    {
-        if ( (elf_pht_ptr[seg_id].p_type == PT_LOAD) &&    // loadable
-             (elf_pht_ptr[seg_id].p_flags & PF_W) )        // writable
-        {
-            // Get segment attributes
-            unsigned int seg_vaddr  = elf_pht_ptr[seg_id].p_vaddr;
-            unsigned int seg_offset = elf_pht_ptr[seg_id].p_offset;
-            unsigned int seg_size   = elf_pht_ptr[seg_id].p_filesz;
-
-            // load the segment
-            if ( _fat_lseek( fd, seg_offset, SEEK_SET ) < 0 ) return 1;
-            if ( _fat_read( fd, (void*)seg_vaddr, seg_size ) < 0 ) return 1;
-
-#if GIET_DEBUG_SWITCH
-if ( _get_proctime() > GIET_DEBUG_SWITCH )
-_printf("\n[DEBUG SWITCH] P[%d,%d,%d] _load_writable_segments() : load segment %x\n",
-        x , y , p , seg_vaddr );
-#endif
-
-        }
-    }  // end loop on writable & loadable segments
-
-    // close .elf file
-    _fat_close( fd );
-
-    return 0;
-}  // end load_writable_segments()
-                             
-
-
-///////////////////////////////////////////////
-static void _ctx_exec_task( unsigned int ltid )
-{
-    // get pointers in mapping
-    mapping_header_t * header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
-    mapping_task_t   * task    = _get_task_base(header);
-    mapping_vseg_t   * vseg    = _get_vseg_base(header);
-    mapping_vspace_t * vspace  = _get_vspace_base(header);
-
-    // get scheduler address for processor running the calling task
-    static_scheduler_t* psched = (static_scheduler_t*)_get_sched();
-
-    // get global task index, vspace index, and stack vseg index
-    unsigned int task_id       = psched->context[ltid][CTX_GTID_ID];
-    unsigned int vspace_id     = psched->context[ltid][CTX_VSID_ID];
-    unsigned int vseg_id       = task[task_id].stack_vseg_id;
-
-#if GIET_DEBUG_SWITCH 
-unsigned int gpid       = _get_procid();
-unsigned int cluster_xy = gpid >> P_WIDTH;
-unsigned int p          = gpid & ((1<<P_WIDTH)-1);
-unsigned int x          = cluster_xy >> Y_WIDTH;
-unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
-if ( _get_proctime() > GIET_DEBUG_SWITCH )
-_printf("\n[DEBUG SWITCH] P[%d,%d,%d] _ctx_exec_task() : enters for %s\n",
-        x , y , p , task[task_id].name );
-#endif
-
-    // reload writable segments
-    if ( _load_writable_segments( &vspace[vspace_id] ) )
-    {
-         _printf("[GIET ERROR] in _ctx_exec_task() for task %s\n",
-                 task[task_id].name );
-         return;
-    } 
-
-    // find initial stack pointer
-    unsigned int sp_value      = vseg[vseg_id].vbase + vseg[vseg_id].length;
-
-    // reset task context: RA / SR / SP / EPC / NORUN
-    psched->context[ltid][CTX_RA_ID]    = (unsigned int)&_ctx_eret;
-    psched->context[ltid][CTX_SR_ID]    = GIET_SR_INIT_VALUE;
-    psched->context[ltid][CTX_SP_ID]    = sp_value;
-    psched->context[ltid][CTX_EPC_ID]   = psched->context[ltid][CTX_ENTRY_ID];
-    psched->context[ltid][CTX_NORUN_ID] = 0;
-}
 
 
@@ -302,13 +146,4 @@
         }
 
-        // this task needs to be executed
-        if ( psched->context[next_task_id][CTX_SIG_ID] & SIG_MASK_EXEC )
-        {
-            // acknowledge signal
-            _atomic_and( &psched->context[next_task_id][CTX_SIG_ID], ~SIG_MASK_EXEC );
-
-            _ctx_exec_task( next_task_id );
-        }
-
         // test if the task is runable
         if ( psched->context[next_task_id][CTX_NORUN_ID] == 0 ) 
