source: soft/giet_vm/sys/boot_handler.c @ 158

//////////////////////////////////////////////////////////////////////////////////
// File     : boot_handler.c
// Date     : 01/04/2012
// Author   : alain greiner
// Copyright (c) UPMC-LIP6
///////////////////////////////////////////////////////////////////////////////////
// The boot_handler.h and boot_handler.c files are part of the GIET nano-kernel.
// This code can be used in the boot phase to launch one or several multi-tasks 
// applications on a many_cores hardware architecture. 
// It uses the SoCLib generic MMU (paged virtual memory) to provide two services:
//
// 1) classical memory protection, when several independant applications compiled
//    in different virtual spaces are executing on the same hardware platform.
// 2) data placement in NUMA architectures, when we want to control the placement 
//    of the software objects (virtual segments) on the physical memory banks.
//
// It uses the MAPPING_INFO binary data structures, that must be pre-loaded in the 
// boot ROM in the seg_boot_mapping segment (at address seg_boot_mapping_base).
// This MAPPING_INFO data structure defines both the hardware architecture,
// and the mapping:
// - number of clusters, 
// - number of processors in each cluster, 
// - physical segmentation of the physical address space, 
// - number of virtual spaces (one multi-task application per vspace), 
// - number of tasks per vspace,
// - number of mwmr channels per vspace,
// - number of virtual segments per vspace,
// - static placement of tasks on the processors, 
// - static placement of virtual segments (vseg) in the physical segments (pseg).
//
// The page table are statically constructed in the boot phase, and they do not 
// change during execution. The GIET uses only 4 Kbytes pages.
// As most applications use only a limited number of segments, the number of PT2s 
// actually used by a given virtual space is generally smaller than 2048, and is
// defined at compile time (GIET_NB_PT2_MAX configuration parameter). 
// For alignment constraints, GIET_NB_PT2_MAX must be an even number.
// The max number of virtual spaces (GIET_NB_VSPACE_MAX) is a configuration parameter.
//
// Each page table (one page table per virtual space) is monolithic:
// - a first 8K aligned PT1[2148] array, indexed by the (ix1) field of VPN. 
//   The PT1 contains 2048 PTD of 4 bytes => 8K bytes.
// - an aray of array PT2[1024][GIET_NB_PT2_MAX], indexed by
//   the (ix2) field of the VPN, and by the PT2 index (pt2_id).
//   Each PT2 contains 512 PTE2 of 8bytes => 4Kbytes * GIET_NB_PT2_MAX
// The size of each page table is 8K + (GIET_NB_PT2_MAX)*4K bytes.
// All page tables must be stored in the seg_kernel_pt segment (at address
// seg_kernel_pt_base) 
////////////////////////////////////////////////////////////////////////////////////

#include <mips32_registers.h>
#include <boot_handler.h>
#include <mapping_info.h>
#include <giet_config.h>
#include <common.h>
#include <ctx_handler.h>
#include <irq_handler.h>
#include <hwr_mapping.h>
#include <mwmr.h>

#define in_ptab __attribute__((section (".ptab")))
#define in_boot __attribute__((section (".boot")))

#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_NB_PT2_MAX)
# error The GIET_NB_PT2_MAX value must be defined in the 'giet_config.h' file !
#endif

////////////////////////////////////////////////////////////////////////////
//  Global variables
////////////////////////////////////////////////////////////////////////////

// Page Tables (each one takes PT1_SIZE + (GIET_NB_PT2_MAX)*PT2_SIZE bytes 
// It will be stored in seg_kernel_pt segment
in_ptab page_table_t      _ptab_array[GIET_NB_VSPACE_MAX];

// PT2 allocator : next free PT2 index 
// will be stored in seg_kernel_data segment
unsigned int    _next_free_pt2[GIET_NB_VSPACE_MAX] =
                         { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };


//////////////////////////////////////////////////////////////////////////////
// boot_procid() 
//////////////////////////////////////////////////////////////////////////////
in_boot unsigned int boot_procid()
{
    unsigned int ret;
    asm volatile("mfc0 %0, $15, 1" : "=r"(ret));
    return (ret & 0x3FF);
}

//////////////////////////////////////////////////////////////////////////////
// boot_time() 
//////////////////////////////////////////////////////////////////////////////
in_boot unsigned int boot_time()
{
    unsigned int ret;
    asm volatile("mfc0 %0, $9" : "=r"(ret));
    return ret;
}

//////////////////////////////////////////////////////////////////////////////
// boot_exit() 
//////////////////////////////////////////////////////////////////////////////
in_boot void boot_exit()
{
    while(1) asm volatile("nop");
}

////////////////////////////////////////////////////////////////////////////
//      boot_eret()
////////////////////////////////////////////////////////////////////////////
in_boot void boot_eret()
{
    asm volatile("eret");
}

////////////////////////////////////////////////////////////////////////////
//      boot_strncmp()
////////////////////////////////////////////////////////////////////////////
in_boot int boot_strncmp( const char* s1, 
                          const char* s2,
                          unsigned int n )
{
    unsigned int i;
    for ( i=0 ; i<n ; i++)
    {
        if ( s1[i] != s2[i] ) return 1;
        if ( s1[i] == 0 )     break;
    }
    return 0;
}

////////////////////////////////////////////////////////////////////////////
// boot_tty_puts()
// (it uses TTY0)
////////////////////////////////////////////////////////////////////////////
in_boot void boot_tty_puts(const char *buffer) 
{
    unsigned int* tty_address = (unsigned int*)&seg_tty_base;
    unsigned int n;

    for ( n=0; n<100; n++)
    {
        if (buffer[n] == 0) break;
        tty_address[0] = (unsigned int)buffer[n];
    }
} 

