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