source: soft/giet_vm/boot/boot_handler.c @ 163

//////////////////////////////////////////////////////////////////////////////////
// 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 build all the pages tables then jumps
// in to the seg_kernel_init segment with an activated MMU. 
//
// 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_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), 
// - static placement of tasks on the processors, 
// - static placement of virtual segments (vseg) in the physical segments (pseg).
// - static placement of virtual objects (vobj) on virtual segments (vseg).
//
// 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 in the MAPPING_INFO_BINARY data structure(using the length field). 
// The value is calculated and put in _max_pte2 indexed by the vspace_id.
// The physical alignment constraints, is ensured by the align flag in the MAPPING_INFO 
// structure.
// 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][_max_pte2[vspace_id]], indexed by
//   the (ix2) field of the VPN, and by the PT2 index (pt2_id).
//   Each PT2 contains 512 PTE2 of 8bytes => 4Kbytes * _max_pte2[vspace_id]
// The size of each page table is 8K + (_max_pte2[vspace_id])*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 <mwmr.h>

#include <stdarg.h>


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

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

// Page Tables 
// Next free PT2 index 
unsigned int  _next_free_pt2[GIET_NB_VSPACE_MAX] =
                         { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };

// Max PT2 index 
unsigned int  _max_pte2[GIET_NB_VSPACE_MAX] =
                         { [0 ... GIET_NB_VSPACE_MAX-1] = 0 };

// Page table pointers
page_table_t* _ptabs[GIET_NB_VSPACE_MAX];

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

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

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


////////////////////////////////////////////////////////////////////////////
// boot_tty_puts()
// (it uses TTY0)
////////////////////////////////////////////////////////////////////////////
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)
////////////////////////////////////////////////////////////////////////////
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
/////////////////////////////////////////////////////////////////////////////
mapping_cluster_t* boot_get_cluster_base( mapping_header_t* header )
{
    return   (mapping_cluster_t*) ((char*)header +
                                  MAPPING_HEADER_SIZE);
}
/////////////////////////////////////////////////////////////////////////////
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);
}
/////////////////////////////////////////////////////////////////////////////
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);
}
/////////////////////////////////////////////////////////////////////////////
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);
}
/////////////////////////////////////////////////////////////////////////////
mapping_vobj_t* boot_get_vobj_base( mapping_header_t* header )
{
    return   (mapping_vobj_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 );
}
/////////////////////////////////////////////////////////////////////////////
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_VOBJ_SIZE*header->vobjs +
                                  MAPPING_VSEG_SIZE*header->vsegs);
}

