1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #include <config.h>
8 #include <mode/model/smp.h>
9 
10 #ifdef ENABLE_SMP_SUPPORT
11 
12 nodeInfo_t node_info[CONFIG_MAX_NUM_NODES] ALIGN(L1_CACHE_LINE_SIZE) VISIBLE;
13 char nodeSkimScratch[CONFIG_MAX_NUM_NODES][sizeof(nodeInfo_t)] ALIGN(L1_CACHE_LINE_SIZE);
14 extern char kernel_stack_alloc[CONFIG_MAX_NUM_NODES][BIT(CONFIG_KERNEL_STACK_BITS)];
15 
mode_init_tls(cpu_id_t cpu_index)16 BOOT_CODE void mode_init_tls(cpu_id_t cpu_index)
17 {
18     node_info[cpu_index].stackTop = kernel_stack_alloc[cpu_index + 1];
19     node_info[cpu_index].irqStack = &x64KSIRQStack[cpu_index][0];
20     node_info[cpu_index].index = cpu_index;
21     x86_wrmsr(IA32_KERNEL_GS_BASE_MSR, (word_t)&node_info[cpu_index]);
22     swapgs();
23 }
24 
25 #endif /* ENABLE_SMP_SUPPORT */
26