////////////////////////////////////////////////////////////////////////////
// boot_tty_putw() 
// (it uses TTY0)
////////////////////////////////////////////////////////////////////////////
in_boot void boot_tty_putw(unsigned int val)
{
    static const char   HexaTab[] = "0123456789ABCDEF";
    char                buf[11];
    unsigned int        c;

    buf[0]  = '0';
    buf[1]  = 'x';
    buf[10] = 0;

    for ( c = 0 ; c < 8 ; c++ )
    { 
        buf[9-c] = HexaTab[val&0xF];
        val = val >> 4;
    }
    boot_tty_puts(buf);
}

/////////////////////////////////////////////////////////////////////////////
// various mapping_info data structure access functions
/////////////////////////////////////////////////////////////////////////////
in_boot mapping_cluster_t* boot_get_cluster_base( mapping_header_t* header )
{
    return   (mapping_cluster_t*) ((char*)header +
                                  MAPPING_HEADER_SIZE);
}
/////////////////////////////////////////////////////////////////////////////
in_boot mapping_pseg_t* boot_get_pseg_base( mapping_header_t* header )
{
    return   (mapping_pseg_t*)    ((char*)header +
                                  MAPPING_HEADER_SIZE +
                                  MAPPING_CLUSTER_SIZE*header->clusters);
}
/////////////////////////////////////////////////////////////////////////////
in_boot mapping_vspace_t* boot_get_vspace_base( mapping_header_t* header )
{
    return   (mapping_vspace_t*)  ((char*)header +
                                  MAPPING_HEADER_SIZE +
                                  MAPPING_CLUSTER_SIZE*header->clusters +
                                  MAPPING_PSEG_SIZE*header->psegs);
}
/////////////////////////////////////////////////////////////////////////////
in_boot mapping_vseg_t* boot_get_vseg_base( mapping_header_t* header )
{
    return   (mapping_vseg_t*)    ((char*)header +
                                  MAPPING_HEADER_SIZE +
                                  MAPPING_CLUSTER_SIZE*header->clusters +
                                  MAPPING_PSEG_SIZE*header->psegs +
                                  MAPPING_VSPACE_SIZE*header->vspaces);
}
/////////////////////////////////////////////////////////////////////////////
in_boot mapping_task_t* boot_get_task_base( mapping_header_t* header )
{
    return   (mapping_task_t*)    ((char*)header +
                                  MAPPING_HEADER_SIZE +
                                  MAPPING_CLUSTER_SIZE*header->clusters +
                                  MAPPING_PSEG_SIZE*header->psegs +
                                  MAPPING_VSPACE_SIZE*header->vspaces +
                                  MAPPING_VSEG_SIZE*header->vsegs);
}

/////////////////////////////////////////////////////////////////////////////
// print the content of the mapping_info data structure 
////////////////////////////////////////////////////////////////////////
in_boot void boot_print_mapping_info()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base; 
    
    unsigned int                vspace_id;
    unsigned int                cluster_id;
    unsigned int                pseg_id;
    unsigned int                vseg_id;
    unsigned int                task_id;

    mapping_cluster_t*  cluster = boot_get_cluster_base( header );
    mapping_pseg_t*         pseg    = boot_get_pseg_base( header );;
    mapping_vspace_t*   vspace  = boot_get_vspace_base ( header );;
    mapping_vseg_t*         vseg    = boot_get_vseg_base ( header );
    mapping_task_t*         task    = boot_get_task_base ( header );;

    // header
    boot_tty_puts("mapping_info");

    boot_tty_puts("\n - signature = ");
    boot_tty_putw(header->signature);
    boot_tty_puts("\n - name      = ");
    boot_tty_puts(header->name);
    boot_tty_puts("\n - clusters  = ");
    boot_tty_putw(header->clusters);
    boot_tty_puts("\n - psegs     = ");
    boot_tty_putw(header->psegs);
    boot_tty_puts("\n - ttys      = ");
    boot_tty_putw(header->ttys);
    boot_tty_puts("\n - vspaces   = ");
    boot_tty_putw(header->vspaces);
    boot_tty_puts("\n - globals   = ");
    boot_tty_putw(header->globals);
    boot_tty_puts("\n - vsegs     = ");
    boot_tty_putw(header->vsegs);
    boot_tty_puts("\n - tasks     = ");
    boot_tty_putw(header->tasks);
    boot_tty_puts("\n - syspath   = ");
    boot_tty_puts(header->syspath);
    boot_tty_puts("\n\n");

    // clusters
    for ( cluster_id = 0 ; cluster_id < header->clusters ; cluster_id++ )
    {
        boot_tty_puts("cluster ");
        boot_tty_putw(cluster_id);

        boot_tty_puts("\n - procs  = ");
        boot_tty_putw(cluster[cluster_id].procs);
        boot_tty_puts("\n - timers = ");
        boot_tty_putw(cluster[cluster_id].timers);
        boot_tty_puts("\n - dmas   = ");
        boot_tty_putw(cluster[cluster_id].dmas);
        boot_tty_puts("\n\n");
    }

    // psegs
    for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
    {
        boot_tty_puts("pseg ");
        boot_tty_putw(pseg_id);

        boot_tty_puts("\n - name   = ");
        boot_tty_puts( pseg[pseg_id].name );
        boot_tty_puts("\n - base   = ");
        boot_tty_putw( pseg[pseg_id].base );
        boot_tty_puts("\n - length = ");
        boot_tty_putw( pseg[pseg_id].length );
        boot_tty_puts("\n\n");
    }

    // globals
    for ( vseg_id = 0 ; vseg_id < header->globals ; vseg_id++ )
    {
        boot_tty_puts("global vseg ");
        boot_tty_putw(vseg_id);

        boot_tty_puts("\n - name   = ");
        boot_tty_puts( vseg[vseg_id].name );
        boot_tty_puts("\n - vbase  = ");
        boot_tty_putw( vseg[vseg_id].vbase );
        boot_tty_puts("\n - length = ");
        boot_tty_putw( vseg[vseg_id].length );
        boot_tty_puts("\n - mode   = ");
        boot_tty_putw( vseg[vseg_id].mode );
        boot_tty_puts("\n - ident = ");
        boot_tty_putw( vseg[vseg_id].ident );
        boot_tty_puts("\n - psegname = ");
        boot_tty_puts( pseg[vseg[vseg_id].psegid].name );
        boot_tty_puts("\n\n");
    }

    // vspaces
    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {
        boot_tty_puts("vspace ");
        boot_tty_putw(vspace_id);

        boot_tty_puts("\n - name    = ");
        boot_tty_puts( vspace[vspace_id].name ); 
        boot_tty_puts("\n - binpath = ");
        boot_tty_puts( vspace[vspace_id].binpath ); 
        boot_tty_puts("\n - vsegs   = ");
        boot_tty_putw( vspace[vspace_id].vsegs );
        boot_tty_puts("\n - tasks   = ");
        boot_tty_putw( vspace[vspace_id].tasks );
        boot_tty_puts("\n - mwmrs   = ");
        boot_tty_putw( vspace[vspace_id].mwmrs );
        boot_tty_puts("\n - ttys    = ");
        boot_tty_putw( vspace[vspace_id].ttys );
        boot_tty_puts("\n\n");

        for ( vseg_id = vspace[vspace_id].vseg_offset ; 
              vseg_id < (vspace[vspace_id].vseg_offset + vspace[vspace_id].vsegs) ; 
              vseg_id++ )
        {
            boot_tty_puts("    private vseg ");
            boot_tty_putw( vseg_id );

            boot_tty_puts("\n    - name   = ");
            boot_tty_puts( vseg[vseg_id].name );
            boot_tty_puts("\n    - vbase  = ");
            boot_tty_putw( vseg[vseg_id].vbase );
            boot_tty_puts("\n    - length = ");
            boot_tty_putw( vseg[vseg_id].length );
            boot_tty_puts("\n    - mode   = ");
            boot_tty_putw( vseg[vseg_id].mode );
            boot_tty_puts("\n    - ident = ");
            boot_tty_putw( vseg[vseg_id].ident );
            boot_tty_puts("\n    - psegname = ");
            boot_tty_puts( pseg[vseg[vseg_id].psegid].name );
            boot_tty_puts("\n\n");
        }

        for ( task_id = vspace[vspace_id].vseg_offset ; 
              task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks) ; 
              task_id++ )
        {
            boot_tty_puts("     task");
            boot_tty_putw( task_id );

            boot_tty_puts("\n     - name = ");
            boot_tty_puts( task[task_id].name );
            boot_tty_puts("\n     - clusterid = ");
            boot_tty_putw( task[task_id].clusterid );
            boot_tty_puts("\n     - proclocid = ");
            boot_tty_putw( task[task_id].proclocid );
            boot_tty_puts("\n     - vseglocid = ");
            boot_tty_putw( task[task_id].vseglocid );
            boot_tty_puts("\n     - startid   = ");
            boot_tty_putw( task[task_id].startid );
            boot_tty_puts("\n     - ttylocid  = ");
            boot_tty_putw( task[task_id].ttylocid );
            boot_tty_puts("\n\n");
        }
    }
} // end boot_print_mapping_info()

