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 
Arch_switchToThread(tcb_t * tcb)15 void 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 
Arch_configureIdleThread(tcb_t * tcb)25 BOOT_CODE void Arch_configureIdleThread(tcb_t *tcb)
26 {
27     setRegister(tcb, CPSR, CPSR_IDLETHREAD);
28     setRegister(tcb, NextIP, (word_t)idleThreadStart);
29 }
30 
Arch_switchToIdleThread(void)31 void 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 
Arch_activateIdleThread(tcb_t * tcb)41 void Arch_activateIdleThread(tcb_t *tcb)
42 {
43     /* Don't need to do anything */
44 }
45