1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #pragma once
8 
9 #include <config.h>
10 #include <arch/types.h>
11 #include <arch/model/statedata.h>
12 #include <model/statedata.h>
13 
14 #ifdef ENABLE_SMP_SUPPORT
15 
16 typedef struct smpStatedata {
17     archNodeState_t cpu;
18     nodeState_t system;
19     PAD_TO_NEXT_CACHE_LN(sizeof(archNodeState_t) + sizeof(nodeState_t));
20 } smpStatedata_t;
21 
22 extern smpStatedata_t ksSMP[CONFIG_MAX_NUM_NODES];
23 
24 void migrateTCB(tcb_t *tcb, word_t new_core);
25 
26 #endif /* ENABLE_SMP_SUPPORT */
27 
28