//////////////////////////////////////////////////////////////////////////////
// boot_pseg_get() 
// This function returns the pointer on a physical segment
// identified  by the segment index.
//////////////////////////////////////////////////////////////////////////////
in_boot mapping_pseg_t* boot_pseg_get( unsigned int seg_id)
{
    mapping_header_t* header = (mapping_header_t*)&seg_boot_mapping_base;
    mapping_pseg_t*   pseg   = boot_get_pseg_base( header );

    // checking argument
    if ( seg_id >= header->psegs )
    {
        boot_tty_puts("\n[BOOT ERROR] : seg_id argument too large\n");
        boot_tty_puts("               in function boot_pseg_get()\n");
        boot_exit();
    }

    return &pseg[seg_id];                                    
} // end boot_pseg_get()

//////////////////////////////////////////////////////////////////////////////
// boot_add_pte() 
// This function registers a new PTE in the page table pointed
// by the vspace_id argument, and updates both PT1 and PT2.
// A new PT2 is used when required.
// 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.
//////////////////////////////////////////////////////////////////////////////
in_boot void boot_add_pte( unsigned int    vspace_id,    
                           unsigned int    vpn,           
                           unsigned int    flags,
                           unsigned int    ppn )
{
    unsigned int    ix1;
    unsigned int    ix2;
    unsigned int    ptba;       // PT2 base address
    unsigned int    pt2_id;     // PT2 index
    unsigned int*   pt_flags;   // pointer on the pte_flags = &PT2[2*ix2]    
    unsigned int*   pt_ppn;     // pointer on the pte_ppn   = &PT2[2*ix2+1]  

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

    // get the page table base address
    page_table_t* pt = (page_table_t *)(&_ptab_array[vspace_id]);

    if ( (pt->pt1[ix1] & PTE_V) == 0 )   // set a new PTD in PT1 
    {
        pt2_id = _next_free_pt2[vspace_id];
        if ( pt2_id == GIET_NB_PT2_MAX )
        {
            boot_tty_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
            boot_tty_puts("the GIET_NB_PT2_MAX parameter is too small\n"); 
            boot_exit();
        }
        else
        {
            ptba = (unsigned int)pt + PT1_SIZE + PT2_SIZE*pt2_id;
            pt->pt1[ix1] = PTE_V | PTE_T | (ptba >> 12);    
            _next_free_pt2[vspace_id] = pt2_id + 1;
        }
    }
    else
    {
        ptba = pt->pt1[ix1] << 12;
    }

    // set PTE2 after checking double mapping error
    pt_flags = (unsigned int*)(ptba + 8*ix2);
    pt_ppn   = (unsigned int*)(ptba + 8*ix2 + 4);

    if ( ( *pt_flags & PTE_V) != 0 )    // page already mapped
    {
        boot_tty_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
        boot_tty_puts("page already mapped\n");
        boot_exit();
    }
    else                                          // set PTE2
    {
        *pt_flags = flags;
        *pt_ppn   = ppn;
    }
} // end boot_add_pte()
                
