/*
 * hal_gpt.c - implementation of the Generic Page Table API for TSAR-MIPS32
 *
 * Author   Alain Greiner (2016)
 *
 * Copyright (c) UPMC Sorbonne Universites
 *
 * This file is part of ALMOS-MKH.
 *
 * ALMOS-MKH.is free software; you can redistribute it and/or modify it
 * under the terms of the GNU General Public License as published by
 * the Free Software Foundation; version 2.0 of the License.
 *
 * ALMOS-MKH.is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with ALMOS-MKH.; if not, write to the Free Software Foundation,
 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
 */

#include <hal_types.h>
#include <hal_gpt.h>
#include <hal_special.h>
#include <printk.h>
#include <bits.h>
#include <process.h>
#include <kmem.h>
#include <thread.h>
#include <cluster.h>
#include <ppm.h>
#include <page.h>

////////////////////////////////////////////////////////////////////////////////////////
// This define the masks for the TSAR MMU PTE attributes. (from TSAR MMU specification)
// the GPT masks are derived from the TSAR MMU PTE attributes
// in the TSAR specific hal_gpt_create() function. 
////////////////////////////////////////////////////////////////////////////////////////

#define TSAR_MMU_PRESENT        0x80000000 
#define TSAR_MMU_PTD1           0x40000000 
#define TSAR_MMU_LOCAL          0x20000000 
#define TSAR_MMU_REMOTE         0x10000000 
#define TSAR_MMU_CACHABLE       0x08000000 
#define TSAR_MMU_WRITABLE       0x04000000 
#define TSAR_MMU_EXECUTABLE     0x02000000 
#define TSAR_MMU_USER           0x01000000 
#define TSAR_MMU_GLOBAL         0x00800000 
#define TSAR_MMU_DIRTY          0x00400000 

#define TSAR_MMU_COW            0x00000001
#define TSAR_MMU_SWAP           0x00000004
#define TSAR_MMU_LOCKED         0x00000008

////////////////////////////////////////////////////////////////////////////////////////
//       TSAR MMU related macros  (from the TSAR MMU specification)
// - IX1  on 11 bits
// - IX2  on  9 bits
// - PPN  on 28 bits
////////////////////////////////////////////////////////////////////////////////////////

#define TSAR_MMU_IX1_WIDTH                 11
#define TSAR_MMU_IX2_WIDTH                 9
#define TSAR_MMU_PPN_WIDTH                 28

#define TSAR_MMU_IX1_FROM_VPN( vpn )       ((vpn >> 9) & 0x7FF)
#define TSAR_MMU_IX2_FROM_VPN( vpn )       (vpn & 0x1FF)

#define TSAR_MMU_PTBA_FROM_PTE1( pte1 )    (pte1 & 0xFFFFFFF)
#define TSAR_MMU_PPN_FROM_PTE1( pte1 )     ((pte1 & 0x7FFFF)<<9) 
#define TSAR_MMU_ATTR_FROM_PTE1( pte1 )    (pte1 & 0xFFC00000)

#define TSAR_MMU_PPN_FROM_PTE2( pte2 )     (pte2 & 0x0FFFFFFF) 
#define TSAR_MMU_ATTR_FROM_PTE2( pte2 )    (pte2 & 0xFFC000FF)

/****************************************************************************************
 * These global variables defines the masks for the Generic Page Table Entry attributes,
 * and must be defined in all GPT implementation.
 ***************************************************************************************/

uint32_t  GPT_MAPPED;
uint32_t  GPT_SMALL;
uint32_t  GPT_READABLE;
uint32_t  GPT_WRITABLE;  
uint32_t  GPT_EXECUTABLE;
uint32_t  GPT_CACHABLE; 
uint32_t  GPT_USER;  
uint32_t  GPT_DIRTY;
uint32_t  GPT_ACCESSED;
uint32_t  GPT_GLOBAL;
uint32_t  GPT_COW;
uint32_t  GPT_SWAP;
uint32_t  GPT_LOCKED;

