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 <types.h>
9 #include <api/failures.h>
10 #include <sel4/constants.h>
11 #include <machine/registerset.h>
12 #include <object/structures.h>
13 #include <arch/machine.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     /* check if thread own its current core FPU */
30     if (nativeThreadUsingFPU(thread)) {
31         switchFpuOwner(NULL, thread->tcbAffinity);
32     }
33 #endif /* CONFIG_HAVE_FPU */
34 }
35 #endif /* ENABLE_SMP_SUPPORT */
36