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