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