1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#include <object.h> 12#include <machine.h> 13#include <arch/model/statedata.h> 14#include <arch/kernel/vspace.h> 15#include <arch/kernel/thread.h> 16#include <linker.h> 17 18void 19Arch_switchToThread(tcb_t* tcb) 20{ 21 /* set PD */ 22 setVMRoot(tcb); 23 if (config_set(CONFIG_KERNEL_X86_IBPB_ON_CONTEXT_SWITCH)) { 24 x86_ibpb(); 25 } 26 27 if (config_set(CONFIG_KERNEL_X86_RSB_ON_CONTEXT_SWITCH)) { 28 x86_flush_rsb(); 29 } 30} 31 32BOOT_CODE void 33Arch_configureIdleThread(tcb_t* tcb) 34{ 35 setRegister(tcb, FLAGS, FLAGS_USER_DEFAULT); 36 setRegister(tcb, NextIP, (word_t)idleThreadStart); 37 setRegister(tcb, CS, SEL_CS_0); 38 setRegister(tcb, DS, SEL_DS_0); 39 setRegister(tcb, ES, SEL_DS_0); 40 setRegister(tcb, FS, SEL_DS_0); 41 setRegister(tcb, GS, SEL_DS_0); 42 setRegister(tcb, SS, SEL_DS_0); 43} 44 45void 46Arch_switchToIdleThread(void) 47{ 48 /* Force the idle thread to run on kernel page table */ 49 setVMRoot(NODE_STATE(ksIdleThread)); 50} 51 52void 53Arch_activateIdleThread(tcb_t* tcb) 54{ 55 /* Don't need to do anything */ 56} 57 58void 59Mode_postModifyRegisters(tcb_t *tptr) 60{ 61 /* Don't need to do anything */ 62} 63