/////////////////////////////////////
error_t hal_gpt_create( gpt_t * gpt )
{
	page_t   * page;

    // check page size
    if( CONFIG_PPM_PAGE_SIZE != 4096 )
    {
        printk("\n[PANIC] in %s : For TSAR, the page must be 4 Kbytes\n", __FUNCTION__ );
        hal_core_sleep();
    }

    // allocates 2 physical pages for PT1
	kmem_req_t req;
	req.type  = KMEM_PAGE;
	req.size  = 1;                     // 2 small pages 
	req.flags = AF_KERNEL | AF_ZERO;
	page = (page_t *)kmem_alloc( &req );

	if( page == NULL )
    {
		printk("\n[ERROR] in %s : cannot allocate physical memory for PT1\n", __FUNCTION__ );
        return ENOMEM;
	}

    // initialize generic page table descriptor
	gpt->ptr  = ppm_page2vaddr( page );
	gpt->ppn  = ppm_page2ppn( page );
	gpt->page = page;

    // initialize PTE entries attributes masks
    GPT_MAPPED     = TSAR_MMU_PRESENT;
    GPT_SMALL      = TSAR_MMU_PTD1;
    GPT_READABLE   = TSAR_MMU_PRESENT;
    GPT_WRITABLE   = TSAR_MMU_WRITABLE;
    GPT_EXECUTABLE = TSAR_MMU_EXECUTABLE;
    GPT_CACHABLE   = TSAR_MMU_CACHABLE;
    GPT_USER       = TSAR_MMU_USER;     
    GPT_DIRTY      = TSAR_MMU_DIRTY;    
    GPT_ACCESSED   = TSAR_MMU_LOCAL | TSAR_MMU_REMOTE;
    GPT_GLOBAL     = TSAR_MMU_GLOBAL; 
    GPT_COW        = TSAR_MMU_COW;
    GPT_SWAP       = TSAR_MMU_SWAP;
    GPT_LOCKED     = TSAR_MMU_LOCKED;

	return 0;
} // end hal_gpt_create()


///////////////////////////////////
void hal_gpt_destroy( gpt_t * gpt )
{
	uint32_t     ix1;
	uint32_t     ix2;
	uint32_t   * pt1;
    uint32_t     pte1;
    ppn_t        pt2_ppn;
    uint32_t   * pt2;
    uint32_t     attr;
    vpn_t        vpn;      
	kmem_req_t   req;
    bool_t       is_ref;

    // get pointer on calling process
    process_t  * process = CURRENT_THREAD->process;

    // compute is_ref 
    is_ref = ( GET_CXY( process->ref_xp ) == local_cxy );

    // get pointer on PT1
    pt1 = (uint32_t *)gpt->ptr;

    // scan the PT1
	for( ix1 = 0 ; ix1 < 2048 ; ix1++ )
	{
        pte1 = pt1[ix1];
		if( (pte1 & GPT_MAPPED) != 0 )  // PTE1 valid
        {
            if( (pte1 & GPT_SMALL) == 0 )   // BIG page
            {
                if( (pte1 & GPT_USER) != 0 ) 
                {
                    // warning message
                    printk("\n[WARNING] in %s : found an USER BIG page / ix1 = %d\n", 
                           __FUNCTION__ , ix1 );

                    // release the big physical page if reference cluster
                    if( is_ref )
                    {
                        vpn = (vpn_t)(ix1 << TSAR_MMU_IX2_WIDTH);
                        hal_gpt_reset_pte( gpt , vpn );
                    }
                }
            }
            else                           // SMALL page
            {
                // get pointer on PT2
                pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );
                pt2 = ppm_ppn2vaddr( pt2_ppn );

                // scan the PT2 to release all entries VALID and USER if reference cluster
	            if( is_ref )
                {
                    for( ix2 = 0 ; ix2 < 512 ; ix2++ )
                    {
                        attr = TSAR_MMU_ATTR_FROM_PTE2( pt2[2 * ix2] );
		                if( ((attr & GPT_MAPPED) != 0 ) && ((attr & GPT_USER) != 0) )  
                        {
                            // release the physical page
                            vpn = (vpn_t)((ix1 << TSAR_MMU_IX2_WIDTH) | ix2);
                            hal_gpt_reset_pte( gpt , vpn );
                        }
                    }
                }

                // release the PT2
                req.type = KMEM_PAGE;
                req.ptr  = ppm_vaddr2page( pt2 );
                kmem_free( &req );
            }
        }
	}

    // release the PT1
    req.type = KMEM_PAGE;
    req.ptr  = ppm_vaddr2page( pt1 );
    kmem_free( &req );

} // end hal_gpt_destroy()

