1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <config.h>
8#include <model/smp.h>
9#include <object/tcb.h>
10
11#ifdef ENABLE_SMP_SUPPORT
12
13void migrateTCB(tcb_t *tcb, word_t new_core)
14{
15#ifdef CONFIG_DEBUG_BUILD
16    tcbDebugRemove(tcb);
17#endif
18    Arch_migrateTCB(tcb);
19    tcb->tcbAffinity = new_core;
20#ifdef CONFIG_DEBUG_BUILD
21    tcbDebugAppend(tcb);
22#endif
23}
24
25#endif /* ENABLE_SMP_SUPPORT */
26