1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#include <config.h> 12#include <mode/model/statedata.h> 13 14/* Current active page directory. This is really just a shadow of CR3 */ 15UP_STATE_DEFINE(paddr_t, ia32KSCurrentPD VISIBLE); 16 17/* The privileged kernel mapping PD & PT */ 18pde_t ia32KSGlobalPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits)); 19pte_t ia32KSGlobalPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits)); 20 21#ifdef CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER 22pte_t ia32KSGlobalLogPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits)); 23#endif /* CONFIG_BENCHMARK_USE_KERNEL_LOG_BUFFER */ 24