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 15word_t CONST Arch_decodeTransfer(word_t flags) 16{ 17 return 0; 18} 19 20exception_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 26void 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