/////////////////////////////////////////////////////////////////////////////
// print the content of the mapping_info data structure 
////////////////////////////////////////////////////////////////////////
#if BOOT_DEBUG_VIEW
void boot_print_mapping_info()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_mapping_base; 
    
    unsigned int                vspace_id;
    unsigned int                cluster_id;
    unsigned int                pseg_id;
    unsigned int                vseg_id;
    unsigned int                vobj_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 );;
    mapping_vobj_t*    vobj   = boot_get_vobj_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\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");
        for ( vobj_id = vseg[vseg_id].vobj_offset ; vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; vobj_id++ )
        {
                        boot_tty_puts("vobjs: \n");
            boot_tty_putw( vobj[vobj_id].name);
            boot_tty_puts("\n");
            boot_tty_puts("\t name     = ");
                        boot_tty_putw(  vobj[vobj_id].name);
                        boot_tty_puts("\n");
            boot_tty_puts("\t type     = ");
                        boot_tty_putw( vobj[vobj_id].type);
                        boot_tty_puts("\n");
            boot_tty_puts("\t length   = ");
                        boot_tty_putw(   vobj[vobj_id].length);
                        boot_tty_puts("\n");
            boot_tty_puts("\t align    = ");
                        boot_tty_putw(   vobj[vobj_id].align);
                        boot_tty_puts("\n");
            boot_tty_puts("\t binpath  = ");
                        boot_tty_putw(   vobj[vobj_id].binpath);
                        boot_tty_puts("\n\n");
        }
    }

    // vspaces
    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {
        unsigned int func_id = vspace[vspace_id].vobj_offset + vspace[vspace_id].funcs_offset; 
        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 - funcs    = ");
        boot_tty_puts( vobj[func_id].name ); 
        boot_tty_puts( vspace[vspace_id].name ); 
        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");
            for ( vobj_id = vseg[vseg_id].vobj_offset ; vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; vobj_id++ )
            {
                boot_tty_puts("\t\t vobjs     = ");
                                boot_tty_putw(     vobj[vobj_id].name);
                                boot_tty_puts("\n");
                boot_tty_puts("\t\t name     = ");
                                boot_tty_putw(     vobj[vobj_id].name);
                                boot_tty_puts("\n");
                boot_tty_puts("\t\t type     = ");
                                boot_tty_putw( vobj[vobj_id].type);
                                boot_tty_puts("\n");
                boot_tty_puts("\t\t length   = ");
                                boot_tty_putw(   vobj[vobj_id].length);
                                boot_tty_puts("\n");
                boot_tty_puts("\t\t align    = ");
                                boot_tty_putw(   vobj[vobj_id].align);
                                boot_tty_puts("\n");
                boot_tty_puts("\t\t binpath  = ");
                                boot_tty_putw(   vobj[vobj_id].binpath);
                                boot_tty_puts("\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     - vobjlocid = ");
            boot_tty_putw( task[task_id].vobjlocid );
            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()
#endif

//////////////////////////////////////////////////////////////////////////////
// boot_pseg_get() 
// This function returns the pointer on a physical segment
// identified  by the segment index.
//////////////////////////////////////////////////////////////////////////////
mapping_pseg_t* boot_pseg_get( unsigned int seg_id)
{
    mapping_header_t* header = (mapping_header_t*)&seg_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.
//
// The parametre global is a boolean taht indicate wether a global vseg is
// being mapped.
//////////////////////////////////////////////////////////////////////////////
void boot_add_pte( unsigned int    vspace_id,    
                   unsigned int    vpn,           
                   unsigned int    flags,
                   unsigned int    ppn,
                   unsigned char   global )
{
    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

        
    unsigned int max_pte2   = _max_pte2[vspace_id];
    if(max_pte2 == 0)
    {
        boot_tty_puts("Unfound page table for vspace ");
        boot_tty_putw(vspace_id);
        boot_tty_puts("\n");
        boot_exit();
    }

    page_table_t* pt    = (page_table_t *)_ptabs[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 == max_pte2 )
        {
            boot_tty_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
            boot_tty_puts("the length of the ptab vobj 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
    {
        if(global)
        {
            boot_tty_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
            boot_tty_puts("page already mapped\n");
            boot_exit();
        }else
        {
            /**
             * The case where a global vseg is already mapped as private vseg of a
             * vspace_id. Typically used when a vseg is being replicated.
             */  
            boot_tty_puts("\n[BOOT] global PTE for vspace ");
            boot_tty_putw(vspace_id);
            boot_tty_puts(" already mapped, vpn = ");
            boot_tty_putw(vpn);
            boot_tty_puts("\n");
            return;
        }
    }

    // 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.
/////////////////////////////////////////////////////////////////////
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_mapping_base;  
    mapping_vspace_t*  vspace = boot_get_vspace_base( header );
    mapping_vseg_t*    vseg   = boot_get_vseg_base( header );
    
    // 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,
                          0 );
            vpn++;
            ppn++;
        }
    }

    // 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,
                          1 );
            vpn++;
            ppn++;
        }
    }

} // end boot_vspace_pt_build()


///////////////////////////////////////////////////////////////////////////
// Align the value "toAlign" to the required alignement indicated by
// alignPow2 ( the logarithme of 2 the alignement).
///////////////////////////////////////////////////////////////////////////
unsigned int align_to( unsigned toAlign, unsigned alignPow2)
{
    unsigned mask = (1 << alignPow2) - 1;
    return ((toAlign + mask ) & ~mask );//page aligned 
}

