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