/////////////////////////////////////////////////////////////////////
// This function build the page table for a given vspace. 
// The physical base addresses for all vsegs (global and private)
// must have been previously computed.
// It initializes the MWMR channels.
/////////////////////////////////////////////////////////////////////
in_boot void boot_vspace_pt_build( unsigned int vspace_id )
{
    unsigned int    vseg_id;
    unsigned int    npages;
    unsigned int    ppn;
    unsigned int    vpn;
    unsigned int    flags;
    unsigned int    page_id;

    mapping_header_t*  header = (mapping_header_t*)&seg_boot_mapping_base;  
    mapping_vspace_t*  vspace = boot_get_vspace_base( header );
    mapping_vseg_t*    vseg   = boot_get_vseg_base( header );

    // global segments
    for ( vseg_id = 0 ; vseg_id < header->globals ; vseg_id++ )
    {
        vpn       = vseg[vseg_id].vbase >> 12;
        ppn       = vseg[vseg_id].pbase >> 12;
        npages    = vseg[vseg_id].length >> 12;
        if ( (vseg[vseg_id].length & 0xFFF) != 0 ) npages++;

        flags = PTE_V;
        if ( vseg[vseg_id].mode & C_MODE_MASK )  flags = flags | PTE_C;
        if ( vseg[vseg_id].mode & X_MODE_MASK )  flags = flags | PTE_X;
        if ( vseg[vseg_id].mode & W_MODE_MASK )  flags = flags | PTE_W;
        if ( vseg[vseg_id].mode & U_MODE_MASK )  flags = flags | PTE_U;

#if BOOT_DEBUG_PT
boot_tty_puts("- vseg ");
boot_tty_puts( vseg[vseg_id].name );
boot_tty_puts(" / flags = ");
boot_tty_putw( flags );
boot_tty_puts(" / npages = ");
boot_tty_putw( npages );
boot_tty_puts("\n");
#endif        
        // loop on 4K pages
        for ( page_id = 0 ; page_id < npages ; page_id++ )
        {
            boot_add_pte( vspace_id,
                          vpn,
                          flags,
                          ppn );
            vpn++;
            ppn++;
        }
    }
    
    // private segments
    for ( vseg_id = vspace[vspace_id].vseg_offset ; 
          vseg_id < (vspace[vspace_id].vseg_offset + vspace[vspace_id].vsegs) ; 
          vseg_id++ )
    {
        vpn       = vseg[vseg_id].vbase >> 12;
        ppn       = vseg[vseg_id].pbase >> 12;
        npages    = vseg[vseg_id].length >> 12;
        if ( (vseg[vseg_id].length & 0xFFF) != 0 ) npages++;

        flags = PTE_V;
        if ( vseg[vseg_id].mode & C_MODE_MASK )  flags = flags | PTE_C;
        if ( vseg[vseg_id].mode & X_MODE_MASK )  flags = flags | PTE_X;
        if ( vseg[vseg_id].mode & W_MODE_MASK )  flags = flags | PTE_W;
        if ( vseg[vseg_id].mode & U_MODE_MASK )  flags = flags | PTE_U;

#if BOOT_DEBUG_PT
boot_tty_puts("- vseg ");
boot_tty_puts( vseg[vseg_id].name );
boot_tty_puts(" / flags = ");
boot_tty_putw( flags );
boot_tty_puts("\n");
#endif        
        // loop on 4K pages
        for ( page_id = 0 ; page_id < npages ; page_id++ )
        {
            boot_add_pte( vspace_id,
                          vpn,
                          flags,
                          ppn );
            vpn++;
            ppn++;
        }

        // initializes MWMR channel if vseg is a MWMR
        // the channel storage capacity is (vseg.legth/4 - 5) words
        if ( vseg[vseg_id].mwmr )
        {
            mwmr_channel_t* mwmr = (mwmr_channel_t*)(vseg[vseg_id].pbase);
            mwmr->ptw   = 0;
            mwmr->ptr   = 0;
            mwmr->sts   = 0;
            mwmr->depth = (vseg[vseg_id].length>>2) - 5;
            mwmr->lock  = 0;

#if BOOT_DEBUG_PT
boot_tty_puts("   MWMR channel depth = ");
boot_tty_putw( mwmr->depth );
boot_tty_puts("\n");
#endif

        }
    }
} // end boot_vspace_pt_build()

//////////////////////////////////////////////////////////////////////
// This function uses the page tables to translate a virtual address
// to a physical address, depending on the vspace index.
//////////////////////////////////////////////////////////////////////
in_boot unsigned int boot_translate( unsigned int vaddr,
                                     unsigned int vspace_id )
{
    page_table_t*   ptp;
    unsigned int*   ptba;
    unsigned int    paddr;

    // compute indexes
    unsigned int    ix1    = (vaddr >> 21) & 0x7FF;
    unsigned int    ix2    = (vaddr >> 12) & 0x1FF;
    unsigned int    offset = vaddr & 0xFFF;
    
    // get the page table base address 
    ptp = (page_table_t*)((char*)&seg_kernel_pt_base + vspace_id*sizeof(page_table_t));
    
    // compute PTBA     
    ptba = (unsigned int*)(ptp->pt1[ix1] << 12);

    // compute paddr    
    paddr = (ptba[2*ix2 + 1] << 12) + offset;

#if BOOT_DEBUG_TRANSLATE
boot_tty_puts("\nAddress Translation\n");
boot_tty_puts("- vaddr = ");
boot_tty_putw( vaddr );
boot_tty_puts("\n");
boot_tty_puts("- ix1   = ");
boot_tty_putw( ix1 );
boot_tty_puts("\n");
boot_tty_puts("- ix2   = ");
boot_tty_putw( ix2 );
boot_tty_puts("\n");
boot_tty_puts("- ptp   = ");
boot_tty_putw( (unsigned int)ptp );
boot_tty_puts("\n");
boot_tty_puts("- ptba  = ");
boot_tty_putw( (unsigned int)ptba );
boot_tty_puts("\n");
boot_tty_puts("- paddr = ");
boot_tty_putw( paddr );
boot_tty_puts("\n");
#endif

    return paddr;
} // end boot_translate()

