1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#include <config.h> 12#include <types.h> 13#include <api/failures.h> 14#include <api/constants.h> 15#include <machine/registerset.h> 16#include <object/structures.h> 17#include <arch/machine.h> 18 19word_t CONST 20Arch_decodeTransfer(word_t flags) 21{ 22 return 0; 23} 24 25exception_t CONST 26Arch_performTransfer(word_t arch, tcb_t *tcb_src, tcb_t *tcb_dest) 27{ 28 return EXCEPTION_NONE; 29} 30 31#ifdef ENABLE_SMP_SUPPORT 32void 33Arch_migrateTCB(tcb_t *thread) 34{ 35#ifdef CONFIG_HAVE_FPU 36 /* check if thread own its current core FPU */ 37 if (nativeThreadUsingFPU(thread)) { 38 switchFpuOwner(NULL, thread->tcbAffinity); 39 } 40#endif /* CONFIG_HAVE_FPU */ 41} 42#endif /* ENABLE_SMP_SUPPORT */ 43 44void 45Arch_setTCBIPCBuffer(tcb_t *thread, word_t bufferAddr) 46{ 47#if defined(CONFIG_IPC_BUF_TPIDRURW) 48 setRegister(thread, TPIDRURW, bufferAddr); 49#endif 50} 51