/////////////////////////////////
void hal_gpt_print( gpt_t * gpt )
{
	uint32_t   ix1;
	uint32_t   ix2;
	uint32_t * pt1;
    uint32_t   pte1;
    ppn_t      pt2_ppn;
    uint32_t * pt2;
    uint32_t   pte2_attr;
    ppn_t      pte2_ppn;

    printk("*** Page Table for process %x in cluster %x ***\n",
           CURRENT_THREAD->process->pid , local_cxy );

    pt1 = (uint32_t *)gpt->ptr;

    // scan the PT1
	for( ix1 = 0 ; ix1 < 2048 ; ix1++ )
	{
        pte1 = pt1[ix1];
		if( (pte1 & GPT_MAPPED) != 0 )
        {
            if( (pte1 & GPT_SMALL) == 0 )  // BIG page
            {
                printk(" - BIG   : pt1[%d] = %x\n", ix1 , pte1 );
            }
            else                           // SMALL pages
            {
                pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );
                pt2 = ppm_ppn2vaddr( pt2_ppn );

                // scan the PT2
	            for( ix2 = 0 ; ix2 < 512 ; ix2++ )
                {
                    pte2_attr = TSAR_MMU_ATTR_FROM_PTE2( pt2[2 * ix2] );
                    pte2_ppn  = TSAR_MMU_PPN_FROM_PTE2( pt2[2 * ix2 + 1] );
		            if( (pte2_attr & GPT_MAPPED) != 0 )
                    {
                        printk(" - SMALL   : pt1[%d] = %x / pt2[%d] / pt2[%d]\n",
                               ix1 , pt1[ix1] , 2*ix2 , pte2_attr , 2*ix2+1 , pte2_ppn );
                    }
                }
            }
        }
	}
} // end hal_gpt_print()


