1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#include <config.h> 8#include <mode/model/statedata.h> 9 10/* Current active page directory. This is really just a shadow of CR3 */ 11UP_STATE_DEFINE(paddr_t, ia32KSCurrentPD VISIBLE); 12 13/* The privileged kernel mapping PD & PT */ 14pde_t ia32KSGlobalPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits)); 15pte_t ia32KSGlobalPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits)); 16 17#ifdef CONFIG_KERNEL_LOG_BUFFER 18pte_t ia32KSGlobalLogPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits)); 19#endif /* CONFIG_KERNEL_LOG_BUFFER */ 20