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
16typedef 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
22extern smpStatedata_t ksSMP[CONFIG_MAX_NUM_NODES];
23
24void migrateTCB(tcb_t *tcb, word_t new_core);
25
26#endif /* ENABLE_SMP_SUPPORT */
27
28