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