//////////////////////////////////////////////////////////////////////////////////
// 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 is executed in the boot phase by proc0 to build  all the pages tables,
// then jump in the seg_kernel_init segment with an activated MMU. 
//
// The SoCLib generic MMU (paged virtual memory) provides 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.
//
// The boot code uses the MAPPING_INFO binary data structures, that must be pre-loaded 
// in the 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 by the (GIET_NB_PT2_MAX) configuration parameter.
// 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, and
// contains one PT1 and (GIET_NB_PT2_MAX) PT2s. The PT1 is addressed using the ix1 field
// (11 bits) of the VPN, and the selected PT2 is addressed using the ix2 field (9 bits).
// - PT1[2048] : a first 8K aligned array of unsigned int, indexed by the (ix1) field of VPN. 
//   Each entry in the PT1 contains a 32 bits PTD. The MSB bit PTD[31] is 
//   the PTD valid bit, and LSB bits PTD[19:0] are the 20 MSB bits of the physical base
//   address of the selected PT2.
//   The PT1 contains 2048 PTD of 4 bytes => 8K bytes.
// - PT2[1024][GIET_NB_PT2_MAX] : an array of array of unsigned int. 
//   Each PT2[1024] must be 4K aligned,  and each entry in a PT2 contains two unsigned int: 
//   the first word contains the protection flags, and the second word contains the PPN.
//   Each PT2 contains 512 PTE2 of 8bytes => 4K bytes.
// The total size of a page table is finally = 8K + (GIET_NB_PT2_MAX)*4K bytes.
////////////////////////////////////////////////////////////////////////////////////

#include "../sys/mips32_registers.h"
#include <boot_handler.h>
#include <giet_config.h>
#include <mapping_info.h>
#include <mwmr_channel.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

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

////////////////////////////////////////////////////////////////////////////
//  Page Tables global variables
////////////////////////////////////////////////////////////////////////////

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

