1/* 2 * Copyright 2020, DornerWorks 3 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 4 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com> 5 * 6 * SPDX-License-Identifier: GPL-2.0-only 7 */ 8 9#include <util.h> 10#include <api/types.h> 11#include <arch/types.h> 12#include <arch/model/statedata.h> 13#include <arch/object/structures.h> 14#include <linker.h> 15#include <plat/machine/hardware.h> 16 17/* The top level asid mapping table */ 18asid_pool_t *riscvKSASIDTable[BIT(asidHighBits)]; 19 20/* Kernel Page Tables */ 21pte_t kernel_root_pageTable[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits)); 22 23#if __riscv_xlen != 32 24pte_t kernel_image_level2_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits)); 25pte_t kernel_image_level2_dev_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits)); 26#elif defined(CONFIG_KERNEL_LOG_BUFFER) 27pte_t kernel_image_level2_log_buffer_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits)); 28#endif 29 30SMP_STATE_DEFINE(core_map_t, coreMap); 31