1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <config.h>
8#include <object.h>
9#include <machine.h>
10#include <arch/model/statedata.h>
11#include <arch/kernel/vspace.h>
12#include <arch/kernel/thread.h>
13#include <linker.h>
14
15void Arch_switchToThread(tcb_t *tcb)
16{
17    if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
18        vcpu_switch(tcb->tcbArch.tcbVCPU);
19    }
20
21    setVMRoot(tcb);
22    clearExMonitor();
23}
24
25BOOT_CODE void Arch_configureIdleThread(tcb_t *tcb)
26{
27    setRegister(tcb, CPSR, CPSR_IDLETHREAD);
28    setRegister(tcb, NextIP, (word_t)idleThreadStart);
29}
30
31void Arch_switchToIdleThread(void)
32{
33    if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
34        vcpu_switch(NULL);
35    }
36
37    /* Force the idle thread to run on kernel page table */
38    setVMRoot(NODE_STATE(ksIdleThread));
39}
40
41void Arch_activateIdleThread(tcb_t *tcb)
42{
43    /* Don't need to do anything */
44}
45