1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4  *
5  * SPDX-License-Identifier: GPL-2.0-only
6  */
7 
8 #include <types.h>
9 #include <api/failures.h>
10 #include <machine/registerset.h>
11 #include <object/structures.h>
12 #include <arch/machine.h>
13 #include <object/tcb.h>
14 
Arch_decodeTransfer(word_t flags)15 word_t CONST Arch_decodeTransfer(word_t flags)
16 {
17     return 0;
18 }
19 
Arch_performTransfer(word_t arch,tcb_t * tcb_src,tcb_t * tcb_dest)20 exception_t CONST Arch_performTransfer(word_t arch, tcb_t *tcb_src, tcb_t *tcb_dest)
21 {
22     return EXCEPTION_NONE;
23 }
24 
25 #ifdef ENABLE_SMP_SUPPORT
Arch_migrateTCB(tcb_t * thread)26 void Arch_migrateTCB(tcb_t *thread)
27 {
28 #ifdef CONFIG_HAVE_FPU
29     if (nativeThreadUsingFPU(thread)) {
30         switchFpuOwner(NULL, thread->tcbAffinity);
31     }
32 #endif
33 }
34 #endif
35