///////////////////////////////////////
error_t hal_gpt_set_pte( gpt_t   * gpt,
                         vpn_t     vpn,
                         ppn_t     ppn,
                         uint32_t  attr )
{
    uint32_t          * pt1;         // virtual base addres of PT1
	volatile uint32_t * pte1_ptr;    // pointer on PT1 entry
	uint32_t            pte1;        // PT1 entry value

	ppn_t               pt2_ppn;     // PPN of PT2
	uint32_t          * pt2;         // virtual base address of PT2

	uint32_t            small;       // requested PTE is for a small page
	bool_t              atomic;      //
	page_t            * page;        // pointer on new physical page descriptor

    uint32_t            ix1;         // index in PT1
    uint32_t            ix2;         // index in PT2

    // compute indexes in PT1 and PT2
    ix1 = TSAR_MMU_IX1_FROM_VPN( vpn );
    ix2 = TSAR_MMU_IX2_FROM_VPN( vpn );

    pt1   = gpt->ptr;
	small = (attr & GPT_SMALL);

    // get PT1 entry value
	pte1_ptr  = &pt1[ix1];
	pte1      = *pte1_ptr;

    // Big pages (PTE1) are only set for the kernel vsegs, in the kernel init phase.
    // There is no risk of concurrent access.
	if( small == 0 )
	{
		if( (pte1 != 0) || (attr & GPT_COW) )
		{
			printk("\n[ERROR] in %s : set a big page in a mapped PT1 entry / PT1[%d] = %x\n",
                   __FUNCTION__ , ix1 , pte1 );
			return EINVAL;
		}
      
        // set the PTE1 
		*pte1_ptr = attr | (ppn >> 9);
		hal_fence();
		return 0;
	}

    // From this point, the requested PTE is a PTE2 (small page)

	if( (pte1 & GPT_MAPPED) == 0 )      // the PT1 entry is not valid
	{
        // allocate one physical page for the PT2
	    kmem_req_t req;
	    req.type  = KMEM_PAGE;
	    req.size  = 0;                     // 1 small page 
	    req.flags = AF_KERNEL | AF_ZERO;
	    page = (page_t *)kmem_alloc( &req );
        if( page == NULL )
        {
			printk("\n[ERROR] in %s : try to set a small page but cannot allocate PT2\n",
                    __FUNCTION__ );
            return ENOMEM;
        }
        pt2_ppn = ppm_page2ppn( page );
        pt2     = ppm_page2vaddr( page );

        // try to atomicaly set a PTD1 in the PT1 entry 
		do 
		{
		    atomic = hal_atomic_cas( (void*)pte1, 0 , 
                                      TSAR_MMU_PRESENT | TSAR_MMU_PTD1 | pt2_ppn );
        } 
        while( (atomic == false) && (*pte1_ptr == 0) );

	    if( atomic == false ) // the mapping has been done by another thread !!!
        {
            // release the allocated page
	        ppm_free_pages( page );

            // read PT1 entry again 
			pte1 = *pte1_ptr;

            // compute PPN of PT2 base
			pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );

            // compute pointer on PT2 base
			pt2 = (uint32_t*)ppm_ppn2vaddr( pt2_ppn );
		}
	}
	else                             // The PT1 entry is valid  
	{
        // This valid entry must be a PTD1
        if( (pte1 & GPT_SMALL) == 0 )
        {
			printk("\n[ERROR] in %s : set a small page in a big PT1 entry / PT1[%d] = %x\n",
                    __FUNCTION__ , ix1 , pte1 );
            return EINVAL;
        }

        // compute PPN of PT2 base
		pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );

        // compute pointer on PT2 base
	    pt2 = (uint32_t*)ppm_ppn2vaddr( pt2_ppn );
	}

    // set PTE2 in this order
	pt2[2 * ix2 + 1] = ppn;
	hal_fence();
	pt2[2 * ix2]     = attr;
	hal_fence();

	return 0;
} // end of hal_gpt_set_pte()

/////////////////////////////////////
void hal_gpt_get_pte( gpt_t    * gpt,
                      vpn_t      vpn,
                      uint32_t * attr,
                      ppn_t    * ppn )
{
    uint32_t * pt1;
    uint32_t   pte1;

    uint32_t * pt2;
    ppn_t      pt2_ppn;

    uint32_t   ix1 = TSAR_MMU_IX1_FROM_VPN( vpn );
    uint32_t   ix2 = TSAR_MMU_IX2_FROM_VPN( vpn );

    // get PTE1 value
	pt1  = gpt->ptr;
    pte1 = pt1[ix1];

	if( (pte1 & GPT_MAPPED) == 0 )   // PT1 entry not present
	{
		*attr = 0;
		*ppn  = 0;
	}

	if( (pte1 & GPT_SMALL) == 0 )     // it's a PTE1
	{
		*attr = TSAR_MMU_ATTR_FROM_PTE1( pte1 );
        *ppn  = TSAR_MMU_PPN_FROM_PTE1( pte1 ) | (vpn & ((1<<TSAR_MMU_IX2_WIDTH)-1));
	}
    else                              // it's a PTD1
    {
        // compute PT2 base address
        pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );
        pt2     = (uint32_t*)ppm_ppn2vaddr( pt2_ppn );

	    *ppn  = pt2[2*ix2+1] & ((1<<TSAR_MMU_PPN_WIDTH)-1);
	    *attr = pt2[2*ix2];
    }
} // end hal_gpt_get_pte()

