1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <object.h>
8#include <machine.h>
9#include <arch/model/statedata.h>
10#include <arch/kernel/vspace.h>
11#include <arch/kernel/thread.h>
12#include <linker.h>
13
14void Arch_switchToThread(tcb_t *tcb)
15{
16    if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
17        vcpu_switch(tcb->tcbArch.tcbVCPU);
18    }
19    setVMRoot(tcb);
20}
21
22BOOT_CODE void Arch_configureIdleThread(tcb_t *tcb)
23{
24    setRegister(tcb, SPSR_EL1, PSTATE_IDLETHREAD);
25    setRegister(tcb, ELR_EL1, (word_t)idleThreadStart);
26}
27
28void Arch_switchToIdleThread(void)
29{
30    if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
31        vcpu_switch(NULL);
32    }
33    setCurrentUserVSpaceRoot(ttbr_new(0, pptr_to_paddr(armKSGlobalUserVSpace)));
34}
35
36void Arch_activateIdleThread(tcb_t *tcb)
37{
38    /* Don't need to do anything */
39}
40