Searched refs:cpu_index (Results 1 - 3 of 3) sorted by relevance

/seL4-l4v-master/seL4/src/arch/x86/64/model/
H A Dsmp.c16 BOOT_CODE void mode_init_tls(cpu_id_t cpu_index) argument
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]);
/seL4-l4v-master/seL4/include/arch/x86/arch/32/mode/model/
H A Dsmp.h32 static inline BOOT_CODE void mode_init_tls(cpu_id_t cpu_index) argument
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/model/
H A Dsmp.h56 mode_init_tls(cpu_id_t cpu_index);

Completed in 14 milliseconds