////////////////////////////////////
void hal_gpt_reset_pte( gpt_t * gpt,
                        vpn_t   vpn )
{
    uint32_t * pt1;         // PT1 base address
    uint32_t   pte1;        // PT1 entry value

    ppn_t      pt2_ppn;     // PPN of PT2 
    uint32_t * pt2;         // PT2 base address

    ppn_t      ppn;         // PPN of page to be released

    kmem_req_t req;

    uint32_t   ix1 = TSAR_MMU_IX1_FROM_VPN( vpn );
    uint32_t   ix2 = TSAR_MMU_IX2_FROM_VPN( vpn );

    // get PTE1 value 
	pt1      = gpt->ptr;
    pte1     = pt1[ix1];

	if( (pte1 & GPT_MAPPED) == 0 )   // PT1 entry not present
	{
		return;
	}

	if( (pte1 & GPT_SMALL) == 0 )     // it's a PTE1
	{
        // get PPN 
        ppn = TSAR_MMU_PPN_FROM_PTE1( pte1 );

        // unmap the big page
        pt1[ix1] = 0;
	    hal_fence();

        // releases the big page
        req.type  = KMEM_PAGE;
	    req.size  = 9;
        req.ptr   = (void*)(ppn << CONFIG_PPM_PAGE_SHIFT);
	    kmem_free( &req );

        return;
	}
    else                              // it's a PTD1
    {
        // compute PT2 base address
        pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );
        pt2 = (uint32_t*)ppm_ppn2vaddr( pt2_ppn );
        
        // get PPN
	    ppn = TSAR_MMU_PPN_FROM_PTE2( pt2[2*ix2+1] );

        // unmap the small page
	    pt2[2*ix2]   = 0;
	    hal_fence();
	    pt2[2*ix2+1] = 0;
	    hal_fence();

        // releases the small page
        req.type  = KMEM_PAGE;
	    req.size  = 0;
        req.ptr   = (void*)(ppn << CONFIG_PPM_PAGE_SHIFT);
	    kmem_free( &req );

        return;
    }
}  // end hal_gpt_reset_pte()

//////////////////////////////////////
error_t hal_gpt_lock_pte( gpt_t * gpt,
                          vpn_t   vpn )
{
    uint32_t          * pt1;             // PT1 base address
	volatile uint32_t * pte1_ptr;        // address of PT1 entry
	uint32_t            pte1;            // value of PT1 entry

    uint32_t          * pt2;             // PT2 base address
	ppn_t               pt2_ppn;         // PPN of PT2 page if missing PT2
	volatile uint32_t * pte2_ptr;        // address of PT2 entry

	uint32_t            attr;
	bool_t              atomic;
    page_t            * page;

    uint32_t  ix1 = TSAR_MMU_IX1_FROM_VPN( vpn );    // index in PT1
    uint32_t  ix2 = TSAR_MMU_IX2_FROM_VPN( vpn );    // index in PT2

    // get the PTE1 value
    pt1       = gpt->ptr; 
	pte1_ptr  = &pt1[ix1];
	pte1      = *pte1_ptr;

    // If present, the page must be small
	if( ((pte1 & GPT_MAPPED) != 0) && ((pte1 & GPT_SMALL) == 0) )
    {
        printk("\n[ERROR] in %s : try to lock a big page / PT1[%d] = %x\n",
               __FUNCTION__ , ix1 , pte1 );
		return EINVAL;
    }

	if( (pte1 & GPT_MAPPED) == 0 )  // missing PT1 entry   
	{
        // allocate one physical page for PT2
	    kmem_req_t req;
	    req.type  = KMEM_PAGE;
	    req.size  = 0;                     // 1 small page 
	    req.flags = AF_KERNEL | AF_ZERO;
	    page = (page_t *)kmem_alloc( &req );

        if( page == NULL )
        {
			printk("\n[ERROR] in %s : try to set a small page but cannot allocate PT2\n",
                      __FUNCTION__ );
            return ENOMEM;
        }

        pt2_ppn = ppm_page2ppn( page );
        pt2     = ppm_page2vaddr( page );

        // try to set the PT1 entry
		do 
		{
			atomic = hal_atomic_cas( (void*)pte1_ptr , 0 , 
                                     TSAR_MMU_PRESENT | TSAR_MMU_PTD1 | pt2_ppn );
		} 
        while( (atomic == false) && (*pte1_ptr == 0) );

		if( atomic == false )  // missing PT2 has been allocate by another core
		{
            // release the allocated page
			ppm_free_pages( page );

            // read again the PTE1	
			pte1 = *pte1_ptr;

            // get the PT2 base address
			pt2_ppn = TSAR_MMU_PPN_FROM_PTE1( pte1 );
 			pt2     = (uint32_t*)ppm_ppn2vaddr( pt2_ppn );
		}
	}
    else
    {
        // This valid entry must be a PTD1
        if( (pte1 & GPT_SMALL) == 0 )
        {
			printk("\n[ERROR] in %s : set a small page in a big PT1 entry / PT1[%d] = %x\n",
                    __FUNCTION__ , ix1 , pte1 );
            return EINVAL;
        }

        // compute PPN of PT2 base
		pt2_ppn = TSAR_MMU_PTBA_FROM_PTE1( pte1 );

        // compute pointer on PT2 base
	    pt2 = (uint32_t*)ppm_ppn2vaddr( pt2_ppn );
    }
    
    // from here we have the PT2 pointer
    
    // compute pointer on PTE2
    pte2_ptr = &pt2[2 * ix2];

    // try to atomically lock the PTE2 until success
	do
    {
        // busy waiting until GPT_LOCK == 0
        do
		{
			attr = *pte2_ptr;
			hal_rdbar();
		}
        while( (attr & GPT_LOCKED) != 0 );

        // try to set the GPT_LOCK wit a CAS
		atomic = hal_atomic_cas( (void*)pte2_ptr, attr , (attr | GPT_LOCKED) );
	}
    while( atomic == 0 );

	return 0;
}  // end hal_gpt_lock_pte()