// Page table pointers array
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_puts()
// (it uses TTY0)
////////////////////////////////////////////////////////////////////////////
void boot_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_putw() 
// (it uses TTY0)
////////////////////////////////////////////////////////////////////////////
void boot_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_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_puts("mapping_info");

    boot_puts("\n - signature = ");
    boot_putw(header->signature);
    boot_puts("\n - name      = ");
    boot_puts(header->name);
    boot_puts("\n - clusters  = ");
    boot_putw(header->clusters);
    boot_puts("\n - psegs     = ");
    boot_putw(header->psegs);
    boot_puts("\n - ttys      = ");
    boot_putw(header->ttys);
    boot_puts("\n - fbs       = ");
    boot_putw(header->fbs);
    boot_puts("\n - vspaces   = ");
    boot_putw(header->vspaces);
    boot_puts("\n - globals   = ");
    boot_putw(header->globals);
    boot_puts("\n - vsegs     = ");
    boot_putw(header->vsegs);
    boot_puts("\n - vobjs     = ");
    boot_putw(header->vobjs);
    boot_puts("\n - tasks     = ");
    boot_putw(header->tasks);
    boot_puts("\n\n");

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

        boot_puts("\n - procs  = ");
        boot_putw(cluster[cluster_id].procs);
        boot_puts("\n\n");
    }

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

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

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

        boot_puts("\n - name        = ");
        boot_puts( vseg[vseg_id].name );
        boot_puts("\n - vbase       = ");
        boot_putw( vseg[vseg_id].vbase );
        boot_puts("\n - length      = ");
        boot_putw( vseg[vseg_id].length );
        boot_puts("\n - mode        = ");
        boot_putw( vseg[vseg_id].mode );
        boot_puts("\n - ident       = ");
        boot_putw( vseg[vseg_id].ident );
        boot_puts("\n - psegname    = ");
        boot_puts( pseg[vseg[vseg_id].psegid].name );
        boot_puts("\n - vobjs       = ");
        boot_putw( vseg[vseg_id].vobjs );
        boot_puts("\n - vobj_offset = ");
        boot_putw( vseg[vseg_id].vobj_offset );
        boot_puts("\n");
        for ( vobj_id = vseg[vseg_id].vobj_offset ; 
              vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; 
              vobj_id++ )
        {
			boot_puts("\n\t vobj ");
            boot_puts( vobj[vobj_id].name);
            boot_puts("\n\t type     = ");
			boot_putw( vobj[vobj_id].type);
            boot_puts("\n\t length   = ");
			boot_putw(   vobj[vobj_id].length);
            boot_puts("\n\t align    = ");
			boot_putw(   vobj[vobj_id].align);
            boot_puts("\n\t binpath  = ");
			boot_puts(   vobj[vobj_id].binpath);
			boot_puts("\n\n");
        }
    }

    // vspaces
    for ( vspace_id = 0 ; vspace_id < header->vspaces ; vspace_id++ )
    {
        unsigned int start_id = vspace[vspace_id].vobj_offset + 
                                vspace[vspace_id].start_offset; 

        boot_puts("vspace ");
        boot_putw(vspace_id);

        boot_puts("\n - name        = ");
        boot_puts( vspace[vspace_id].name ); 
        boot_puts("\n - start_vobj  = ");
        boot_puts( vobj[start_id].name ); 
        boot_puts("\n - vsegs       = ");
        boot_putw( vspace[vspace_id].vsegs ); 
        boot_puts("\n - vobjs       = ");
        boot_putw( vspace[vspace_id].vobjs ); 
        boot_puts("\n - tasks       = ");
        boot_putw( vspace[vspace_id].tasks ); 
        boot_puts("\n - vseg_offset = ");
        boot_putw( vspace[vspace_id].vseg_offset ); 
        boot_puts("\n - vobj_offset = ");
        boot_putw( vspace[vspace_id].vobj_offset ); 
        boot_puts("\n - task_offset = ");
        boot_putw( vspace[vspace_id].task_offset ); 
        boot_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_puts("    private vseg ");
            boot_putw( vseg_id );

            boot_puts("\n    - name        = ");
            boot_puts( vseg[vseg_id].name );
            boot_puts("\n    - vbase       = ");
            boot_putw( vseg[vseg_id].vbase );
            boot_puts("\n    - length      = ");
            boot_putw( vseg[vseg_id].length );
            boot_puts("\n    - mode        = ");
            boot_putw( vseg[vseg_id].mode );
            boot_puts("\n    - ident       = ");
            boot_putw( vseg[vseg_id].ident );
            boot_puts("\n    - psegname    = ");
            boot_puts( pseg[vseg[vseg_id].psegid].name );
            boot_puts("\n    - vobjs       = ");
            boot_putw( vseg[vseg_id].vobjs );
            boot_puts("\n    - vobj_offset = ");
            boot_putw( vseg[vseg_id].vobj_offset );
            boot_puts("\n");

            for ( vobj_id = vseg[vseg_id].vobj_offset ; 
                  vobj_id < vseg[vseg_id].vobj_offset + vseg[vseg_id].vobjs ; 
                  vobj_id++ )
            {
                boot_puts("\n\t\t vobj ");
                boot_puts( vobj[vobj_id].name);
                boot_puts("\n\t\t type     = ");
                boot_putw( vobj[vobj_id].type);
                boot_puts("\n\t\t length   = ");
			    boot_putw(   vobj[vobj_id].length);
                boot_puts("\n\t\t align    = ");
			    boot_putw(   vobj[vobj_id].align);
                boot_puts("\n\t\t binpath  = ");
	    		boot_puts(   vobj[vobj_id].binpath);
    			boot_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_puts("     task");
            boot_putw( task_id );

            boot_puts("\n     - name = ");
            boot_puts( task[task_id].name );
            boot_puts("\n     - clusterid = ");
            boot_putw( task[task_id].clusterid );
            boot_puts("\n     - proclocid = ");
            boot_putw( task[task_id].proclocid );
            boot_puts("\n     - vobjlocid = ");
            boot_putw( task[task_id].vobjlocid );
            boot_puts("\n     - startid   = ");
            boot_putw( task[task_id].startid );
            boot_puts("\n     - use_tty   = ");
            boot_putw( task[task_id].use_tty );
            boot_puts("\n     - use_fb   = ");
            boot_putw( task[task_id].use_fb );
            boot_puts("\n\n");
        }
    }
} // end boot_print_mapping_info()
#endif

//////////////////////////////////////////////////////////////////////////////
// boot_pseg_get() 
// This function returns the pointer on a physical segment
// identified  by the pseg 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_puts("\n[BOOT ERROR] : seg_id argument too large\n");
        boot_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 global parameter is a boolean indicating 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 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

    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 == GIET_NB_PT2_MAX )
        {
            boot_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
            boot_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
    {
        boot_puts("\n[BOOT ERROR] in boot_add_pte() function\n");
        boot_puts("page already mapped\n");
        boot_exit();
    }

    // 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_puts("- vseg ");
boot_puts( vseg[vseg_id].name );
boot_puts(" / flags = ");
boot_putw( flags );
boot_puts(" / npages = ");
boot_putw( npages );
boot_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++;
        }
    }

    // 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_puts("- vseg ");
boot_puts( vseg[vseg_id].name );
boot_puts(" / flags = ");
boot_putw( flags );
boot_puts(" / npages = ");
boot_putw( npages );
boot_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++;
        }
    }

} // 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 int toAlign, 
                       unsigned int alignPow2)
{
    unsigned int    mask = (1 << alignPow2) - 1;
    return ((toAlign + mask ) & ~mask ); 
}

