source: soft/giet_vm/giet_boot/boot.c @ 441

/////////////////////////////////////////////////////////////////////////////////////////
// File     : boot.c
// Date     : 01/11/2013
// Author   : alain greiner
// Copyright (c) UPMC-LIP6
//////////////////////////////////////////////////////////////////////////////////////////
// The boot.c file is part of the GIET-VM nano-kernel.
//
// This nano-kernel has been written for the MIPS32 processor.
// The virtual adresses are on 32 bits and use the (unsigned int) type. The 
// physicals addresses can have up to 40 bits, and use the  (unsigned long long) type.
// It natively supports clusterised shared memory multi-processors architectures, 
// where each processor is identified by a composite index (cluster_xy, local_id),
// and where there is one physical memory bank per cluster.
//
// This code, executed in the boot phase by proc[0,0,0], performs the following tasks:
// - load into memory various binary files, from a FAT32 file system,
// - build the various page tables (one page table per vspace) 
// - initialize the shedulers (one scheduler per processor)
//
// 1) The binary files to be loaded are:
//    - the "map.bin" file contains the hardware architecture description and the
//      mapping directives. It must be stored in the the seg_boot_mapping segment 
//      (at address SEG_BOOT_MAPPING_BASE defined in hard_config.h file).
//    - the "sys.elf" file contains the kernel binary code and data.
//    - the various "application.elf" files.
//
// 2) The map.bin file contains the binary representation of the map.xml file defining: 
//    - the hardware architecture: number of clusters, number or processors, 
//      size of the memory segments, and peripherals in each cluster.
//    - The structure of the various multi-threaded software applications:
//      number of tasks, communication channels.
//    - The mapping: grouping of virtual objects (vobj) in the virtual segments (vseg),
//      placement of virtual segments (vseg) in the physical segments (pseg), placement 
//      of software tasks on the processors, 
//
// 3) The GIET-VM uses the paged virtual memory to provides two services:
//    - classical memory protection, when several independant applications compiled
//      in different virtual spaces are executing on the same hardware platform.
//    - data placement in NUMA architectures, to control the placement 
//      of the software objects (vsegs) on the physical memory banks (psegs).
//
//    The max number of vspaces (GIET_NB_VSPACE_MAX) is a configuration parameter.
//    The page table are statically build in the boot phase, and they do not 
//    change during execution. 
//    The GIET_VM uses both small pages (4 Kbytes), and big pages (2 Mbytes). 
//
//    Each page table (one page table per virtual space) is monolithic, and contains 
//    one PT1 (8 Kbytes) and a variable number of PT2s (4 Kbytes each). For each vspace,
//    the numberof PT2s is defined by the size of the PTAB vobj in the mapping.
//    The PT1 is indexed by the ix1 field (11 bits) of the VPN. Each entry is 32 bits.
//    A PT2 is indexed the ix2 field (9 bits) of the VPN. Each entry is a double word. 
//    The first word contains the flags, the second word contains the PPN.
//
//    The page tables can be distributed in all clusters.
///////////////////////////////////////////////////////////////////////////////////////
// Implementation Notes:
//
// 1) The cluster_id variable is a linear index in the mapping_info array of clusters. 
//    We use the cluster_xy variable for the tological index = x << Y_WIDTH + y
// 
///////////////////////////////////////////////////////////////////////////////////////

#include <giet_config.h>
#include <mapping_info.h>
#include <mwmr_channel.h>
#include <barrier.h>
#include <memspace.h>
#include <tty_driver.h>
#include <xcu_driver.h>
#include <bdv_driver.h>
#include <dma_driver.h>
#include <cma_driver.h>
#include <nic_driver.h>
#include <ioc_driver.h>
#include <iob_driver.h>
#include <pic_driver.h>
#include <mwr_driver.h>
#include <ctx_handler.h>
#include <irq_handler.h>
#include <vmem.h>
#include <pmem.h>
#include <utils.h>
#include <elf-types.h>

// for boot FAT initialisation 
#include <fat32.h>

#include <mips32_registers.h>
#include <stdarg.h>

#if !defined(X_SIZE)
# error: The X_SIZE value must be defined in the 'hard_config.h' file !
#endif

#if !defined(Y_SIZE)
# error: The Y_SIZE value must be defined in the 'hard_config.h' file !
#endif

#if !defined(X_WIDTH)
# error: The X_WIDTH value must be defined in the 'hard_config.h' file !
#endif

#if !defined(Y_WIDTH)
# error: The Y_WIDTH value must be defined in the 'hard_config.h' file !
#endif

#if !defined(SEG_BOOT_MAPPING_BASE) 
# error: The SEG_BOOT_MAPPING_BASE value must be defined in the hard_config.h file !
#endif

#if !defined(NB_PROCS_MAX)
# error: The NB_PROCS_MAX value must be defined in the 'hard_config.h' file !
#endif

#if !defined(GIET_NB_VSPACE_MAX)
# error: The GIET_NB_VSPACE_MAX value must be defined in the 'giet_config.h' file !
#endif

#if !defined(GIET_ELF_BUFFER_SIZE) 
# error: The GIET_ELF_BUFFER_SIZE value must be defined in the giet_config.h file !
#endif

////////////////////////////////////////////////////////////////////////////
//      Global variables for boot code
////////////////////////////////////////////////////////////////////////////

extern void boot_entry();

// FAT internal representation for boot code  
__attribute__((section (".bootdata"))) 
fat32_fs_t             fat   __attribute__((aligned(512)));

// Temporaty buffer used to load one complete .elf file  
__attribute__((section (".bootdata"))) 
char                   boot_elf_buffer[GIET_ELF_BUFFER_SIZE] __attribute__((aligned(512)));

// Physical memory allocators array (one per cluster)
__attribute__((section (".bootdata"))) 
pmem_alloc_t           boot_pmem_alloc[X_SIZE][Y_SIZE];

// Schedulers virtual base addresses array (one per processor)
__attribute__((section (".bootdata"))) 
static_scheduler_t*    _schedulers[X_SIZE][Y_SIZE][NB_PROCS_MAX];

// Page tables virtual base addresses array (one per vspace)
__attribute__((section (".bootdata"))) 
unsigned int           _ptabs_vaddr[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE];

// Page tables physical base addresses (one per vspace and per cluster)
__attribute__((section (".bootdata"))) 
paddr_t                _ptabs_paddr[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE];

// Page tables pt2 allocators (one per vspace and per cluster)
__attribute__((section (".bootdata"))) 
unsigned int           _ptabs_next_pt2[GIET_NB_VSPACE_MAX][X_SIZE][Y_SIZE];

// Page tables max_pt2  (same value for all page tables)
__attribute__((section (".bootdata"))) 
unsigned int           _ptabs_max_pt2;

/////////////////////////////////////////////////////////////////////
// This function checks consistence beween the  mapping_info data 
// structure (soft), and the giet_config file (hard).
/////////////////////////////////////////////////////////////////////
void boot_mapping_check() 
{
    mapping_header_t * header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;

    // checking mapping availability
    if (header->signature != IN_MAPPING_SIGNATURE) 
    {
        _puts("\n[BOOT ERROR] Illegal mapping signature: ");
        _putx(header->signature);
        _puts("\n");
        _exit();
    }

    // checking number of clusters
    if ( (header->x_size  != X_SIZE)  || 
         (header->y_size  != Y_SIZE)  ||
         (header->x_width != X_WIDTH) ||
         (header->y_width != Y_WIDTH) )
    {
        _puts("\n[BOOT ERROR] Incoherent X_SIZE or Y_SIZE ");
        _puts("\n             - In hard_config:  X_SIZE = ");
        _putd( X_SIZE );
        _puts(" / Y_SIZE = ");
        _putd( Y_SIZE );
        _puts(" / X_WIDTH = ");
        _putd( X_WIDTH );
        _puts(" / Y_WIDTH = ");
        _putd( Y_WIDTH );
        _puts("\n             - In mapping_info: x_size = ");
        _putd( header->x_size );
        _puts(" / y_size = ");
        _putd( header->y_size );
        _puts(" / x_width = ");
        _putd( header->x_width );
        _puts(" / y_width = ");
        _putd( header->y_width );
        _puts("\n");
        _exit();
    }
    // checking number of virtual spaces
    if (header->vspaces > GIET_NB_VSPACE_MAX) 
    {
        _puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
        _puts("\n");
        _exit();
    }

#if BOOT_DEBUG_MAPPING
_puts("\n - x_size    = ");
_putd( header->x_size );
_puts("\n - y_size    = ");
_putd( header->y_size );
_puts("\n - procs     = ");
_putd( header->procs );
_puts("\n - periphs   = ");
_putd( header->periphs );
_puts("\n - vspaces   = ");
_putd( header->vspaces );
_puts("\n - tasks     = ");
_putd( header->tasks );
_puts("\n");
_puts("\n - size of header  = ");
_putd( MAPPING_HEADER_SIZE );
_puts("\n - size of cluster = ");
_putd( MAPPING_CLUSTER_SIZE );
_puts("\n - size of pseg    = ");
_putd( MAPPING_PSEG_SIZE );
_puts("\n - size of proc    = ");
_putd( MAPPING_PROC_SIZE );
_puts("\n - size of vspace  = ");
_putd( MAPPING_VSPACE_SIZE );
_puts("\n - size of vseg    = ");
_putd( MAPPING_VSEG_SIZE );
_puts("\n - size of vobj    = ");
_putd( MAPPING_VOBJ_SIZE );
_puts("\n - size of task    = ");
_putd( MAPPING_TASK_SIZE );
_puts("\n");

unsigned int cluster_id;
mapping_cluster_t * cluster = _get_cluster_base(header);
for( cluster_id = 0; cluster_id < X_SIZE*Y_SIZE ; cluster_id++) 
{
    _puts("\n - cluster[");
    _putd( cluster[cluster_id].x );
    _puts(",");
    _putd( cluster[cluster_id].y );
    _puts("]\n   procs   = ");
    _putd( cluster[cluster_id].procs );
    _puts("\n   psegs   = ");
    _putd( cluster[cluster_id].psegs );
    _puts("\n   periphs = ");
    _putd( cluster[cluster_id].periphs );
    _puts("\n");
}
#endif

} // end boot_mapping_check()