////////////////////////////////////////
error_t hal_gpt_unlock_pte( gpt_t * gpt,
                            vpn_t   vpn )
{
    uint32_t * pt1;             // PT1 base address
	uint32_t   pte1;            // value of PT1 entry

    uint32_t * pt2;             // PT2 base address
	ppn_t      pt2_ppn;         // PPN of PT2 page if missing PT2
	uint32_t * pte2_ptr;        // address of PT2 entry

	uint32_t   attr;            // PTE2 attribute

    // compute indexes in P1 and PT2
    uint32_t  ix1 = TSAR_MMU_IX1_FROM_VPN( vpn );    // index in PT1
    uint32_t  ix2 = TSAR_MMU_IX2_FROM_VPN( vpn );    // index in PT2

    // get pointer on PT1 base
    pt1  = (uint32_t*)gpt->ptr;

    // get PTE1
    pte1 = pt1[ix1];

    // check PTE1 present and small page
    if( ((pte1 & GPT_MAPPED) == 0) || ((pte1 & GPT_SMALL) == 0) )
    {
        printk("\n[ERROR] in %s : try to unlock a big or undefined page / PT1[%d] = %x\n",
                 __FUNCTION__ , ix1 , pte1 );
        return EINVAL;
    }

    // get pointer on PT2 base
    pt2_ppn = TSAR_MMU_PPN_FROM_PTE1( pte1 );
    pt2     = ppm_ppn2vaddr( pt2_ppn );
 
    // get pointer on PTE2
	pte2_ptr = &pt2[2 * ix2];

    // get PTE2_ATTR
	attr = *pte2_ptr;

    // check PTE2 present and locked
    if( ((attr & GPT_MAPPED) == 0) || ((attr & GPT_LOCKED) == 0) );
    {
        printk("\n[ERROR] in %s : try to unlock an undefined page / PT1[%d] = %x\n",
                 __FUNCTION__ , ix1 , pte1 );
        return EINVAL;
    }

    // reset GPT_LOCK
	*pte2_ptr = attr & !GPT_LOCKED;

	return 0;
}  // end hal_gpt_unlock_pte()

