1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#pragma once 8 9#include <config.h> 10#include <object/structures.h> 11#include <arch/types.h> 12#include <model/statedata.h> 13 14extern pml4e_t x64KSKernelPML4[BIT(PML4_INDEX_BITS)] VISIBLE; 15extern pdpte_t x64KSKernelPDPT[BIT(PDPT_INDEX_BITS)]; 16#ifdef CONFIG_HUGE_PAGE 17extern pde_t x64KSKernelPD[BIT(PD_INDEX_BITS)]; 18#else 19extern pde_t x64KSKernelPDs[BIT(PDPT_INDEX_BITS)][BIT(PD_INDEX_BITS)]; 20#endif 21extern pte_t x64KSKernelPT[BIT(PT_INDEX_BITS)]; 22 23#ifdef CONFIG_KERNEL_SKIM_WINDOW 24extern pml4e_t x64KSSKIMPML4[BIT(PML4_INDEX_BITS)] ALIGN(BIT(seL4_PML4Bits)); 25extern pdpte_t x64KSSKIMPDPT[BIT(PDPT_INDEX_BITS)] ALIGN(BIT(seL4_PDPTBits)); 26/* we only need a single PD regardless of huge pages or not as the skim window 27 just has a few 2M entries out of the 1gb region of the kernel image */ 28extern pde_t x64KSSKIMPD[BIT(PD_INDEX_BITS)] ALIGN(BIT(seL4_PageDirBits)); 29#endif 30 31NODE_STATE_BEGIN(modeNodeState) 32#ifdef CONFIG_KERNEL_SKIM_WINDOW 33/* we declare this as a word_t and not a cr3_t as we cache both state and potentially 34 * command information (state being pml4 base and pcid) and command being whether or not 35 * to flush translation. the formal cr3_t type only talks about the state */ 36NODE_STATE_DECLARE(word_t, x64KSCurrentUserCR3); 37#else 38NODE_STATE_DECLARE(cr3_t, x64KSCurrentCR3); 39#endif 40NODE_STATE_END(modeNodeState); 41 42/* hardware interrupt handlers push up to 6 words onto the stack. The order of the 43 words is Error, RIP, CS, FLAGS, RSP, SS. It also needs to be 16byte aligned for 44 the hardware to push correctly. For better SMP performance we add 2 words to the 45 array (such that each array is 64 bytes) and align to 64 bytes as well (which is 46 the typical L1 cache line size). Note that we do not align to the L1_CACHE_LINE_SZ 47 macro as that *could* be configured to be less than 16, which would be incorrect 48 for us here */ 49#define IRQ_STACK_SIZE 6 50extern word_t x64KSIRQStack[CONFIG_MAX_NUM_NODES][IRQ_STACK_SIZE + 2] ALIGN(64) VISIBLE SKIM_BSS; 51 52