//////////////////////////////////////////////////////////////////////////////
// This function registers a new PTE1 in the page table defined
// by the vspace_id argument, and the (x,y) coordinates.
// It updates only the first level PT1.
//////////////////////////////////////////////////////////////////////////////
void boot_add_pte1( unsigned int vspace_id,
                    unsigned int x,
                    unsigned int y,
                    unsigned int vpn,        // 20 bits right-justified
                    unsigned int flags,      // 10 bits left-justified 
                    unsigned int ppn )       // 28 bits right-justified
{

#if (BOOT_DEBUG_PT > 1)
_puts(" - PTE1 in PTAB[");
_putd( vspace_id );
_puts(",");
_putd( x );
_puts(",");
_putd( y );
_puts("] : vpn = ");
_putx( vpn );
#endif

    // compute index in PT1
    unsigned int    ix1 = vpn >> 9;         // 11 bits for ix1

    // get page table physical base address 
    paddr_t         pt1_pbase = _ptabs_paddr[vspace_id][x][y];

    // check pt1_base
    if ( pt1_pbase == 0 )
    {
        _puts("\n[BOOT ERROR] in boot_add_pte1() : illegal pbase address for PTAB[");
        _putd( vspace_id );
        _puts(",");
        _putd( x );
        _puts(",");
        _putd( y );
        _puts("]\n");
        _exit();
    }

    // compute pte1 : 2 bits V T / 8 bits flags / 3 bits RSVD / 19 bits bppi
    unsigned int    pte1 = PTE_V |
                           (flags & 0x3FC00000) |
                           ((ppn>>9) & 0x0007FFFF);

    // write pte1 in PT1
    _physical_write( pt1_pbase + 4*ix1, pte1 );

#if (BOOT_DEBUG_PT > 1)
_puts(" / ppn = ");
_putx( ppn );
_puts(" / flags = ");
_putx( flags );
_puts("\n");
#endif

}   // end boot_add_pte1()

//////////////////////////////////////////////////////////////////////////////
// This function registers a new PTE2 in the page table defined
// by the vspace_id argument, and the (x,y) coordinates.
// It updates both the first level PT1 and the second level PT2.
// As the set of PT2s is implemented as a fixed size array (no dynamic 
// allocation), this function checks a possible overflow of the PT2 array.
//////////////////////////////////////////////////////////////////////////////
void boot_add_pte2( unsigned int vspace_id,
                    unsigned int x,
                    unsigned int y,
                    unsigned int vpn,        // 20 bits right-justified
                    unsigned int flags,      // 10 bits left-justified 
                    unsigned int ppn )       // 28 bits right-justified
{

#if (BOOT_DEBUG_PT > 1)
_puts(" - PTE2 in PTAB[");
_putd( vspace_id );
_puts(",");
_putd( x );
_puts(",");
_putd( y );
_puts("] : vpn = ");
_putx( vpn );
#endif

    unsigned int ix1;
    unsigned int ix2;
    paddr_t      pt2_pbase;     // PT2 physical base address
    paddr_t      pte2_paddr;    // PTE2 physical address
    unsigned int pt2_id;        // PT2 index
    unsigned int ptd;           // PTD : entry in PT1

    ix1 = vpn >> 9;             // 11 bits for ix1
    ix2 = vpn & 0x1FF;          //  9 bits for ix2

    // get page table physical base address and size
    paddr_t      pt1_pbase = _ptabs_paddr[vspace_id][x][y];

    // check pt1_base
    if ( pt1_pbase == 0 )
    {
        _puts("\n[BOOT ERROR] in boot_add_pte2() : PTAB[");
        _putd( vspace_id );
        _puts(",");
        _putd( x );
        _puts(",");
        _putd( y );
        _puts("] undefined\n");
        _exit();
    }

    // get ptd in PT1
    ptd = _physical_read(pt1_pbase + 4 * ix1);

    if ((ptd & PTE_V) == 0)    // undefined PTD: compute PT2 base address, 
                               // and set a new PTD in PT1 
    {
        pt2_id = _ptabs_next_pt2[vspace_id][x][y];
        if (pt2_id == _ptabs_max_pt2) 
        {
            _puts("\n[BOOT ERROR] in boot_add_pte2() : PTAB[");
            _putd( vspace_id );
            _puts(",");
            _putd( x );
            _puts(",");
            _putd( y );
            _puts("] contains not enough PT2s\n");
            _exit();
        }

        pt2_pbase = pt1_pbase + PT1_SIZE + PT2_SIZE * pt2_id;
        ptd = PTE_V | PTE_T | (unsigned int) (pt2_pbase >> 12);
        _physical_write( pt1_pbase + 4*ix1, ptd);
        _ptabs_next_pt2[vspace_id][x][y] = pt2_id + 1;
    }
    else                       // valid PTD: compute PT2 base address
    {
        pt2_pbase = ((paddr_t)(ptd & 0x0FFFFFFF)) << 12;
    }

    // set PTE in PT2 : flags & PPN in two 32 bits words
    pte2_paddr  = pt2_pbase + 8 * ix2;
    _physical_write(pte2_paddr     , (PTE_V |flags) );
    _physical_write(pte2_paddr + 4 , ppn);

#if (BOOT_DEBUG_PT > 1)
_puts(" / ppn = ");
_putx( ppn );
_puts(" / flags = ");
_putx( flags );
_puts("\n");
#endif

}   // end boot_add_pte2()

////////////////////////////////////////////////////////////////////////////////////
// Align the value of paddr or vaddr to the required alignement,
// defined by alignPow2 == L2(alignement).
////////////////////////////////////////////////////////////////////////////////////
paddr_t paddr_align_to(paddr_t paddr, unsigned int alignPow2) 
{
    paddr_t mask = (1 << alignPow2) - 1;
    return ((paddr + mask) & ~mask);
}

unsigned int vaddr_align_to(unsigned int vaddr, unsigned int alignPow2) 
{
    unsigned int mask = (1 << alignPow2) - 1;
    return ((vaddr + mask) & ~mask);
}

/////////////////////////////////////////////////////////////////////////////////////
// This function map a vseg identified by the vseg pointer.
//
// A given vseg can be mapped in Big Physical Pages (BPP: 2 Mbytes) or in a
// Small Physical Pages (SPP: 4 Kbytes), depending on the "big" attribute of vseg,
// with the following rules:
// - SPP : There is only one vseg in a small physical page, but a single vseg
//   can cover several contiguous small physical pages.
// - BPP : It can exist several vsegs in a single big physical page, and a single
//   vseg can cover several contiguous big physical pages.
//
// 1) First step: it computes the vseg length, and register it in vseg->length field.
//    It computes - for each vobj - the actual vbase address, taking into
//    account the alignment constraints and register it in vobj->vbase field.
//
// 2) Second step: it allocates the required number of physical pages, 
//    computes the physical base address (if the vseg is not identity mapping),
//    and register it in the vseg pbase field.
//    Only the 4 vsegs used by the boot code and the peripheral vsegs
//    can be identity mapping: The first big physical page in cluster[0,0] 
//    is reserved for the 4 boot vsegs.
//
// 3) Third step (only for vseg that have the VOBJ_TYPE_PTAB): all page tables
//    associated to the various vspaces must be packed in the same vseg.
//    We divide the vseg in M sub-segments, and compute the vbase and pbase
//    addresses for each page table, and register it in the _ptabs_paddr
//    and _ptabs_vaddr arrays.
//  
/////////////////////////////////////////////////////////////////////////////////////
void boot_vseg_map( mapping_vseg_t* vseg,
                    unsigned int    vspace_id )
{
    mapping_header_t*   header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_vobj_t*     vobj    = _get_vobj_base(header);
    mapping_cluster_t*  cluster = _get_cluster_base(header);
    mapping_pseg_t*     pseg    = _get_pseg_base(header);

    // compute destination cluster pointer & coordinates
    pseg    = pseg + vseg->psegid;
    cluster = cluster + pseg->clusterid;
    unsigned int        x_dest     = cluster->x;
    unsigned int        y_dest     = cluster->y;

    // compute the first vobj global index
    unsigned int        vobj_id = vseg->vobj_offset;
    
    // compute the "big" vseg attribute
    unsigned int        big = vseg->big;

    // compute the "is_ram" vseg attribute
    unsigned int        is_ram;
    if ( pseg->type == PSEG_TYPE_RAM )  is_ram = 1;
    else                                is_ram = 0;

    // compute the "is_ptab" attribute
    unsigned int        is_ptab;
    if ( vobj[vobj_id].type == VOBJ_TYPE_PTAB ) is_ptab = 1;
    else                                        is_ptab = 0;

    // compute actual vspace index
    unsigned int vsid;
    if ( vspace_id == 0xFFFFFFFF ) vsid = 0;
    else                           vsid = vspace_id;

    //////////// First step : compute vseg length and vobj(s) vbase

    unsigned int vobj_vbase = vseg->vbase;   // min vbase for first vobj

    for ( vobj_id = vseg->vobj_offset ;
          vobj_id < (vseg->vobj_offset + vseg->vobjs) ; 
          vobj_id++ ) 
    {
        // compute and register vobj vbase
        vobj[vobj_id].vbase = vaddr_align_to( vobj_vbase, vobj[vobj_id].align );
   
        // compute min vbase for next vobj
        vobj_vbase = vobj[vobj_id].vbase + vobj[vobj_id].length;
    }

    // compute and register vseg length (multiple of 4 Kbytes)
    vseg->length = vaddr_align_to( vobj_vbase - vseg->vbase, 12 );
    
    //////////// Second step : compute ppn and npages  
    //////////// - if identity mapping :  ppn <= vpn 
    //////////// - if vseg is periph   :  ppn <= pseg.base >> 12
    //////////// - if vseg is ram      :  ppn <= physical memory allocator

    unsigned int ppn;          // first physical page index ( 28 bits = |x|y|bppi|sppi| ) 
    unsigned int vpn;          // first virtual page index  ( 20 bits = |ix1|ix2| )
    unsigned int vpn_max;      // last  virtual page index  ( 20 bits = |ix1|ix2| )

    vpn     = vseg->vbase >> 12;
    vpn_max = (vseg->vbase + vseg->length - 1) >> 12;

    // compute npages
    unsigned int npages;       // number of required (big or small) pages
    if ( big == 0 ) npages  = vpn_max - vpn + 1;            // number of small pages
    else            npages  = (vpn_max>>9) - (vpn>>9) + 1;  // number of big pages

    // compute ppn
    if ( vseg->ident )           // identity mapping
    {
        ppn = vpn;
    }
    else                         // not identity mapping
    {
        if ( is_ram )            // RAM : physical memory allocation required
        {
            // compute pointer on physical memory allocator in dest cluster
            pmem_alloc_t*     palloc = &boot_pmem_alloc[x_dest][y_dest];

            if ( big == 0 )             // SPP : small physical pages
            {
                // allocate contiguous small physical pages
                ppn = _get_small_ppn( palloc, npages );
            }
            else                            // BPP : big physical pages
            {
 
                // one big page can be shared by several vsegs 
                // we must chek if BPP already allocated 
                if ( is_ptab )   // It cannot be mapped
                {
                    ppn = _get_big_ppn( palloc, npages ); 
                }
                else             // It can be mapped
                {
                    unsigned int ix1   = vpn >> 9;   // 11 bits
                    paddr_t      paddr = _ptabs_paddr[vsid][x_dest][y_dest] + (ix1<<2);
                    unsigned int pte1  = _physical_read( paddr );
                    if ( (pte1 & PTE_V) == 0 )     // BPP not allocated yet
                    {
                        // allocate contiguous big physical pages 
                        ppn = _get_big_ppn( palloc, npages );
                    }
                    else                           // BPP already allocated
                    {
                        // test if new vseg has the same mode bits than
                        // the other vsegs in the same big page
                        unsigned int pte1_mode = 0;
                        if (pte1 & PTE_C) pte1_mode |= C_MODE_MASK;
                        if (pte1 & PTE_X) pte1_mode |= X_MODE_MASK;
                        if (pte1 & PTE_W) pte1_mode |= W_MODE_MASK;
                        if (pte1 & PTE_U) pte1_mode |= U_MODE_MASK;
                        if (vseg->mode != pte1_mode) {
                            _puts("\n[BOOT ERROR] in boot_vseg_map() : vseg ");
                            _puts( vseg->name );
                            _puts(" has different flags (");
                            _putx( vseg->mode );
                            _puts(") than other vsegs sharing the same big page (");
                            _putx( pte1_mode );
                            _puts(")");
                            _exit();
                        }

                        ppn = ((pte1 << 9) & 0x0FFFFE00);
                    }
                }
                ppn = ppn | (vpn & 0x1FF);
            }
        }
        else                    // PERI : no memory allocation required
        {
            ppn = pseg->base >> 12;
        }
    }

    // update vseg.pbase field and update vsegs chaining
    vseg->pbase     = ((paddr_t)ppn) << 12;
    vseg->next_vseg = pseg->next_vseg;
    pseg->next_vseg = (unsigned int)vseg;


    //////////// Third step : (only if the vseg is a page table)
    //////////// - compute the physical & virtual base address for each vspace
    ////////////   by dividing the vseg in several sub-segments.
    //////////// - register it in _ptabs_vaddr & _ptabs_paddr arrays,
    ////////////   and initialize next_pt2 allocators.
    //////////// - reset all entries in first level page tables
    
    if ( is_ptab )
    {
        unsigned int   vs;        // vspace index
        unsigned int   nspaces;   // number of vspaces
        unsigned int   nsp;       // number of small pages for one PTAB
        unsigned int   offset;    // address offset for current PTAB

        nspaces = header->vspaces;
        offset  = 0;

        // each PTAB must be aligned on a 8 Kbytes boundary
        nsp = ( vseg->length >> 12 ) / nspaces;
        if ( (nsp & 0x1) == 0x1 ) nsp = nsp - 1;

        // compute max_pt2
        _ptabs_max_pt2 = ((nsp<<12) - PT1_SIZE) / PT2_SIZE;

        for ( vs = 0 ; vs < nspaces ; vs++ )
        {
            _ptabs_vaddr   [vs][x_dest][y_dest] = (vpn + offset) << 12;
            _ptabs_paddr   [vs][x_dest][y_dest] = ((paddr_t)(ppn + offset)) << 12;
            _ptabs_next_pt2[vs][x_dest][y_dest] = 0;
            offset += nsp;

            // reset all entries in PT1 (8 Kbytes)
            _physical_memset( _ptabs_paddr[vs][x_dest][y_dest], PT1_SIZE, 0 );
        }
    }

#if BOOT_DEBUG_PT
_puts("[BOOT DEBUG] ");
_puts( vseg->name );
_puts(" in cluster[");
_putd( x_dest );
_puts(",");
_putd( y_dest );
_puts("] : vbase = ");
_putx( vseg->vbase );
_puts(" / length = ");
_putx( vseg->length );
if ( big ) _puts(" / BIG   / npages = ");
else       _puts(" / SMALL / npages = ");
_putd( npages );
_puts(" / pbase = ");
_putl( vseg->pbase );
_puts("\n");
#endif

} // end boot_vseg_map()

