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