///////////////////////////////////////////////////////////////////////////
// Initialise vobjs
// For now only one type is initialised the: PTAB
//
// param:
//  vobj: the vobj to initialise
//  region_id: the vspace in wich the vobj is located or the global space(-1).
///////////////////////////////////////////////////////////////////////////
void initailise_vobj(mapping_vobj_t* vobj, unsigned int region_id)
{
    if(vobj->type == PTAB)
    {
        if(region_id == ((unsigned int) -1))
        {
            boot_tty_puts( "No PTAB vobjs are allowed in the global region" );
            boot_exit();
        }
        if(vobj->length < (PT1_SIZE + PT2_SIZE) ) //at least one pt2 => ( max_pt2 >= 1)
        {
            boot_tty_puts("PTAB too small, minumum size is ");
            boot_tty_putw( PT1_SIZE + PT2_SIZE);
            boot_exit();
        }

        _ptabs[region_id]        = (page_table_t*) vobj->paddr;
        _max_pte2[region_id]    = (vobj->length - PT1_SIZE) / PT2_SIZE;

#if BOOT_DEBUG_VIEW
        boot_tty_puts("ptabs for vspace ");
        boot_tty_putw(region_id);
        boot_tty_puts(" address: ");
        boot_tty_putw((unsigned)_ptabs[region_id]);
        boot_tty_puts("\n");
#endif
    } 
}

///////////////////////////////////////////////////////////////////////////
// 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.
// region_id: the vspace in wich the vseg is located or the global space(-1).
///////////////////////////////////////////////////////////////////////////
void boot_vseg_map( mapping_vseg_t* vseg, unsigned int region_id ) 
{
    unsigned pages;
    unsigned vobj_id;
    unsigned cur_vaddr;
    unsigned cur_paddr;
    mapping_header_t*   header = (mapping_header_t*)&seg_mapping_base;  
    mapping_vobj_t*     vobj   = boot_get_vobj_base( header );
 
    // 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);
    }
    

    //loop on vobj:
    // + to computes the length of the current vseg
    // + Align vobjs
    // + Initialise the vobj
    cur_vaddr = vseg->vbase;
    cur_paddr = vseg->pbase;
    for(vobj_id= vseg->vobj_offset; vobj_id < (vseg->vobj_offset + vseg->vobjs); vobj_id++)
    {
        if(vobj[vobj_id].align)
        {
            cur_paddr = align_to(cur_paddr, vobj[vobj_id].align);
        }

        //set vaddr/paddr
        vobj[vobj_id].vaddr = cur_vaddr;        
        vobj[vobj_id].paddr = cur_paddr;  
      
        //set next vaddr/paddr
        cur_vaddr += vobj[vobj_id].length;
        cur_paddr += vobj[vobj_id].length; 
        initailise_vobj(&vobj[vobj_id], region_id);
    } 
    
    //set the length
    vseg->length = align_to((cur_paddr - vseg->pbase), 12);

    // computes number of pages
    pages = vseg->length >> 12;
    if ( (vseg->length & 0xFFF) != 0 ) pages++;

    // set the next free physical address
    if ( vseg->ident != 0 )
            ;            // nothing to do
    else                                
        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 
/////////////////////////////////////////////////////////////////////
void boot_check_mapping()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_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();
    }

    // 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.
/////////////////////////////////////////////////////////////////////
void boot_pt_init()
{
    mapping_header_t*   header = (mapping_header_t*)&seg_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

#if BOOT_DEBUG_PT
boot_tty_puts("\n******* mapping global vsegs ********");
#endif
            
    // physical page allocators must be initialised ???
    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], ((unsigned int)(-1)) );
    }

    // loop on virtual vspaces 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], vspace_id ); 
        }
    } 

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



////////////////////////////////////////////////////////////////////////////////////
// boot_init()
// This function is executed by one single processor to initialize the page
// tables, the tasks contexts and the peripherals, for all applications.
////////////////////////////////////////////////////////////////////////////////////
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");

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