/////////////////////////////////////////////////////////////////////////////////////
// For the vseg defined by the vseg pointer, this function register all PTEs
// in one or several page tables.
// It is a global vseg (kernel vseg) if (vspace_id == 0xFFFFFFFF).
// The number of involved PTABs depends on the "local" and "global" attributes:
//  - PTEs are replicated in all vspaces for a global vseg.
//  - PTEs are replicated in all clusters for a non local vseg.
/////////////////////////////////////////////////////////////////////////////////////
void boot_vseg_pte( mapping_vseg_t*  vseg,
                    unsigned int     vspace_id )
{
    // compute the "global" vseg attribute and actual vspace index
    unsigned int        global;
    unsigned int        vsid;    
    if ( vspace_id == 0xFFFFFFFF )
    {
        global = 1;
        vsid   = 0;
    }
    else
    {
        global = 0;
        vsid   = vspace_id;
    }

    // compute the "local" and "big" attributes 
    unsigned int        local  = vseg->local;
    unsigned int        big    = vseg->big;

    // compute vseg flags
    // The three flags (Local, Remote and Dirty) are set to 1 to reduce
    // latency of TLB miss (L/R) and write (D): Avoid hardware update
    // mechanism for these flags because GIET_VM does use these flags.
    unsigned int flags = 0;
    if (vseg->mode & C_MODE_MASK) flags |= PTE_C;
    if (vseg->mode & X_MODE_MASK) flags |= PTE_X;
    if (vseg->mode & W_MODE_MASK) flags |= PTE_W;
    if (vseg->mode & U_MODE_MASK) flags |= PTE_U;
    if ( global )                 flags |= PTE_G;
                                  flags |= PTE_L;
                                  flags |= PTE_R;
                                  flags |= PTE_D;

    // compute VPN, PPN and number of pages (big or small) 
    unsigned int vpn     = vseg->vbase >> 12;
    unsigned int vpn_max = (vseg->vbase + vseg->length - 1) >> 12;
    unsigned int ppn     = (unsigned int)(vseg->pbase >> 12);
    unsigned int npages;
    if ( big == 0 ) npages  = vpn_max - vpn + 1;            
    else            npages  = (vpn_max>>9) - (vpn>>9) + 1; 

    // compute destination cluster coordinates
    unsigned int        x_dest;
    unsigned int        y_dest;
    mapping_header_t*   header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_cluster_t*  cluster = _get_cluster_base(header);
    mapping_pseg_t*     pseg    = _get_pseg_base(header);
    pseg     = pseg + vseg->psegid;
    cluster  = cluster + pseg->clusterid;
    x_dest   = cluster->x;
    y_dest   = cluster->y;

    unsigned int p;     // iterator for physical page index
    unsigned int x;     // iterator for cluster x coordinate  
    unsigned int y;     // iterator for cluster y coordinate  
    unsigned int v;     // iterator for vspace index 

    // loop on PTEs
    for ( p = 0 ; p < npages ; p++ )
    { 
        if  ( (local != 0) && (global == 0) )         // one cluster  / one vspace
        {
            if ( big )   // big pages => PTE1s
            {
                boot_add_pte1( vsid,
                               x_dest,
                               y_dest,
                               vpn + (p<<9),
                               flags, 
                               ppn + (p<<9) );
            }
            else         // small pages => PTE2s
            {
                boot_add_pte2( vsid,
                               x_dest,
                               y_dest,
                               vpn + p,      
                               flags, 
                               ppn + p );
            }
        }
        else if ( (local == 0) && (global == 0) )     // all clusters / one vspace
        {
            for ( x = 0 ; x < X_SIZE ; x++ )
            {
                for ( y = 0 ; y < Y_SIZE ; y++ )
                {
                    if ( big )   // big pages => PTE1s
                    {
                        boot_add_pte1( vsid,
                                       x,
                                       y,
                                       vpn + (p<<9),
                                       flags, 
                                       ppn + (p<<9) );
                    }
                    else         // small pages => PTE2s
                    {
                        boot_add_pte2( vsid,
                                       x,
                                       y,
                                       vpn + p,
                                       flags, 
                                       ppn + p );
                    }
                }
            }
        }
        else if ( (local != 0) && (global != 0) )     // one cluster  / all vspaces 
        {
            for ( v = 0 ; v < header->vspaces ; v++ )
            {
                if ( big )   // big pages => PTE1s
                {
                    boot_add_pte1( v,
                                   x_dest,
                                   y_dest,
                                   vpn + (p<<9),
                                   flags, 
                                   ppn + (p<<9) );
                }
                else         // small pages = PTE2s
                { 
                    boot_add_pte2( v,
                                   x_dest,
                                   y_dest,
                                   vpn + p,
                                   flags, 
                                   ppn + p );
                }
            }
        }
        else if ( (local == 0) && (global != 0) )     // all clusters / all vspaces
        {
            for ( x = 0 ; x < X_SIZE ; x++ )
            {
                for ( y = 0 ; y < Y_SIZE ; y++ )
                {
                    for ( v = 0 ; v < header->vspaces ; v++ )
                    {
                        if ( big )  // big pages => PTE1s
                        {
                            boot_add_pte1( v,
                                           x,
                                           y,
                                           vpn + (p<<9),
                                           flags, 
                                           ppn + (p<<9) );
                        }
                        else        // small pages -> PTE2s
                        {
                            boot_add_pte2( v,
                                           x,
                                           y,
                                           vpn + p,
                                           flags, 
                                           ppn + p );
                        }
                    }
                }
            }
        }
    }  // end for pages
}  // end boot_vseg_pte()

///////////////////////////////////////////////////////////////////////////////
// This function initialises the page tables for all vspaces defined 
// in the mapping_info data structure.
// For each vspace, there is one page table per cluster.
// In each cluster all page tables for the different vspaces must be
// packed in one vseg occupying one single BPP (Big Physical Page).
//
// For each vseg, the mapping is done in two steps:
// 1) mapping : the boot_vseg_map() function allocates contiguous BPPs 
//    or SPPs (if the vseg is not associated to a peripheral), and register
//    the physical base address in the vseg pbase field. It initialises the
//    _ptabs_vaddr and _ptabs_paddr arrays if the vseg is a PTAB.
//
// 2) page table initialisation : the boot_vseg_pte() function initialise 
//    the PTEs (both PTE1 and PTE2) in one or several page tables:
//    - PTEs are replicated in all vspaces for a global vseg.
//    - PTEs are replicated in all clusters for a non local vseg.
//
// We must handle vsegs in the following order
//   1) all global vsegs containing a page table,
//   2) all global vsegs occupying more than one BPP, 
//   3) all others global vsegs
//   4) all private vsegs in user space.
///////////////////////////////////////////////////////////////////////////////
void boot_ptabs_init() 
{
    mapping_header_t*   header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_vspace_t*   vspace = _get_vspace_base(header);
    mapping_vseg_t*     vseg   = _get_vseg_base(header);
    mapping_vobj_t*     vobj   = _get_vobj_base(header);

    unsigned int vspace_id;
    unsigned int vseg_id;

    if (header->vspaces == 0 )
    {
        _puts("\n[BOOT ERROR] in boot_ptabs_init() : mapping ");
        _puts( header->name );
        _puts(" contains no vspace\n");
        _exit();
    }

    ///////// Phase 1 : global vsegs containing a PTAB (two loops required)

#if BOOT_DEBUG_PT
_puts("\n[BOOT DEBUG] map PTAB global vsegs\n");
#endif

    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) 
    {
        unsigned int vobj_id = vseg[vseg_id].vobj_offset;
        if ( (vobj[vobj_id].type == VOBJ_TYPE_PTAB) )
        {
            boot_vseg_map( &vseg[vseg_id], 0xFFFFFFFF );
            vseg[vseg_id].mapped = 1;
        }
    }

    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) 
    {
        unsigned int vobj_id = vseg[vseg_id].vobj_offset;
        if ( (vobj[vobj_id].type == VOBJ_TYPE_PTAB) )
        {
            boot_vseg_pte( &vseg[vseg_id], 0xFFFFFFFF );
            vseg[vseg_id].mapped = 1;
        }
    }

    ///////// Phase 2 : global vsegs occupying more than one BPP (one loop)