///////////////////////////////////////////////////////////////////////////////
// This function initialises the task context for a given vspace.
// There is a private context array for each vspace, indexed by the
// (task_id, proc_id) composite index.
// The following values are written in the task context:
// - SP     stack pointer = stack_base + stack_length
// - RA     return address = &boot_eret
// - EPC    start address = start_vector[task->startid]
// - SR     status register = OxFF13
// - TTY    TTY index = base_tty_id + tty_local_id
// - PTPR   page table base address / 8K
// - MODE   mmu_mode = 0xF (TLBs and caches activated)
// It statically allocates the task to the proper scheduler
// (one scheduler per processor).
////////////////////////////////////////////////////////////////////////////////
in_boot void boot_task_map( unsigned int        task_id,    // global index
                            unsigned int        vspace_id,  // global index
                            unsigned int        base_tty_id,
                            unsigned int*       start_vector )
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base;  

    mapping_vseg_t*     vseg   = boot_get_vseg_base(header);
    mapping_task_t*     task   = boot_get_task_base(header);
    mapping_vspace_t*   vspace = boot_get_vspace_base(header);

    unsigned int        vseg_id;
    unsigned int        loc_id;
    unsigned int        proc_id;

    unsigned int        sp;
    unsigned int        ra   = (unsigned int)&boot_eret;
    unsigned int        epc  = start_vector[task[task_id].startid];
    unsigned int        tty  = base_tty_id + task[task_id].ttylocid; 
    unsigned int        sr   = 0x0000FF13;
    unsigned int        ptpr = ((unsigned int)&_ptab_array[vspace_id]) >> 13;
    unsigned int        mode = 0xF;

    // check values
    if ( task[task_id].proclocid >= NB_PROCS )
    {
        boot_tty_puts("\n[BOOT ERROR] : processor index too large for task ");
        boot_tty_puts( task[task_id].name );
        boot_tty_puts(" in vspace ");
        boot_tty_puts( vspace[vspace_id].name );
        boot_tty_puts("\n");
        boot_exit();
    }
    if ( task[task_id].clusterid >= NB_CLUSTERS )
    {
        boot_tty_puts("\n[BOOT ERROR] : cluster index too large for task ");
        boot_tty_puts( task[task_id].name );
        boot_tty_puts(" in vspace ");
        boot_tty_puts( vspace[vspace_id].name );
        boot_tty_puts("\n");
        boot_exit();
    }
    if ( task[task_id].vseglocid >= vspace->vsegs )
    {
        boot_tty_puts("\n[BOOT ERROR] : vseg index too large for task ");
        boot_tty_puts( task[task_id].name );
        boot_tty_puts(" in vspace ");
        boot_tty_puts( vspace[vspace_id].name );
        boot_tty_puts("\n");
        boot_exit();
    }
    if ( task[task_id].startid >= vspace->tasks )
    {
        boot_tty_puts("\n[BOOT ERROR] : start index too large for task ");
        boot_tty_puts( task[task_id].name );
        boot_tty_puts(" in vspace ");
        boot_tty_puts( vspace[vspace_id].name );
        boot_tty_puts("\n");
        boot_exit();
    }
    if ( tty >= NB_TTYS )
    {
        boot_tty_puts("\n[BOOT ERROR] : TTY index too large for task ");
        boot_tty_puts( task[task_id].name );
        boot_tty_puts(" in vspace ");
        boot_tty_puts( vspace[vspace_id].name );
        boot_tty_puts("\n");
        boot_exit();
    }

    // get stack pointer value
    vseg_id = task[task_id].vseglocid + vspace[vspace_id].vseg_offset;
    sp = vseg[vseg_id].vbase + vseg[vseg_id].length;

    // compute global processor index
    proc_id = task[task_id].clusterid * NB_PROCS + task[task_id].proclocid;

    // check local task index
    loc_id = _scheduler[proc_id].tasks;
    if ( loc_id >= GIET_NB_TASKS_MAX )
    {
        boot_tty_puts("\n[BOOT ERROR] : too much tasks allocated to processor ");
        boot_tty_putw( proc_id );
        boot_tty_puts("\n");
        boot_exit();
    }
    
    // update number of tasks allocated to scheduler
    _scheduler[proc_id].tasks = loc_id + 1;

    // initializes the task context
    _scheduler[proc_id].context[loc_id][CTX_SR_ID]   = sr;
    _scheduler[proc_id].context[loc_id][CTX_SP_ID]   = sp;
    _scheduler[proc_id].context[loc_id][CTX_RA_ID]   = ra;
    _scheduler[proc_id].context[loc_id][CTX_EPC_ID]  = epc;
    _scheduler[proc_id].context[loc_id][CTX_TTY_ID]  = tty;
    _scheduler[proc_id].context[loc_id][CTX_PTPR_ID] = ptpr;
    _scheduler[proc_id].context[loc_id][CTX_MODE_ID] = mode;
    
#if BOOT_DEBUG_CTX
boot_tty_puts("Task ");
boot_tty_puts( task[task_id].name );
boot_tty_puts(" allocated to processor ");
boot_tty_putw( proc_id );
boot_tty_puts(" / loc_id = ");
boot_tty_putw( loc_id );
boot_tty_puts("\n");

boot_tty_puts("  - SR          = ");
boot_tty_putw( sr );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_SR_ID] );
boot_tty_puts("\n");

boot_tty_puts("  - RA          = ");
boot_tty_putw( ra );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_RA_ID] );
boot_tty_puts("\n");

