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 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 /* 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