#if BOOT_DEBUG_PT
_puts("\n[BOOT DEBUG] map all multi-BPP global vsegs\n");
#endif

    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) 
    {
        unsigned int vobj_id = vseg[vseg_id].vobj_offset;
        if ( (vobj[vobj_id].length > 0x200000) &&
             (vseg[vseg_id].mapped == 0) )
        {
            boot_vseg_map( &vseg[vseg_id], 0xFFFFFFFF );
            vseg[vseg_id].mapped = 1;
            boot_vseg_pte( &vseg[vseg_id], 0xFFFFFFFF );
        }
    }

    ///////// Phase 3 : all others global vsegs (one loop)

#if BOOT_DEBUG_PT
_puts("\n[BOOT DEBUG] map all others global vsegs\n");
#endif

    for (vseg_id = 0; vseg_id < header->globals; vseg_id++) 
    {
        if ( vseg[vseg_id].mapped == 0 )
        {
            boot_vseg_map( &vseg[vseg_id], 0xFFFFFFFF );
            vseg[vseg_id].mapped = 1;
            boot_vseg_pte( &vseg[vseg_id], 0xFFFFFFFF );
        }
    }

    ///////// Phase 4 : all private vsegs (two nested loops)

    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
    {

#if BOOT_DEBUG_PT
_puts("\n[BOOT DEBUG] map private vsegs for vspace ");
_puts( vspace[vspace_id].name );
_puts("\n");
#endif

        for (vseg_id = vspace[vspace_id].vseg_offset;
             vseg_id < (vspace[vspace_id].vseg_offset + vspace[vspace_id].vsegs);
             vseg_id++) 
        {
            boot_vseg_map( &vseg[vseg_id], vspace_id );
            vseg[vseg_id].mapped = 1;
            boot_vseg_pte( &vseg[vseg_id], vspace_id );
        }
    }

#if (BOOT_DEBUG_PT > 1) 
mapping_vseg_t*    curr;
mapping_pseg_t*    pseg    = _get_pseg_base(header);
mapping_cluster_t* cluster = _get_cluster_base(header);
unsigned int       pseg_id;
for( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
{
    unsigned int cluster_id = pseg[pseg_id].clusterid;
    _puts("\n[BOOT DEBUG] vsegs mapped on pseg ");
    _puts( pseg[pseg_id].name );
    _puts(" in cluster[");
    _putd( cluster[cluster_id].x );
    _puts(",");
    _putd( cluster[cluster_id].y );
    _puts("]\n");
    for( curr = (mapping_vseg_t*)pseg[pseg_id].next_vseg ;
         curr != 0 ;
         curr = (mapping_vseg_t*)curr->next_vseg )
    {
        _puts(" - vseg ");
        _puts( curr->name );
        _puts(" : len = ");
        _putx( curr->length );
        _puts(" / vbase ");
        _putx( curr->vbase );
        _puts(" / pbase ");
        _putl( curr->pbase );
        _puts("\n");
    }  
}
#endif

} // end boot_ptabs_init()