boot_tty_puts("  - SP          = ");
boot_tty_putw( sp );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_SP_ID] );
boot_tty_puts("\n");

boot_tty_puts("  - EPC         = ");
boot_tty_putw( epc );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_EPC_ID] );
boot_tty_puts("\n");

boot_tty_puts("  - TTY         = ");
boot_tty_putw( tty );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_TTY_ID] );
boot_tty_puts("\n");

boot_tty_puts("  - PTPR        = ");
boot_tty_putw( ptpr<<13 );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_PTPR_ID] );
boot_tty_puts("\n");

boot_tty_puts("  - MODE        = ");
boot_tty_putw( mode );
boot_tty_puts("  saved at ");
boot_tty_putw( (unsigned int)&_scheduler[proc_id].context[loc_id][CTX_MODE_ID] );
boot_tty_puts("\n");
#endif

} // end boot_task_map()

///////////////////////////////////////////////////////////////////////////
// This function compute the physical base address for a vseg
// as specified in the mapping info data structure.
// It updates the pbase field of the vseg.
// It updates the page allocator (nextfreepage field of the pseg),
// and checks a possible pseg overflow.
///////////////////////////////////////////////////////////////////////////
in_boot void boot_vseg_map( mapping_vseg_t* vseg ) 
{
    unsigned int    pages;

    // check vseg alignment on 4K pages
    if ( (vseg->vbase & 0xfff) != 0 )
    {
        boot_tty_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
        boot_tty_puts("virtual segment base address not aligned: ");
        boot_tty_puts( vseg->name );
        boot_tty_puts("\n");
        boot_exit();
    }
    
    // computes number of pages
    pages = vseg->length >> 12;
    if ( (vseg->length & 0xFFF) != 0 ) pages++;

    // get physical segment pointer
    mapping_pseg_t*  pseg = boot_pseg_get( vseg->psegid );

    // compute physical base address
    if ( vseg->ident != 0 )            // identity mapping required
    {
        // check physical segment overflow  
        if ( (vseg->vbase < pseg->base) || 
             ((vseg->vbase + vseg->length) > (pseg->base + pseg->length)) )
        {
            boot_tty_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
            boot_tty_puts("impossible identity mapping for virtual segment: ");
            boot_tty_puts( vseg->name ); 
            boot_tty_puts("\n"); 
            boot_exit();
        }
        vseg->pbase = vseg->vbase;
    }
    else                                // unconstrained mapping
    {
        // check physical segment overflow
        if ( (vseg->vbase + vseg->length) > (pseg->base + pseg->length) )
        {
            boot_tty_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
            boot_tty_puts("physical segment ");
            boot_tty_puts( pseg->name ); 
            boot_tty_puts(" is too small to map virtual segment");
            boot_tty_puts( vseg->name ); 
            boot_tty_puts("\n");
            boot_exit();
        }
        vseg->pbase = pseg->base + (pseg->next_free_page<<12);
        pseg->next_free_page = pseg->next_free_page + pages;
    }

#if BOOT_DEBUG_PT
boot_tty_puts("- vseg ");
boot_tty_puts( vseg->name );
boot_tty_puts(" : vbase = ");
boot_tty_putw( vseg->vbase );
boot_tty_puts(" / pbase = ");
boot_tty_putw( vseg->pbase );
boot_tty_puts("\n");
#endif  

} // end boot_vseg_map()

/////////////////////////////////////////////////////////////////////
// This function cheks the mapping_info data structure 
/////////////////////////////////////////////////////////////////////
in_boot void boot_check_mapping()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base;  

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

#if BOOT_DEBUG_VIEW
boot_print_mapping_info();
#endif

    // checking double definition of NB_CLUSTERS
    if ( header->clusters != NB_CLUSTERS )
    {
        boot_tty_puts("\n[BOOT ERROR] Incoherent NB_CLUSTERS");
        boot_tty_puts("\n             - In giet_config,  value = ");
        boot_tty_putw ( NB_CLUSTERS );
        boot_tty_puts("\n             - In mapping_info, value = ");
        boot_tty_putw ( header->clusters );
        boot_tty_puts("\n");
        boot_exit();
    }

    // checking double definition of NB_TTYS
    if ( header->ttys != NB_TTYS )
    {
        boot_tty_puts("\n[BOOT ERROR] Incoherent NB_TTYS");
        boot_tty_puts("\n             - In giet_config,  value = ");
        boot_tty_putw ( NB_TTYS );
        boot_tty_puts("\n             - In mapping_info, value = ");
        boot_tty_putw ( header->ttys );
        boot_tty_puts("\n");
        boot_exit();
    }

    // GIET_NB_PT2_MAX must be even
    if ( (GIET_NB_PT2_MAX & 0x1) != 0 )
    {
        boot_tty_puts("\n[BOOT ERROR] : GIET_NB_PT2_MAX must be an even numver\n");
        boot_tty_puts("\n");
        boot_exit();
    }

    // number of virtual spaces no larger than GIET_NB_VSPACE_MAX
    if ( header->vspaces > GIET_NB_VSPACE_MAX )
    {
        boot_tty_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
        boot_tty_puts("\n");
        boot_exit();
    }
} // end boot_check_mapping()

