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