///////////////////////////////////////////////////////////////////////////////
// This function initializes all private vobjs defined in the vspaces,
// such as mwmr channels, barriers and locks, because these vobjs 
// are not known, and not initialized by the compiler.
// The MMU is supposed to be activated...
///////////////////////////////////////////////////////////////////////////////
void boot_vobjs_init() 
{
    mapping_header_t* header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_vspace_t* vspace = _get_vspace_base(header);
    mapping_vobj_t* vobj     = _get_vobj_base(header);

    unsigned int vspace_id;
    unsigned int vobj_id;

    // loop on the vspaces
    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
    {

#if BOOT_DEBUG_VOBJS
_puts("\n[BOOT DEBUG] ****** vobjs initialisation in vspace ");
_puts(vspace[vspace_id].name);
_puts(" ******\n");
#endif

        _set_mmu_ptpr( (unsigned int)(_ptabs_paddr[vspace_id][0][0] >> 13) );

        // loop on the vobjs
        for (vobj_id = vspace[vspace_id].vobj_offset;
             vobj_id < (vspace[vspace_id].vobj_offset + vspace[vspace_id].vobjs);
             vobj_id++) 
        {
            switch (vobj[vobj_id].type) 
            {
                case VOBJ_TYPE_MWMR:    // storage capacity is (vobj.length/4 - 5) words
                {
#if BOOT_DEBUG_VOBJS
_puts("MWMR    : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    mwmr_channel_t* mwmr = (mwmr_channel_t *) (vobj[vobj_id].vbase);
                    mwmr->ptw = 0;
                    mwmr->ptr = 0;
                    mwmr->sts = 0;
                    mwmr->width = vobj[vobj_id].init;
                    mwmr->depth = (vobj[vobj_id].length >> 2) - 6;
                    mwmr->lock = 0;
#if BOOT_DEBUG_VOBJS
_puts("          fifo depth = ");
_putd(mwmr->depth);
_puts(" / width = ");
_putd(mwmr->width);
_puts("\n");
#endif
                    break;
                }
                case VOBJ_TYPE_ELF:    // initialisation done by the loader 
                {
#if BOOT_DEBUG_VOBJS
_puts("ELF     : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    break;
                }
                case VOBJ_TYPE_BLOB:    // initialisation done by the loader 
                {
#if BOOT_DEBUG_VOBJS
_puts("BLOB    : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    break;
                }
                case VOBJ_TYPE_BARRIER:    // init is the number of participants
                {
#if BOOT_DEBUG_VOBJS
_puts("BARRIER : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    giet_barrier_t* barrier = (giet_barrier_t *) (vobj[vobj_id].vbase);
                    barrier->count  = vobj[vobj_id].init;
                    barrier->ntasks = vobj[vobj_id].init;
                    barrier->sense  = 0;
#if BOOT_DEBUG_VOBJS
_puts("          init_value = ");
_putd(barrier->init);
_puts("\n");
#endif
                    break;
                }
                case VOBJ_TYPE_LOCK:    // init value is "not taken"
                {
#if BOOT_DEBUG_VOBJS
_puts("LOCK    : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    unsigned int* lock = (unsigned int *) (vobj[vobj_id].vbase);
                    *lock = 0;
                    break;
                }
                case VOBJ_TYPE_BUFFER:    // nothing to initialise
                {
#if BOOT_DEBUG_VOBJS
_puts("BUFFER  : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    break;
                }
                case VOBJ_TYPE_MEMSPACE:
                {
#if BOOT_DEBUG_VOBJS
_puts("MEMSPACE  : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts("\n");
#endif
                    giet_memspace_t* memspace = (giet_memspace_t *) vobj[vobj_id].vbase;
                    memspace->buffer = (void *) vobj[vobj_id].vbase + 8;
                    memspace->size = vobj[vobj_id].length - 8;
#if BOOT_DEBUG_VOBJS
_puts("          buffer vbase = ");
_putx((unsigned int)memspace->buffer);
_puts(" / size = ");
_putx(memspace->size);
_puts("\n");
#endif
                    break;
                }
                case VOBJ_TYPE_CONST:
                {
#if BOOT_DEBUG_VOBJS
_puts("CONST   : ");
_puts(vobj[vobj_id].name);
_puts(" / vaddr = ");
_putx(vobj[vobj_id].vaddr);
_puts(" / paddr = ");
_putl(vobj[vobj_id].paddr);
_puts(" / length = ");
_putx(vobj[vobj_id].length);
_puts(" / init = ");
_putx(vobj[vobj_id].init);
_puts("\n");
#endif
                    unsigned int* addr = (unsigned int *) vobj[vobj_id].vbase;
                    *addr = vobj[vobj_id].init;

#if BOOT_DEBUG_VOBJS
_puts("          init = ");
_putx(*addr);
_puts("\n");
#endif
                    break;
                }
                default:
                {
                    _puts("\n[BOOT ERROR] in boot_vobjs_init() : Illegal vobj type ");
                    _putd( vobj[vobj_id].type );
                    _puts(" in vspace ");
                    _puts( vspace[vspace_id].name );
                    _puts("\n");
                    _exit();
                }
            }            // end switch type
        }          // end loop on vobjs
    }        // end loop on vspaces
} // end boot_vobjs_init()

///////////////////////////////////////////////////////////////////////////////
// This function returns in the vbase and length buffers the virtual base 
// address and the length of the  segment allocated to the schedulers array 
// in the cluster defined by the clusterid argument.
///////////////////////////////////////////////////////////////////////////////
void boot_get_sched_vaddr( unsigned int  cluster_id,
                           unsigned int* vbase, 
                           unsigned int* length )
{
    mapping_header_t* header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_vobj_t*   vobj   = _get_vobj_base(header);
    mapping_vseg_t*   vseg   = _get_vseg_base(header);
    mapping_pseg_t*   pseg   = _get_pseg_base(header);

    unsigned int vseg_id;
    unsigned int found = 0;

    for ( vseg_id = 0 ; (vseg_id < header->vsegs) && (found == 0) ; vseg_id++ )
    {
        if ( (vobj[vseg[vseg_id].vobj_offset].type == VOBJ_TYPE_SCHED) && 
             (pseg[vseg[vseg_id].psegid].clusterid == cluster_id ) )
        {
            *vbase  = vseg[vseg_id].vbase;
            *length = vobj[vseg[vseg_id].vobj_offset].length;
            found = 1;
        }
    }
    if ( found == 0 )
    {
        mapping_cluster_t* cluster = _get_cluster_base(header);
        _puts("\n[BOOT ERROR] No vobj of type SCHED in cluster [");
        _putd( cluster[cluster_id].x );
        _puts(",");
        _putd( cluster[cluster_id].y );
        _puts("]\n");
        _exit();
    }
} // end boot_get_sched_vaddr()

////////////////////////////////////////////////////////////////////////////////////
// This function initialises all processors schedulers.
// This is done by processor 0, and the MMU must be activated.
// - In Step 1, it initialises the _schedulers[x][y][l] pointers array, and scan
//              the processors for a first initialisation of the schedulers:
//              idle_task context, and HWI / SWI / PTI vectors. 
// - In Step 2, it scan all tasks in all vspaces to complete the tasks contexts, 
//              initialisation as specified in the mapping_info data structure. 
////////////////////////////////////////////////////////////////////////////////////
void boot_schedulers_init() 
{
    mapping_header_t*  header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_cluster_t* cluster = _get_cluster_base(header);
    mapping_vspace_t*  vspace  = _get_vspace_base(header);
    mapping_task_t*    task    = _get_task_base(header);
    mapping_vobj_t*    vobj    = _get_vobj_base(header);
    mapping_periph_t*  periph  = _get_periph_base(header);
    mapping_irq_t*     irq     = _get_irq_base(header);

    unsigned int cluster_id;    // cluster index in mapping_info 
    unsigned int periph_id;     // peripheral index in mapping_info
    unsigned int irq_id;        // irq index in mapping_info
    unsigned int vspace_id;     // vspace index in mapping_info
    unsigned int task_id;       // task index in mapping_info
    unsigned int vobj_id;       // vobj index in mapping_info

    unsigned int lpid;          // local processor index (for several loops)

    // WTI allocators to processors (for HWIs translated to WTIs)  
    // In all clusters the first NB_PROCS_MAX WTIs are reserved for WAKUP
    unsigned int alloc_wti_channel[X_SIZE*Y_SIZE];   // one per cluster

    // pointers on the XCU and PIC peripherals
    mapping_periph_t*  xcu = NULL;
    mapping_periph_t*  pic = NULL;

    unsigned int          sched_vbase;  // schedulers array vbase address in a cluster
    unsigned int          sched_length; // schedulers array length
    static_scheduler_t*   psched;       // pointer on processor scheduler

    /////////////////////////////////////////////////////////////////////////
    // Step 1 : loop on the clusters and on the processors 
    //          to initialize the schedulers[] array of pointers,
    //          idle task context and interrupt vectors.
    // Implementation note:
    // We need to use both (proc_id) to scan the mapping info structure,
    // and (x,y,lpid) to access the schedulers array.

    for (cluster_id = 0 ; cluster_id < X_SIZE*Y_SIZE ; cluster_id++) 
    {
        unsigned int x          = cluster[cluster_id].x;
        unsigned int y          = cluster[cluster_id].y;

#if BOOT_DEBUG_SCHED
_puts("\n[BOOT DEBUG] Initialise schedulers in cluster[");
_putd( x );
_puts(",");
_putd( y );
_puts("]\n");
#endif
        alloc_wti_channel[cluster_id] = NB_PROCS_MAX;

        // checking processors number
        if ( cluster[cluster_id].procs > NB_PROCS_MAX )
        {
            _puts("\n[BOOT ERROR] Too much processors in cluster[");
            _putd( x );
            _puts(",");
            _putd( y );
            _puts("]\n");
            _exit();
        }
 
        // no schedulers initialisation if nprocs == 0
        if ( cluster[cluster_id].procs > 0 )
        {
            // get scheduler array virtual base address in cluster[cluster_id]
            boot_get_sched_vaddr( cluster_id, &sched_vbase, &sched_length );

            if ( sched_length < (cluster[cluster_id].procs<<13) ) // 8 Kbytes per scheduler
            {
                _puts("\n[BOOT ERROR] Schedulers segment too small in cluster[");
                _putd( x );
                _puts(",");
                _putd( y );
                _puts("]\n");
                _exit();
            }

            // scan peripherals to find the XCU and the PIC component

            xcu = NULL;  
            for ( periph_id = cluster[cluster_id].periph_offset ;
                  periph_id < cluster[cluster_id].periph_offset + cluster[cluster_id].periphs;
                  periph_id++ )
            {
                if( periph[periph_id].type == PERIPH_TYPE_XCU ) 
                {
                    xcu = &periph[periph_id];

                    if ( xcu->arg < cluster[cluster_id].procs )
                    {
                        _puts("\n[BOOT ERROR] Not enough inputs for XCU[");
                        _putd( x );
                        _puts(",");
                        _putd( y );
                        _puts("]\n");
                        _exit();
                    }
                }
                if( periph[periph_id].type == PERIPH_TYPE_PIC )   
                {
                    pic = &periph[periph_id];
                }
            } 
            if ( xcu == NULL )
            {         
                _puts("\n[BOOT ERROR] No XCU component in cluster[");
                _putd( x );
                _puts(",");
                _putd( y );
                _puts("]\n");
                _exit();
            }

            // loop on processors for schedulers default values
            // initialisation, including WTI and PTI vectors
            for ( lpid = 0 ; lpid < cluster[cluster_id].procs ; lpid++ )
            {
                // pointer on processor scheduler
                psched = (static_scheduler_t*)(sched_vbase + (lpid<<13));

                // initialise the schedulers pointers array
                _schedulers[x][y][lpid] = psched;

#if BOOT_DEBUG_SCHED
unsigned int   sched_vbase = (unsigned int)_schedulers[x][y][lpid];
unsigned int   sched_ppn;
unsigned int   sched_flags;
paddr_t        sched_pbase;

page_table_t* ptab = (page_table_t*)(_ptabs_vaddr[0][x][y]);
_v2p_translate( ptab, sched_vbase>>12, &sched_ppn, &sched_flags );
sched_pbase = ((paddr_t)sched_ppn)<<12;

_puts("\nProc[");
_putd( x );
_puts(",");
_putd( y );
_puts(",");
_putd( lpid );
_puts("] : scheduler vbase = ");
_putx( sched_vbase );
_puts(" : scheduler pbase = ");
_putl( sched_pbase );
_puts("\n");
#endif
                // initialise the "tasks" and "current" variables default values
                psched->tasks   = 0;
                psched->current = IDLE_TASK_INDEX;

                // default values for HWI / PTI / SWI vectors (valid bit = 0)
                unsigned int slot;
                for (slot = 0; slot < 32; slot++)
                {
                    psched->hwi_vector[slot] = 0;
                    psched->pti_vector[slot] = 0;
                    psched->wti_vector[slot] = 0;
                }

                // WTI[lpid] <= ISR_WAKUP / PTI[lpid] <= ISR_TICK 
                psched->wti_vector[lpid] = ISR_WAKUP | 0x80000000;
                psched->pti_vector[lpid] = ISR_TICK  | 0x80000000;

                // initializes the idle_task context in scheduler:
                // - the SR slot is 0xFF03 because this task run in kernel mode.
                // - it uses the page table of vspace[0]
                // - it uses the kernel TTY terminal
                // - slots containing addresses (SP, RA, EPC)
                //   must be initialised by kernel_init()

                psched->context[IDLE_TASK_INDEX][CTX_CR_ID]   = 0;
                psched->context[IDLE_TASK_INDEX][CTX_SR_ID]   = 0xFF03;
                psched->context[IDLE_TASK_INDEX][CTX_PTPR_ID] = _ptabs_paddr[0][x][y]>>13;
                psched->context[IDLE_TASK_INDEX][CTX_PTAB_ID] = _ptabs_vaddr[0][x][y];
                psched->context[IDLE_TASK_INDEX][CTX_TTY_ID]  = 0;
                psched->context[IDLE_TASK_INDEX][CTX_LTID_ID] = IDLE_TASK_INDEX;
                psched->context[IDLE_TASK_INDEX][CTX_VSID_ID] = 0;
                psched->context[IDLE_TASK_INDEX][CTX_RUN_ID]  = 1;

            }  // end for processors

            // scan HWIs connected to local XCU 
            // for round-robin allocation to processors
            lpid = 0;
            for ( irq_id = xcu->irq_offset ;
                  irq_id < xcu->irq_offset + xcu->irqs ;
                  irq_id++ )
            {
                unsigned int type    = irq[irq_id].srctype;
                unsigned int srcid   = irq[irq_id].srcid;
                unsigned int isr     = irq[irq_id].isr & 0xFFFF;
                unsigned int channel = irq[irq_id].channel << 16;

                if ( (type != IRQ_TYPE_HWI) || (srcid > 31) )
                {
                    _puts("\n[BOOT ERROR] Bad IRQ in XCU of cluster[");
                    _putd( x );
                    _puts(",");
                    _putd( y );
                    _puts("]\n");
                    _exit();
                }

                _schedulers[x][y][lpid]->hwi_vector[srcid] = isr | channel | 0x80000000;
                lpid = (lpid + 1) % cluster[cluster_id].procs; 

            } // end for irqs
        } // end if nprocs > 0
    } // end for clusters

    // If there is an external PIC component, we scan HWIs connected to PIC
    // for Round Robin allocation (as WTI) to processors.
    // We allocate one WTI per processor, starting from proc[0,0,0], 
    // and we increment (cluster_id, lpid) as required.
    if ( pic != NULL )
    {   
        unsigned int cluster_id = 0;   // index in clusters array
        unsigned int lpid       = 0;   // processor local index

        // scan IRQS defined in PIC
        for ( irq_id = pic->irq_offset ;
              irq_id < pic->irq_offset + pic->irqs ;
              irq_id++ )
        {
            // compute next values for (cluster_id,lpid)
            // if no more procesor available in current cluster
            unsigned int overflow = 0;
            while ( (lpid >= cluster[cluster_id].procs) ||
                    (alloc_wti_channel[cluster_id] >= xcu->arg) )
            {
                overflow++;
                cluster_id = (cluster_id + 1) % (X_SIZE*Y_SIZE);
                lpid       = 0;

                // overflow detection
                if ( overflow > (X_SIZE*Y_SIZE*NB_PROCS_MAX*32) )
                {
                    _puts("\n[BOOT ERROR] Not enough processors for external IRQs\n");
                    _exit();
                }
            }

            unsigned int type    = irq[irq_id].srctype;
            unsigned int srcid   = irq[irq_id].srcid;
            unsigned int isr     = irq[irq_id].isr & 0xFFFF;
            unsigned int channel = irq[irq_id].channel << 16;

            if ( (type != IRQ_TYPE_HWI) || (srcid > 31) )
            {
                _puts("\n[BOOT ERROR] Bad IRQ in PIC component\n");
                _exit();
            }

            // get scheduler[cluster_id] address
            unsigned int x          = cluster[cluster_id].x;
            unsigned int y          = cluster[cluster_id].y;
            unsigned int cluster_xy = (x<<Y_WIDTH) + y;
            psched                  = _schedulers[x][y][lpid];

            // update WTI vector for scheduler[cluster_id][lpid]
            unsigned int index            = alloc_wti_channel[cluster_id];
            psched->wti_vector[index]     = isr | channel | 0x80000000;
            alloc_wti_channel[cluster_id] = index + 1;
            lpid                          = lpid + 1;

            // update IRQ fields in mapping for PIC initialisation
            irq[irq_id].dest_id = index;
            irq[irq_id].dest_xy = cluster_xy;

        }  // end for IRQs
    } // end if PIC
                
#if BOOT_DEBUG_SCHED
for ( cluster_id = 0 ; cluster_id < (X_SIZE*Y_SIZE) ; cluster_id++ )
{
    unsigned int x          = cluster[cluster_id].x;
    unsigned int y          = cluster[cluster_id].y;
    unsigned int slot;
    unsigned int entry;
    for ( lpid = 0 ; lpid < cluster[cluster_id].procs ; lpid++ )
    {
        psched = _schedulers[x][y][lpid];
        
        _puts("\n*** IRQS for proc[");
        _putd( x );
        _puts(",");
        _putd( y );
        _puts(",");
        _putd( lpid );
        _puts("]\n");
        for ( slot = 0 ; slot < 32 ; slot++ )
        {
            entry = psched->hwi_vector[slot];
            if ( entry & 0x80000000 ) 
            {
                _puts(" - HWI ");
                _putd( slot );
                _puts(" / isrtype = ");
                _putd( entry & 0xFFFF ); 
                _puts(" / channel = ");
                _putd( (entry >> 16) & 0x7FFF ); 
                _puts("\n");
            }
        }
        for ( slot = 0 ; slot < 32 ; slot++ )
        {
            entry = psched->wti_vector[slot];
            if ( entry & 0x80000000 ) 
            {
                _puts(" - WTI ");
                _putd( slot );
                _puts(" / isrtype = ");
                _putd( entry & 0xFFFF ); 
                _puts(" / channel = ");
                _putd( (entry >> 16) & 0x7FFF ); 
                _puts("\n");
            }
        }
        for ( slot = 0 ; slot < 32 ; slot++ )
        {
            entry = psched->pti_vector[slot];
            if ( entry & 0x80000000 ) 
            {
                _puts(" - PTI ");
                _putd( slot );
                _puts(" / isrtype = ");
                _putd( entry & 0xFFFF ); 
                _puts(" / channel = ");
                _putd( (entry >> 16) & 0x7FFF ); 
                _puts("\n");
            }
        }
    }
}
#endif

    ///////////////////////////////////////////////////////////////////
    // Step 2 : loop on the vspaces and the tasks  to complete
    //          the schedulers and task contexts initialisation.

    for (vspace_id = 0; vspace_id < header->vspaces; vspace_id++) 
    {
        // We must set the PTPR depending on the vspace, because the start_vector 
        // and the stack address are defined in virtual space.
        _set_mmu_ptpr( (unsigned int)(_ptabs_paddr[vspace_id][0][0] >> 13) );

        // loop on the tasks in vspace (task_id is the global index in mapping)
        for (task_id = vspace[vspace_id].task_offset;
             task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks);
             task_id++) 
        {
            // compute the cluster coordinates & local processor index
            unsigned int x          = cluster[task[task_id].clusterid].x;
            unsigned int y          = cluster[task[task_id].clusterid].y;
            unsigned int cluster_xy = (x<<Y_WIDTH) + y;
            unsigned int lpid       = task[task_id].proclocid;                 

#if BOOT_DEBUG_SCHED
_puts("\n[BOOT DEBUG] Initialise context for task ");
_puts( task[task_id].name );
_puts(" in vspace ");
_puts( vspace[vspace_id].name );
_puts("\n");
#endif
            // compute gpid (global processor index) and scheduler base address
            unsigned int gpid = (cluster_xy << P_WIDTH) + lpid;
            psched            = _schedulers[x][y][lpid];

            // ctx_sr : value required before an eret instruction
            unsigned int ctx_sr = 0x0000FF13;

            // ctx_ptpr : page table physical base address (shifted by 13 bit)
            unsigned int ctx_ptpr = (unsigned int)(_ptabs_paddr[vspace_id][x][y] >> 13);

            // ctx_ptab : page_table virtual base address
            unsigned int ctx_ptab = _ptabs_vaddr[vspace_id][x][y];

            // ctx_epc : Get the virtual address of the memory location containing
            // the task entry point : the start_vector is stored by GCC in the seg_data 
            // segment and we must wait the .elf loading to get the entry point value...
            vobj_id = vspace[vspace_id].start_vobj_id;     
            unsigned int ctx_epc = vobj[vobj_id].vbase + (task[task_id].startid)*4;

            // ctx_sp :  Get the vobj containing the stack 
            vobj_id = task[task_id].stack_vobj_id;
            unsigned int ctx_sp = vobj[vobj_id].vbase + vobj[vobj_id].length;

            // get local task index in scheduler
            unsigned int ltid = psched->tasks;

            // get vspace thread index
            unsigned int thread_id = task[task_id].trdid;

            if (ltid >= IDLE_TASK_INDEX) 
            {
                _puts("\n[BOOT ERROR] in boot_schedulers_init() : ");
                _putd( ltid );
                _puts(" tasks allocated to processor ");
                _putd( gpid );
                _puts(" / max is ");
                _putd( IDLE_TASK_INDEX );
                _puts("\n");
                _exit();
            }

            // update the "tasks" and "current" fields in scheduler:
            // the first task to execute is task 0 as soon as there is at least
            // one task allocated to processor. 
            psched->tasks   = ltid + 1;
            psched->current = 0;

            // initializes the task context 
            psched->context[ltid][CTX_CR_ID]    = 0;
            psched->context[ltid][CTX_SR_ID]    = ctx_sr;
            psched->context[ltid][CTX_SP_ID]    = ctx_sp;
            psched->context[ltid][CTX_EPC_ID]   = ctx_epc;
            psched->context[ltid][CTX_PTPR_ID]  = ctx_ptpr;
            psched->context[ltid][CTX_PTAB_ID]  = ctx_ptab;
            psched->context[ltid][CTX_LTID_ID]  = ltid;
            psched->context[ltid][CTX_GTID_ID]  = task_id;
            psched->context[ltid][CTX_TRDID_ID] = thread_id;
            psched->context[ltid][CTX_VSID_ID]  = vspace_id;
            psched->context[ltid][CTX_RUN_ID]   = 1;

            psched->context[ltid][CTX_TTY_ID]   = 0xFFFFFFFF;
            psched->context[ltid][CTX_FBCMA_ID] = 0xFFFFFFFF;
            psched->context[ltid][CTX_RXCMA_ID] = 0xFFFFFFFF;
            psched->context[ltid][CTX_TXCMA_ID] = 0xFFFFFFFF;
            psched->context[ltid][CTX_NIC_ID]   = 0xFFFFFFFF;
            psched->context[ltid][CTX_HBA_ID]   = 0xFFFFFFFF;
            psched->context[ltid][CTX_TIM_ID]   = 0xFFFFFFFF;

#if BOOT_DEBUG_SCHED
_puts("\nTask ");
_putd( task_id );
_puts(" allocated to processor[");
_putd( x );
_puts(",");
_putd( y );
_puts(",");
_putd( lpid );
_puts("]\n  - ctx[LTID]   = ");
_putd( psched->context[ltid][CTX_LTID_ID] );
_puts("\n  - ctx[SR]     = ");
_putx( psched->context[ltid][CTX_SR_ID] );
_puts("\n  - ctx[SP]     = ");
_putx( psched->context[ltid][CTX_SP_ID] );
_puts("\n  - ctx[EPC]    = ");
_putx( psched->context[ltid][CTX_EPC_ID] );
_puts("\n  - ctx[PTPR]   = ");
_putx( psched->context[ltid][CTX_PTPR_ID] );
_puts("\n  - ctx[PTAB]   = ");
_putx( psched->context[ltid][CTX_PTAB_ID] );
_puts("\n  - ctx[GTID]   = ");
_putx( psched->context[ltid][CTX_GTID_ID] );
_puts("\n  - ctx[VSID]   = ");
_putx( psched->context[ltid][CTX_VSID_ID] );
_puts("\n  - ctx[TRDID]  = ");
_putx( psched->context[ltid][CTX_TRDID_ID] );
_puts("\n");
#endif

        } // end loop on tasks
    } // end loop on vspaces
} // end boot_schedulers_init()

//////////////////////////////////////////////////////////////////////////////////
// This function loads the map.bin file from block device.
//////////////////////////////////////////////////////////////////////////////////
void boot_mapping_init()
{
    // desactivates IOC interrupt
    _ioc_init( 0 );

    // open file "map.bin"
    int fd_id = _fat_open( IOC_BOOT_MODE,
                           "map.bin",
                           0 );         // no creation
    if ( fd_id == -1 )
    {
        _puts("\n[BOOT ERROR] : map.bin file not found \n");
        _exit();
    }

#if BOOT_DEBUG_MAPPING
_puts("\n[BOOT] map.bin file successfully open at cycle ");
_putd(_get_proctime());
_puts("\n");
#endif

    // get "map.bin" file size (from fat) and check it
    unsigned int size    = fat.fd[fd_id].file_size;

    if ( size > SEG_BOOT_MAPPING_SIZE )
    {
        _puts("\n[BOOT ERROR] : allocated segment too small for map.bin file\n");
        _exit();
    }

    // load "map.bin" file into buffer
    unsigned int nblocks = size >> 9;
    unsigned int offset  = size & 0x1FF;
    if ( offset ) nblocks++;

    unsigned int ok = _fat_read( IOC_BOOT_MODE,
                                 fd_id, 
                                 (unsigned int*)SEG_BOOT_MAPPING_BASE, 
                                 nblocks,       
                                 0 );      // offset
    if ( ok == -1 )
    {
        _puts("\n[BOOT ERROR] : unable to load map.bin file \n");
        _exit();
    }
    _fat_close( fd_id );
    
    // close file "map.bin"
    boot_mapping_check();

} // end boot_mapping_init()


/////////////////////////////////////////////////////////////////////////////////////
// This function load all loadable segments for one .elf file, identified 
// by the "pathname" argument. Some loadable segments can be copied in several
// clusters: same virtual address but different physical addresses.  
// - It open the file.
// - It loads the complete file in the dedicated boot_elf_buffer.
// - It copies each loadable segments  at the virtual address defined in 
//   the .elf file, making several copies if the target vseg is not local.
// - It closes the file.
// This function is supposed to be executed by processor[0,0,0].
// Note: 
//   We must use physical addresses to reach the destination buffers that
//   can be located in remote clusters. We use either a _physical_memcpy(), 
//   or a _dma_physical_copy() if DMA is available.
//////////////////////////////////////////////////////////////////////////////////////
void load_one_elf_file( unsigned int is_kernel,     // kernel file if non zero
                        char*        pathname,
                        unsigned int vspace_id )    // to scan the proper vspace
{
    mapping_header_t  * header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_vspace_t  * vspace  = _get_vspace_base(header);
    mapping_vseg_t    * vseg    = _get_vseg_base(header);
    mapping_vobj_t    * vobj    = _get_vobj_base(header);

    unsigned int seg_id;

#if BOOT_DEBUG_ELF
_puts("\n[BOOT DEBUG] Start searching file ");
_puts( pathname );
_puts(" at cycle ");
_putd( _get_proctime() );
_puts("\n");
#endif

    // open .elf file
    int fd_id = _fat_open( IOC_BOOT_MODE,
                           pathname,
                           0 );      // no creation
    if ( fd_id < 0 )
    {
        _puts("\n[BOOT ERROR] load_one_elf_file() : ");
        _puts( pathname );
        _puts(" not found\n");
        _exit();
    }

    // check buffer size versus file size
    if ( fat.fd[fd_id].file_size > GIET_ELF_BUFFER_SIZE )
    {
        _puts("\n[BOOT ERROR] load_one_elf_file() : ");
        _puts( pathname );
        _puts(" exceeds the GIET_ELF_BUFFERSIZE defined in giet_config.h\n");
        _exit();
    }

    // compute number of sectors
    unsigned int nbytes   = fat.fd[fd_id].file_size;
    unsigned int nsectors = nbytes>>9;
    if( nbytes & 0x1FF) nsectors++;

    // load file in elf buffer
    if( _fat_read( IOC_BOOT_MODE, 
                   fd_id, 
                   boot_elf_buffer,
                   nsectors,
                   0 ) != nsectors )
    {
        _puts("\n[BOOT ERROR] load_one_elf_file() : unexpected EOF for file ");
        _puts( pathname );
        _puts("\n");   
        _exit();
    }

    // Check ELF Magic Number in ELF header
    Elf32_Ehdr* elf_header_ptr = (Elf32_Ehdr*)boot_elf_buffer;

    if ( (elf_header_ptr->e_ident[EI_MAG0] != ELFMAG0) ||
         (elf_header_ptr->e_ident[EI_MAG1] != ELFMAG1) ||
         (elf_header_ptr->e_ident[EI_MAG2] != ELFMAG2) ||
         (elf_header_ptr->e_ident[EI_MAG3] != ELFMAG3) )
    {
        _puts("\n[BOOT ERROR] load_elf() : file ");
        _puts( pathname );
        _puts(" does not use ELF format\n");   
        _exit();
    }

    // get program header table pointer
    unsigned int pht_index = elf_header_ptr->e_phoff;
    if( pht_index == 0 )
    {
        _puts("\n[BOOT ERROR] load_one_elf_file() : file ");
        _puts( pathname );
        _puts(" does not contain loadable segment\n");   
        _exit();
    }
    Elf32_Phdr* elf_pht_ptr = (Elf32_Phdr*)(boot_elf_buffer + pht_index);

    // get number of segments
    unsigned int nsegments   = elf_header_ptr->e_phnum;

    _puts("\n[BOOT] File ");
    _puts( pathname );
    _puts(" loaded at cycle ");
    _putd( _get_proctime() );
    _puts("\n");

    // Loop on loadable segments in the .elf file
    for (seg_id = 0 ; seg_id < nsegments ; seg_id++)
    {
        if(elf_pht_ptr[seg_id].p_type == PT_LOAD)
        {
            // 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_filesz = elf_pht_ptr[seg_id].p_filesz;
            unsigned int seg_memsz  = elf_pht_ptr[seg_id].p_memsz;

#if BOOT_DEBUG_ELF
_puts(" - segment ");
_putd( seg_id );
_puts(" / vaddr = ");
_putx( seg_vaddr );
_puts(" / file_size = ");
_putx( seg_filesz );
_puts("\n");
#endif

            if( seg_memsz < seg_filesz )
            {
                _puts("\n[BOOT ERROR] load_one_elf_file() : segment at vaddr = ");
                _putx( seg_vaddr );
                _puts(" in file ");
                _puts( pathname );
                _puts(" has memsz < filesz \n");   
                _exit();
            }

            // fill empty space with 0 as required
            if( seg_memsz > seg_filesz )
            {
                unsigned int i; 
                for( i = seg_filesz ; i < seg_memsz ; i++ ) boot_elf_buffer[i+seg_offset] = 0;
            } 

            unsigned int src_vaddr = (unsigned int)boot_elf_buffer + seg_offset;

            // search all vsegs matching the virtual address
            unsigned int vseg_first;
            unsigned int vseg_last;
            unsigned int vseg_id;
            unsigned int found = 0;
            if ( is_kernel )
            {
                vseg_first = 0;
                vseg_last  = header->globals;
            }
            else
            {
                vseg_first = vspace[vspace_id].vseg_offset;
                vseg_last  = vseg_first + vspace[vspace_id].vsegs;
            }

            for ( vseg_id = vseg_first ; vseg_id < vseg_last ; vseg_id++ )
            {
                if ( seg_vaddr == vseg[vseg_id].vbase )  // matching 
                {
                    found = 1;

                    // get destination buffer physical address and size
                    paddr_t      seg_paddr  = vseg[vseg_id].pbase;
                    unsigned int vobj_id    = vseg[vseg_id].vobj_offset;
                    unsigned int seg_size   = vobj[vobj_id].length;
                    
#if BOOT_DEBUG_ELF
_puts("   loaded into vseg ");
_puts( vseg[vseg_id].name );
_puts(" at paddr = ");
_putl( seg_paddr );
_puts(" (buffer size = ");
_putx( seg_size );
_puts(")\n");
#endif
                    // check vseg size
                    if ( seg_size < seg_filesz )
                    {
                        _puts("\n[BOOT ERROR] in load_one_elf_file()\n");
                        _puts("vseg ");
                        _puts( vseg[vseg_id].name );
                        _puts(" is to small for loadable segment ");
                        _putx( seg_vaddr );
                        _puts(" in file ");
                        _puts( pathname );
                        _puts(" \n");   
                        _exit();
                    }

                    // copy the segment from boot buffer to destination buffer
                    // using DMA channel[0,0,0] if it is available.
                    if( NB_DMA_CHANNELS > 0 )
                    {
                        _dma_physical_copy( 0,                  // DMA in cluster[0,0]
                                            0,                  // DMA channel 0
                                            (paddr_t)seg_paddr, // destination paddr
                                            (paddr_t)src_vaddr, // source paddr
                                            seg_filesz );       // size
                    }
                    else
                    {
                        _physical_memcpy( (paddr_t)seg_paddr,   // destination paddr
                                          (paddr_t)src_vaddr,   // source paddr
                                          seg_filesz );         // size
                    }
                }
            }  // end for vsegs in vspace

            // check at least one matching vseg
            if ( found == 0 )
            {
                _puts("\n[BOOT ERROR] in load_one_elf_file()\n");
                _puts("vseg for loadable segment ");
                _putx( seg_vaddr );
                _puts(" in file ");
                _puts( pathname );
                _puts(" not found: \n");   
                _puts(" check consistency between the .py and .ld files...\n");
                _exit();
            }
        }
    }  // end for loadable segments

    // close .elf file
    _fat_close( fd_id );

} // end load_one_elf_file()


/////i////////////////////////////////////////////////////////////////////////////////
// This function uses the map.bin data structure to load the "kernel.elf" file
// as well as the various "application.elf" files into memory.
// - The "preloader.elf" file is not loaded, because it has been burned in the ROM.
// - The "boot.elf" file is not loaded, because it has been loaded by the preloader.
// This function scans all vobjs defined in the map.bin data structure to collect
// all .elf files pathnames, and calls the load_one_elf_file() for each .elf file.
// As the code can be replicated in several vsegs, the same code can be copied 
// in one or several clusters by the load_one_elf_file() function.
//////////////////////////////////////////////////////////////////////////////////////
void boot_elf_load()
{
    mapping_header_t* header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_vspace_t* vspace = _get_vspace_base( header );
    mapping_vobj_t*   vobj   = _get_vobj_base( header );
    unsigned int      vspace_id;
    unsigned int      vobj_id;
    unsigned int      found;

    // Scan all vobjs corresponding to global vsegs,
    // to find the pathname to the kernel.elf file
    found = 0;
    for( vobj_id = 0 ; vobj_id < header->globals ; vobj_id++ )
    {
        if(vobj[vobj_id].type == VOBJ_TYPE_ELF) 
        {   
            found = 1;
            break;
        }
    }

    // We need one kernel.elf file
    if (found == 0)
    {
        _puts("[BOOT ERROR] boot_elf_load() : kernel.elf file not found\n");
        _exit();
    }

    // Load the kernel 
    load_one_elf_file( 1,                           // kernel file
                       vobj[vobj_id].binpath,       // file pathname
                       0 );                         // vspace 0

    // loop on the vspaces, scanning all vobjs in the vspace,
    // to find the pathname of the .elf file associated to the vspace.
    for( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {
        // loop on the vobjs in vspace (vobj_id is the global index)
        unsigned int found = 0;
        for (vobj_id = vspace[vspace_id].vobj_offset;
             vobj_id < (vspace[vspace_id].vobj_offset + vspace[vspace_id].vobjs);
             vobj_id++) 
        {
            if(vobj[vobj_id].type == VOBJ_TYPE_ELF) 
            {   
                found = 1;
                break;
            }
        }

        // We want one .elf file per vspace
        if (found == 0)
        {
            _puts("[BOOT ERROR] boot_elf_load() : .elf file not found for vspace ");
            _puts( vspace[vspace_id].name );
            _puts("\n");
            _exit();
        }

        load_one_elf_file( 0,                          // not a kernel file
                           vobj[vobj_id].binpath,      // file pathname
                           vspace_id );                // vspace index

    }  // end for vspaces

} // end boot_elf_load()

////////////////////////////////////////////////////////////////////////////////
// This function intializes the periherals and coprocessors, as specified
// in the mapping_info file.
////////////////////////////////////////////////////////////////////////////////
void boot_peripherals_init() 
{
    mapping_header_t * header   = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_cluster_t * cluster = _get_cluster_base(header);
    mapping_periph_t * periph   = _get_periph_base(header);
    mapping_vobj_t * vobj       = _get_vobj_base(header);
    mapping_coproc_t * coproc   = _get_coproc_base(header);
    mapping_cp_port_t * cp_port = _get_cp_port_base(header);
    mapping_irq_t * irq         = _get_irq_base(header);

    unsigned int cluster_id;
    unsigned int periph_id;
    unsigned int coproc_id;
    unsigned int cp_port_id;
    unsigned int channel_id;

    // loop on all physical clusters
    for (cluster_id = 0; cluster_id < X_SIZE*Y_SIZE; cluster_id++) 
    {
        // computes cluster coordinates
        unsigned int x          = cluster[cluster_id].x;
        unsigned int y          = cluster[cluster_id].y;
        unsigned int cluster_xy = (x<<Y_WIDTH) + y;

#if BOOT_DEBUG_PERI
_puts("\n[BOOT DEBUG] Peripherals initialisation in cluster[");
_putd( x );
_puts(",");
_putd( y );
_puts("]\n");
#endif

        // loop on peripherals
        for (periph_id = cluster[cluster_id].periph_offset;
             periph_id < cluster[cluster_id].periph_offset +
             cluster[cluster_id].periphs; periph_id++) 
        {
            unsigned int type       = periph[periph_id].type;
            unsigned int subtype    = periph[periph_id].subtype;
            unsigned int channels   = periph[periph_id].channels;

            switch (type) 
            {
                case PERIPH_TYPE_IOC:    // vci_block_device component
                {
                    if ( subtype == PERIPH_SUBTYPE_BDV )
                    {
                        _bdv_lock.value = 0;
#if BOOT_DEBUG_PERI
_puts("- BDV : channels = ");
_putd(channels);
_puts("\n");
#endif
                    }
                    else if ( subtype == PERIPH_SUBTYPE_HBA )
                    {
                        // TODO
                    }
                    else if ( subtype == PERIPH_SUBTYPE_SPI )
                    {
                        // TODO
                    }
                    break;
                }
                case PERIPH_TYPE_CMA:    // vci_chbuf_dma component
                {
                    for (channel_id = 0; channel_id < channels; channel_id++) 
                    {
                        // TODO
                    }
#if BOOT_DEBUG_PERI
_puts("- CMA : channels = ");
_putd(channels);
_puts("\n");
#endif
                    break;
                }
                case PERIPH_TYPE_NIC:    // vci_multi_nic component
                {
                    for (channel_id = 0; channel_id < channels; channel_id++) 
                    {
                        // TODO
                    }
#if BOOT_DEBUG_PERI
_puts("- NIC : channels = ");
_putd(channels);
_puts("\n");
#endif
                    break;
                }
                case PERIPH_TYPE_TTY:    // vci_multi_tty component
                {
                    for (channel_id = 0; channel_id < channels; channel_id++) 
                    {
                        _tty_lock[channel_id].value = 0;
                        _tty_rx_full[channel_id]    = 0;
                    }
#if BOOT_DEBUG_PERI
_puts("- TTY : channels = ");
_putd(channels);
_puts("\n");
#endif
                    break;
                }
                case PERIPH_TYPE_IOB:    // vci_io_bridge component
                {
                    if (GIET_USE_IOMMU) 
                    {
                        // TODO
                        // get the iommu page table physical address
                        // set IOMMU page table address
                        // pseg_base[IOB_IOMMU_PTPR] = ptab_pbase;    
                        // activate IOMMU
                        // pseg_base[IOB_IOMMU_ACTIVE] = 1;        
                    }
                    break;
                }
                case PERIPH_TYPE_PIC:    // vci_iopic component
                {
#if BOOT_DEBUG_PERI
_puts("- PIC : channels = ");
_putd(channels);
_puts("\n");
#endif
                    // scan all IRQs defined in mapping for PIC component,
                    // and initialises addresses for WTI IRQs
                    for ( channel_id = periph[periph_id].irq_offset ;
                          channel_id < periph[periph_id].irq_offset + periph[periph_id].irqs ;
                          channel_id++ )
                    {
                        unsigned int hwi_id     = irq[channel_id].srcid;   // HWI index in PIC
                        unsigned int wti_id     = irq[channel_id].dest_id; // WTI index in XCU
                        unsigned int cluster_xy = irq[channel_id].dest_xy; // XCU coordinates
                        unsigned int vaddr;

                        _xcu_get_wti_address( wti_id, &vaddr );
                        _pic_init( hwi_id, vaddr, cluster_xy ); 

#if BOOT_DEBUG_PERI
unsigned int address = _pic_get_register( channel_id, IOPIC_ADDRESS );
unsigned int extend  = _pic_get_register( channel_id, IOPIC_EXTEND  );
_puts("    hwi_index = ");
_putd( hwi_id );
_puts(" / wti_index = ");
_putd( wti_id );
_puts(" / vaddr = ");
_putx( vaddr );
_puts(" in cluster[");
_putd( cluster_xy >> Y_WIDTH );
_puts(",");
_putd( cluster_xy & ((1<<Y_WIDTH)-1) );
_puts("] / checked_xcu_paddr = ");
_putl( (paddr_t)address + (((paddr_t)extend)<<32) );
_puts("\n");
#endif
                    }
                    break;
                }
            }  // end switch periph type
        }  // end for periphs

#if BOOT_DEBUG_PERI
_puts("\n[BOOT DEBUG] Coprocessors initialisation in cluster[");
_putd( x );
_puts(",");
_putd( y );
_puts("]\n");
#endif

        // loop on coprocessors
        for ( coproc_id = cluster[cluster_id].coproc_offset;
              coproc_id < cluster[cluster_id].coproc_offset +
              cluster[cluster_id].coprocs; coproc_id++ ) 
        {

#if BOOT_DEBUG_PERI
_puts("- coprocessor name : ");
_puts(coproc[coproc_id].name);
_puts(" / nb ports = ");
_putd((unsigned int) coproc[coproc_id].ports);
_puts("\n");
#endif
            // loop on the coprocessor ports
            for ( cp_port_id = coproc[coproc_id].port_offset;
                  cp_port_id < coproc[coproc_id].port_offset + coproc[coproc_id].ports;
                  cp_port_id++ ) 
            {
                // get global index of associted vobj
                unsigned int vobj_id   = cp_port[cp_port_id].mwmr_vobj_id; 

                // get MWMR channel base address 
                page_table_t* ptab  = (page_table_t*)_ptabs_vaddr[0][x][y];
                unsigned int  vbase = vobj[vobj_id].vbase;
                unsigned int  ppn;
                unsigned int  flags;
                paddr_t       pbase;

                _v2p_translate( ptab, 
                                vbase>>12 , 
                                &ppn, 
                                &flags );

                pbase = ((paddr_t)ppn)<<12;

                // initialise cp_port
                _mwr_hw_init( cluster_xy,
                              cp_port_id, 
                              cp_port[cp_port_id].direction, 
                              pbase );
#if BOOT_DEBUG_PERI
_puts("     port direction: ");
_putd( (unsigned int)cp_port[cp_port_id].direction );
_puts(" / mwmr_channel_pbase = ");
_putl( pbase );
_puts(" / name = ");
_puts(vobj[vobj_id].name);
_puts("\n"); 
#endif
            } // end for cp_ports
        } // end for coprocs
    } // end for clusters
} // end boot_peripherals_init()

/////////////////////////////////////////////////////////////////////////
// This function initialises the physical memory allocators in each
// cluster containing a RAM pseg.
/////////////////////////////////////////////////////////////////////////
void boot_pmem_init() 
{
    mapping_header_t*  header     = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_cluster_t* cluster    = _get_cluster_base(header);
    mapping_pseg_t*    pseg       = _get_pseg_base(header);

    unsigned int cluster_id;
    unsigned int pseg_id;

    // scan all clusters
    for ( cluster_id = 0 ; cluster_id < X_SIZE*Y_SIZE ; cluster_id++ ) 
    {
        // scan the psegs in cluster to find first pseg of type RAM
        unsigned int pseg_min = cluster[cluster_id].pseg_offset;
        unsigned int pseg_max = pseg_min + cluster[cluster_id].psegs;
        for ( pseg_id = pseg_min ; pseg_id < pseg_max ; pseg_id++ )
        {
            if ( pseg[pseg_id].type == PSEG_TYPE_RAM )
            {
                unsigned int x    = cluster[cluster_id].x;
                unsigned int y    = cluster[cluster_id].y;
                unsigned int base = (unsigned int)pseg[pseg_id].base;
                unsigned int size = (unsigned int)pseg[pseg_id].length;
                _pmem_alloc_init( x, y, base, size );

#if BOOT_DEBUG_PT
_puts("\n[BOOT DEBUG] pmem allocator initialised in cluster[");
_putd( x );
_puts(",");
_putd( y );
_puts("] base = ");
_putx( base );
_puts(" / size = ");
_putx( size );
_puts("\n");
#endif
               break;
            }
        }
    }
} // end boot_pmem_init()
 
/////////////////////////////////////////////////////////////////////////
// This function is the entry point of the boot code for all processors.
// Most of this code is executed by Processor 0 only.
/////////////////////////////////////////////////////////////////////////
void boot_init() 
{
    mapping_header_t*  header     = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
    mapping_cluster_t* cluster    = _get_cluster_base(header);
    unsigned int       gpid       = _get_procid();
 
    if ( gpid == 0 )    // only Processor 0 does it
    {
        _puts("\n[BOOT] boot_init start at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Load the map.bin file into memory and check it
        boot_mapping_init();

        _puts("\n[BOOT] Mapping \"");
        _puts( header->name );
        _puts("\" loaded at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Initializes the physical memory allocators
        boot_pmem_init();

        _puts("\n[BOOT] Physical memory allocators initialised at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Build page tables
        boot_ptabs_init();

        _puts("\n[BOOT] Page tables initialised at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Activate MMU for proc [0,0,0]
        _set_mmu_ptpr( (unsigned int)(_ptabs_paddr[0][0][0]>>13) );
        _set_mmu_mode( 0xF );

        _puts("\n[BOOT] Processor[0,0,0] : MMU activation at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Initialise private vobjs in vspaces
        boot_vobjs_init();

        _puts("\n[BOOT] Private vobjs initialised at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Initialise schedulers
        boot_schedulers_init();

        _puts("\n[BOOT] Schedulers initialised at cycle ");
        _putd(_get_proctime());
        _puts("\n");
        
        // Set CP0_SCHED register for proc [0,0,0]
        _set_sched( (unsigned int)_schedulers[0][0][0] );

        // Initialise non replicated peripherals
        boot_peripherals_init();

        _puts("\n[BOOT] Non replicated peripherals initialised at cycle ");
        _putd(_get_proctime());
        _puts("\n");

        // Loading all .elf files
        boot_elf_load();

        // P0 starts all other processors
        unsigned int clusterid, p;

        for ( clusterid = 0 ; clusterid < X_SIZE*Y_SIZE ; clusterid++ ) 
        {
            unsigned int nprocs     = cluster[clusterid].procs;
            unsigned int x          = cluster[clusterid].x;
            unsigned int y          = cluster[clusterid].y;
            unsigned int cluster_xy = (x<<Y_WIDTH) + y;

            for ( p = 0 ; p < nprocs; p++ ) 
            {
                if ( (nprocs > 0) && ((clusterid != 0) || (p != 0)) )
                {
                    _xcu_send_wti( cluster_xy, p, (unsigned int)boot_entry );
                }
            }
        }
  
    }  // end monoprocessor boot

    ///////////////////////////////////////////////////////////////////////////////
    //            Parallel execution starts actually here
    ///////////////////////////////////////////////////////////////////////////////

    // all processor initialise the SCHED register
    // from the _schedulers[x][y][lpid array]
    unsigned int cluster_xy = gpid >> P_WIDTH;
    unsigned int lpid       = gpid & ((1<<P_WIDTH)-1);
    unsigned int x          = cluster_xy >> Y_WIDTH;
    unsigned int y          = cluster_xy & ((1<<Y_WIDTH)-1);
    _set_sched( (unsigned int)_schedulers[x][y][lpid] );

    // all processors (but Proc[0,0,0]) activate MMU
    if ( gpid != 0 )
    {
        _set_mmu_ptpr( (unsigned int)(_ptabs_paddr[0][x][y]>>13) );
        _set_mmu_mode( 0xF );
    }

    // all processors reset BEV bit in the status register to use
    // the GIET_VM exception handler instead of the PRELOADER exception handler
    _set_sr( 0 );

    // all processors jump to kernel_init 
    // using the address defined in the giet_vsegs.ld file
    unsigned int kernel_entry = (unsigned int)&kernel_init_vbase;
    asm volatile( "jr   %0" ::"r"(kernel_entry) );

} // end boot_init()


// 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