/////////////////////////////////////////////////////////////////////
// This function builds the page tables for all virtual spaces 
// defined in the mapping_info data structure.
// For each virtual space, it maps both the global virtual segments 
// (replicated in all vspaces), and the private virtuals segments.
/////////////////////////////////////////////////////////////////////
in_boot void boot_pt_init()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base;  

    mapping_vspace_t*   vspace = boot_get_vspace_base( header );     
    mapping_pseg_t*     pseg   = boot_get_pseg_base( header ); 
    mapping_vseg_t*     vseg   = boot_get_vseg_base( header );

    unsigned int        vspace_id;  
    unsigned int        vseg_id;
    unsigned int        pseg_id;

    // first loop on virtual spaces to map global vsegs
    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {

#if BOOT_DEBUG_PT
boot_tty_puts("\n******* mapping global vsegs in vspace ");
boot_tty_puts(vspace[vspace_id].name);
boot_tty_puts(" ********\n");
#endif
            
        // physical page allocators must be re-initialised for each vspace
        for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
        {
            pseg[pseg_id].next_free_page = 0;
        }

        for ( vseg_id = 0 ; vseg_id < header->globals ; vseg_id++ )
        {
            boot_vseg_map( &vseg[vseg_id] );
        }
    } 

    // second loop on virtual spaces to map private vsegs
    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {

#if BOOT_DEBUG_PT
boot_tty_puts("\n******* mapping private vsegs in vspace ");
boot_tty_puts(vspace[vspace_id].name);
boot_tty_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] ); 
        }
    } 

    // third loop on the vspaces to build the page tables
    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {

#if BOOT_DEBUG_PT
boot_tty_puts("\n******* building page table for vspace ");
boot_tty_puts(vspace[vspace_id].name);
boot_tty_puts(" ********\n");
#endif
            
        boot_vspace_pt_build( vspace_id );
    } 
} // end boot_pt_init()

///////////////////////////////////////////////////////////////////////////////
// This function sets the schedulers default values for all processors
// (tasks <= 0, and current <= 0).
// Then it scan all tasks (in all vspaces) to initialise the schedulers, 
// the tasks contexts, as defined in the mapping_info data structure. 
// A global TTY index is allocated to each task, as specified in the mapping.
// TTY0 is reserved for the kernel.
///////////////////////////////////////////////////////////////////////////////
in_boot void boot_tcg_init()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base;  

    mapping_vspace_t*   vspace  = boot_get_vspace_base( header );     
    mapping_vseg_t*     vseg    = boot_get_vseg_base( header );     
    mapping_cluster_t*  cluster = boot_get_cluster_base( header );

    unsigned int*       start_vector_base;

    unsigned int        base_tty_id = 1;     // TTY allocator

    unsigned int        cluster_id;  
    unsigned int        proc_id;  
    unsigned int        vspace_id;  
    unsigned int        task_id;

    // initialise the schedulers (not done by the compiler/loader)
    for ( cluster_id = 0 ; cluster_id < header->clusters ; cluster_id++ )
    {
        for ( proc_id = 0 ; proc_id < cluster[cluster_id].procs ; proc_id++ )
        {
            if ( proc_id >= NB_PROCS )
            {
                boot_tty_puts("\n[BOOT ERROR] The number of processors in cluster ");
                boot_tty_putw( cluster_id );
                boot_tty_puts(" is larger than NB_PROCS \n");
                boot_exit();
            }
            _scheduler[cluster_id*NB_PROCS+proc_id].tasks   = 0;
            _scheduler[cluster_id*NB_PROCS+proc_id].current = 0;
        }
    }

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

#if BOOT_DEBUG_CTX
boot_tty_puts("\n******* mapping tasks and channels in vspace ");
boot_tty_puts(vspace[vspace_id].name);
boot_tty_puts(" ********\n");
#endif

        // Get the physical address of the start_vector for the vspace.
        // The start_vector is stored at the beginning of the seg_data segment, 
        // and contains the start addresses for all tasks defined in a vspace.
        // The seg_data segment must be the first vseg defined in 
        // the mapping_info data structure. 
        mapping_vseg_t* vseg_data = &vseg[ vspace[vspace_id].vseg_offset];
        start_vector_base = (unsigned int*)boot_translate( vseg_data->vbase,
                                                           vspace_id );
        // map tasks
        for ( task_id = vspace[vspace_id].task_offset ; 
              task_id < (vspace[vspace_id].task_offset + vspace[vspace_id].tasks) ; 
              task_id++ )
        {
            boot_task_map( task_id, 
                           vspace_id,
                           base_tty_id,
                           start_vector_base );            
        }

        // increment TTY allocator
        base_tty_id = base_tty_id + vspace[vspace_id].ttys;    
    }
} // end boot_tc_init()

/////////////////////////////////////////////////////////////////////
// This function signals the mapping completion by writing
// a new value in the mapping_info signature.
/////////////////////////////////////////////////////////////////////
in_boot void boot_mapping_done()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base;  
    header->signature = OUT_MAPPING_SIGNATURE;
} // end boot_mapping_done()