///////////////////////////////////////////////////////////////////////////
// This function compute the physical base address for a vseg
// as specified in the mapping info data structure.
// It updates the pbase and the length fields of the vseg.
// It updates the pbase and vbase fields of all vobjs in the vseg.
// It updates the next_base field of the pseg.
// It checks a possible pseg overflow.
// It is a global vseg if vspace_id = (-1) 
///////////////////////////////////////////////////////////////////////////
void boot_vseg_map( mapping_vseg_t*     vseg, 
                    unsigned int        vspace_id ) 
{
    unsigned int        vobj_id;
    unsigned int        cur_vaddr;
    unsigned int        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
    {
         vseg->pbase = vseg->vbase;
    }
    else                                // unconstrained mapping
    {
        vseg->pbase = pseg->next_base;

        // test alignment constraint
        if ( vobj[vseg->vobj_offset].align )
        {
            vseg->pbase = align_to( vseg->pbase, vobj[vseg->vobj_offset].align );
        }
    }
    
    // loop on vobjs to (1) computes the length of the vseg,
    // (2) initialise the vaddr and paddr fields of all vobjs,
    // (3) initialise the page table pointers array 

    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 for current vobj
        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; 

        // initialise _ptabs[] if current vobj is a PTAB
        if ( vobj[vobj_id].type == VOBJ_TYPE_PTAB )
        {
            if(vobj[vobj_id].length < (PT1_SIZE + PT2_SIZE*GIET_NB_PT2_MAX) ) 
            {
                boot_puts( "\n[BOOT ERROR] in boot_vseg_map() function: " );
                boot_puts("PTAB vobj is too small in vspace ");
                boot_putw(vspace_id);
                boot_puts("\n");
                boot_exit();
            }
            if(vspace_id == ((unsigned int) -1))    // global vseg
            {
                boot_puts( "\n[BOOT ERROR] in boot_vseg_map() function: " );
                boot_puts( "a PTAB vobj cannot be global" );
                boot_exit();
            }
            _ptabs[vspace_id] = (page_table_t*)vobj[vobj_id].paddr;
        }
    } // end for vobjs
    
    //set the vseg length
    vseg->length = align_to( (cur_paddr - vseg->pbase), 12);

    // checking pseg overflow
    if ( (vseg->pbase < pseg->base) || 
         ((vseg->pbase + vseg->length) > (pseg->base + pseg->length)) )
    {
        boot_puts("\n[BOOT ERROR] in boot_vseg_map() function\n");
        boot_puts("impossible mapping for virtual segment: ");
        boot_puts( vseg->name ); 
        boot_puts("\n"); 
        boot_puts("vseg pbase = ");
        boot_putw( vseg->pbase ); 
        boot_puts("\n"); 
        boot_puts("vseg length = ");
        boot_putw( vseg->length ); 
        boot_puts("\n"); 
        boot_puts("pseg pbase = ");
        boot_putw( pseg->base ); 
        boot_puts("\n"); 
        boot_puts("pseg length = ");
        boot_putw( pseg->length ); 
        boot_puts("\n"); 
        boot_exit();
    }

    // set the next_base field in vseg
    if ( vseg->ident == 0 )
        pseg->next_base = vseg->pbase + vseg->length;

#if BOOT_DEBUG_PT
boot_puts( vseg->name );
boot_puts(" : len = ");
boot_putw( vseg->length );
boot_puts(" / vbase = ");
boot_putw( vseg->vbase );
boot_puts(" / pbase = ");
boot_putw( vseg->pbase );
boot_puts("\n");
#endif  

} // end boot_vseg_map()

/////////////////////////////////////////////////////////////////////
// This function checks 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_puts("\n[BOOT ERROR] Illegal mapping signature: ");
        boot_putw(header->signature);
        boot_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_puts("\n[BOOT ERROR] Incoherent NB_CLUSTERS");
        boot_puts("\n             - In giet_config,  value = ");
        boot_putw ( NB_CLUSTERS );
        boot_puts("\n             - In mapping_info, value = ");
        boot_putw ( header->clusters );
        boot_puts("\n");
        boot_exit();
    }

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

    // number of virtual spaces no larger than GIET_NB_VSPACE_MAX
    if ( header->vspaces > GIET_NB_VSPACE_MAX )
    {
        boot_puts("\n[BOOT ERROR] : number of vspaces > GIET_NB_VSPACE_MAX\n");
        boot_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;

    // checking mapping_info
    boot_check_mapping();

    // physical page allocators must be initialised 
    for ( pseg_id = 0 ; pseg_id < header->psegs ; pseg_id++ )
    {
        pseg[pseg_id].next_base = pseg[pseg_id].base;
    }

#if BOOT_DEBUG_PT
boot_puts("\n******* mapping global vsegs ********\n");
#endif
            
    // step 1 : first loop on virtual spaces to map global vsegs
    for ( vseg_id = 0 ; vseg_id < header->globals ; vseg_id++ )
    {
        boot_vseg_map( &vseg[vseg_id], ((unsigned int)(-1)) );
    }

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

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

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

#if BOOT_DEBUG_PT
boot_puts("\n******* building page table for vspace ");
boot_puts(vspace[vspace_id].name);
boot_puts(" ********\n");
#endif
            
        boot_vspace_pt_build( vspace_id );

#if BOOT_DEBUG_PT
boot_puts("\n>>> page table physical address = ");
boot_putw((unsigned int)_ptabs[vspace_id]);
boot_puts("\n");
#endif
    } 

    boot_puts("\n[BOOT] Page Tables initialisation completed at cycle ");
    boot_putw( boot_time() );
    boot_puts("\n");

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