1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 8 * See "LICENSE_GPLv2.txt" for details. 9 * 10 * @TAG(DATA61_GPL) 11 */ 12 13#include <arch/model/statedata.h> 14 15/* The privileged kernel mapping PD & PT */ 16pml4e_t x64KSKernelPML4[BIT(PML4_INDEX_BITS)] ALIGN(BIT(seL4_PML4Bits)) VISIBLE; 17pdpte_t x64KSKernelPDPT[BIT(PDPT_INDEX_BITS)] ALIGN(BIT(seL4_PDPTBits)); 18#ifdef CONFIG_HUGE_PAGE 19pde_t x64KSKernelPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits)); 20#else 21pde_t x64KSKernelPDs[BIT(PDPT_INDEX_BITS)][BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits)); 22#endif 23pte_t x64KSKernelPT[BIT(PT_INDEX_BITS)] ALIGN(BIT(seL4_PageTableBits)); 24 25#ifdef CONFIG_KERNEL_SKIM_WINDOW 26pml4e_t x64KSSKIMPML4[BIT(PML4_INDEX_BITS)] ALIGN(BIT(seL4_PML4Bits)); 27pdpte_t x64KSSKIMPDPT[BIT(PDPT_INDEX_BITS)] ALIGN(BIT(seL4_PDPTBits)); 28pde_t x64KSSKIMPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits)); 29#endif 30 31#ifdef CONFIG_KERNEL_SKIM_WINDOW 32UP_STATE_DEFINE(word_t, x64KSCurrentUserCR3); 33#else 34UP_STATE_DEFINE(cr3_t, x64KSCurrentCR3); 35#endif 36 37word_t x64KSIRQStack[CONFIG_MAX_NUM_NODES][IRQ_STACK_SIZE + 2] ALIGN(64) VISIBLE SKIM_BSS; 38