////////////////////////////////////////////////////////////////////////////////
//      boot_peri_init()
// This generic function initializes the interrupt vector, the ICU masks, 
// and the timers for the context switch.
// The hardware parameters are NB_CLUSTERS, NB_PROCS, NB_TIMERS, NB_DMAS
// CLUSTER_SPAN, seg_icu_base, seg_timer_base.
// The number of processor per cluster cannot be larger than 8.
// The total number of TTYs cannot be larger than 15. 
// The NB_TIMERS, NB_DMAS & NB_PROCS parameters must be equal. 
////////////////////////////////////////////////////////////////////////////////
in_boot void boot_peri_init()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_boot_mapping_base; 
    mapping_cluster_t* cluster = boot_get_cluster_base( header );

    unsigned int cluster_id;

    if ( NB_TIMERS != NB_PROCS )
    {
        boot_tty_puts("\n[BOOT ERROR] NB_TIMERS != NB_PROCS\n");
        boot_exit();
    }
    if ( NB_DMAS != NB_PROCS )
    {
        boot_tty_puts("\n[BOOT ERROR] NB_DMAS != NB_PROCS\n");
        boot_exit();
    }

    // interrupt vector initialisation

    _interrupt_vector[0]  = &_isr_ioc;

    _interrupt_vector[1]  = &_isr_tty_get_0;
    _interrupt_vector[2]  = &_isr_tty_get_1;
    _interrupt_vector[3]  = &_isr_tty_get_2;
    _interrupt_vector[4]  = &_isr_tty_get_3;
    _interrupt_vector[5]  = &_isr_tty_get_4;
    _interrupt_vector[6]  = &_isr_tty_get_5;
    _interrupt_vector[7]  = &_isr_tty_get_6;
    _interrupt_vector[8]  = &_isr_tty_get_7;
    _interrupt_vector[9]  = &_isr_tty_get_8;
    _interrupt_vector[10] = &_isr_tty_get_9;
    _interrupt_vector[11] = &_isr_tty_get_10;
    _interrupt_vector[12] = &_isr_tty_get_11;
    _interrupt_vector[13] = &_isr_tty_get_12;
    _interrupt_vector[14] = &_isr_tty_get_13;
    _interrupt_vector[14] = &_isr_tty_get_14;


    _interrupt_vector[16] = &_isr_switch;
    _interrupt_vector[17] = &_isr_dma;
    _interrupt_vector[18] = &_isr_switch;
    _interrupt_vector[19] = &_isr_dma;
    _interrupt_vector[20] = &_isr_switch;
    _interrupt_vector[21] = &_isr_dma;
    _interrupt_vector[22] = &_isr_switch;
    _interrupt_vector[23] = &_isr_dma;
    _interrupt_vector[24] = &_isr_switch;
    _interrupt_vector[25] = &_isr_dma;
    _interrupt_vector[26] = &_isr_switch;
    _interrupt_vector[27] = &_isr_dma;
    _interrupt_vector[28] = &_isr_switch;
    _interrupt_vector[29] = &_isr_dma;
    _interrupt_vector[30] = &_isr_switch;
    _interrupt_vector[31] = &_isr_dma;

    // ICU MASKs and TIMERS initialisation

    volatile unsigned int* icu   = (unsigned int*)&seg_icu_base;
    volatile unsigned int* timer = (unsigned int*)&seg_timer_base;
    
    for ( cluster_id = 0 ; cluster_id < header->clusters ; cluster_id++ )
    {
        if ( cluster[cluster_id].procs == 0 ) break;

        icu[ICU_MASK_SET + 0*ICU_SPAN] = 0x000380FF;    // ICU_MASK for proc 0
        if ( _scheduler[cluster_id*NB_PROCS + 0].tasks > 1 )
        {
           timer[TIMER_PERIOD + 0*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 0*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 1 ) break;

        icu[ICU_MASK_SET + 1*ICU_SPAN] = 0x000C0000;    // ICU_MASK for proc 1
        if ( _scheduler[cluster_id*NB_PROCS + 1].tasks > 1 )
        {
           timer[TIMER_PERIOD + 1*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 1*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 2 ) break;

        icu[ICU_MASK_SET + 2*ICU_SPAN] = 0x00300000;    // ICU_MASK for proc 2
        if ( _scheduler[cluster_id*NB_PROCS + 2].tasks > 1 )
        {
           timer[TIMER_PERIOD + 2*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 2*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 3 ) break;

        icu[ICU_MASK_SET + 3*ICU_SPAN] = 0x00C00000;    // ICU_MASK for proc 3
        if ( _scheduler[cluster_id*NB_PROCS + 3].tasks > 1 )
        {
           timer[TIMER_PERIOD + 3*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 3*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 4 ) break;
        icu[ICU_MASK_SET + 4*ICU_SPAN] = 0x03000000;    // ICU_MASK for proc 4

        if ( _scheduler[cluster_id*NB_PROCS + 4].tasks > 1 )
        {
           timer[TIMER_PERIOD + 4*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 4*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 5 ) break;

        icu[ICU_MASK_SET + 5*ICU_SPAN] = 0x0C000000;    // ICU_MASK for proc 5
        if ( _scheduler[cluster_id*NB_PROCS + 5].tasks > 1 )
        {
           timer[TIMER_PERIOD + 5*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 5*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 6 ) break;

        icu[ICU_MASK_SET + 6*ICU_SPAN] = 0x30000000;    // ICU_MASK for proc 6
        if ( _scheduler[cluster_id*NB_PROCS + 6].tasks > 1 )
        {
           timer[TIMER_PERIOD + 6*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 6*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs == 7 ) break;

        icu[ICU_MASK_SET + 7*ICU_SPAN] = 0xC0000000;    // ICU_MASK for proc 7
        if ( _scheduler[cluster_id*NB_PROCS + 7].tasks > 1 )
        {
           timer[TIMER_PERIOD + 7*TIMER_SPAN] = GIET_TICK_VALUE;
           timer[TIMER_MODE   + 7*TIMER_SPAN] = 0x3;
        }

        if ( cluster[cluster_id].procs > 8 ) 
        {
            boot_tty_puts("\n[BOOT ERROR] The number of processors per cluster\n");
            boot_tty_puts("               cannot be larger than 8\n");
            boot_exit();
        }
        icu   = icu   + (CLUSTER_SPAN>>2);
        timer = timer + (CLUSTER_SPAN>>2);
    }
} // end boot_peri_init()
 
////////////////////////////////////////////////////////////////////////////////////
// boot_init()
// This function is executed by one single processor to initialize the page
// tables, the tasks contexts and the peripherals, for all applications.
////////////////////////////////////////////////////////////////////////////////////
in_boot void boot_init()
{
    // checking mapping_info
    boot_check_mapping();

    // building page tables
    boot_pt_init();
    boot_tty_puts("\n[BOOT] Page Tables completed at cycle ");
    boot_tty_putw( boot_time() );
    boot_tty_puts("\n");

    // building tasks contexts
    boot_tcg_init();
    boot_tty_puts("\n[BOOT] Task Contexts completed at cycle ");
    boot_tty_putw( boot_time() );
    boot_tty_puts("\n");

    // Initialize peripherals
    boot_peri_init();
    boot_tty_puts("\n[BOOT] Peripherals completed at cycle ");
    boot_tty_putw( boot_time() );
    boot_tty_puts("\n");

    // signals completion to all processors
    boot_mapping_done();

} // 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=cpp:expandtab:shiftwidth=4:tabstop=4:softtabstop=4