///////////////////////////////////////
error_t hal_gpt_copy( gpt_t  * dst_gpt,
                      gpt_t  * src_gpt,
                      bool_t   cow )
{
    uint32_t     ix1;       // index in PT1
    uint32_t     ix2;       // index in PT2

	uint32_t   * src_pt1;   // local pointer on PT1 for SRC_GPT 
	uint32_t   * dst_pt1;   // local pointer on PT1 for DST_GPT
    uint32_t   * dst_pt2;   // local pointer on PT2 for DST_GPT
    uint32_t   * src_pt2;   // local pointer on PT2 for SRC_GPT

    uint32_t     pte1;
    uint32_t     pte2_attr;
    uint32_t     pte2_ppn;
    uint32_t     pte2_writable;

    page_t     * page;

    ppn_t        src_pt2_ppn;
    ppn_t        dst_pt2_ppn;

    // get pointers on PT1 for src_gpt & dst_gpt
    src_pt1 = (uint32_t *)src_gpt->ptr;
    dst_pt1 = (uint32_t *)dst_gpt->ptr;

    // scan the SRC_PT1
	for( ix1 = 0 ; ix1 < 2048 ; ix1++ )
	{
        pte1 = src_pt1[ix1];
		if( (pte1 & GPT_MAPPED) != 0 )
        {
            if( (pte1 & GPT_SMALL) == 0 )  // PTE1 => big kernel page
            {
                // big kernel pages are shared by all processes => copy it
                dst_pt1[ix1] = pte1;
            }
            else                           // PTD1 => smal pages
            {
                // allocate one physical page for a PT2 in DST_GPT
	            kmem_req_t req;
	            req.type  = KMEM_PAGE;
	            req.size  = 0;                     // 1 small page 
	            req.flags = AF_KERNEL | AF_ZERO;
	            page = (page_t *)kmem_alloc( &req );

                if( page == NULL )
                {
                    // TODO release all memory allocated to DST_GPT
			        printk("\n[ERROR] in %s : cannot allocate PT2\n", __FUNCTION__ );
                    return ENOMEM;
                }

                // get pointer on new PT2 in DST_GPT
                dst_pt2 = (uint32_t *)ppm_page2vaddr( page );

                // set a new PTD1 in DST_GPT
                dst_pt2_ppn  = (ppn_t)ppm_page2ppn( page );
                dst_pt1[ix1] = TSAR_MMU_PRESENT | TSAR_MMU_PTD1 | dst_pt2_ppn;

                // get pointer on PT2 in SRC_GPT
                src_pt2_ppn = (ppn_t)TSAR_MMU_PTBA_FROM_PTE1( pte1 );
                src_pt2     = (uint32_t *)ppm_ppn2vaddr( src_pt2_ppn );

                // scan the SRC_PT2
                for( ix2 = 0 ; ix2 < 512 ; ix2++ )
                {
                    // get attr & ppn from PTE2
                    pte2_attr = TSAR_MMU_ATTR_FROM_PTE2( src_pt2[2 * ix2] );

		            if( (pte2_attr & GPT_MAPPED) != 0 )  // valid PTE2 in SRC_GPT
                    {
                        // get GPT_WRITABLE & PPN
                        pte2_writable = pte2_attr & GPT_WRITABLE;
                        pte2_ppn      = TSAR_MMU_PPN_FROM_PTE2(  src_pt2[2 * ix2 + 1] );

                        // set a new PTE2 in DST_GPT
                        dst_pt2[2*ix2]     = pte2_attr;
                        dst_pt2[2*ix2 + 1] = pte2_ppn;
                        
                        // handle Copy-On-Write
                        if( cow && pte2_writable )
                        {
                            // reset GPT_WRITABLE in both SRC_GPT and DST_GPT
                            hal_atomic_and( &dst_pt2[2*ix2] , ~GPT_WRITABLE );
                            hal_atomic_and( &src_pt2[2*ix2] , ~GPT_WRITABLE );

                            // register PG_COW in page descriptor
                            page = ppm_ppn2page( pte2_ppn );
                            hal_atomic_or( &page->flags , PG_COW );
							hal_atomic_add( &page->fork_nr , 1 );
                        }
                    }
                }  // end loop on ix2
            } 
        }
    }  // end loop ix1

    hal_fence();

    return 0;

}  // end hal_gpt_copy()

