1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
8 * See "LICENSE_GPLv2.txt" for details.
9 *
10 * @TAG(DATA61_GPL)
11 */
12
13#ifndef __MODEL_SMP_H_
14#define __MODEL_SMP_H_
15
16#include <config.h>
17#include <arch/types.h>
18#include <arch/model/statedata.h>
19#include <model/statedata.h>
20
21#ifdef ENABLE_SMP_SUPPORT
22
23typedef struct smpStatedata {
24    archNodeState_t cpu;
25    nodeState_t system;
26    PAD_TO_NEXT_CACHE_LN(sizeof(archNodeState_t) + sizeof(nodeState_t));
27} smpStatedata_t;
28
29extern smpStatedata_t ksSMP[CONFIG_MAX_NUM_NODES];
30
31void migrateTCB(tcb_t *tcb, word_t new_core);
32
33#endif /* ENABLE_SMP_SUPPORT */
34
35#endif /* __MODEL_SMP_H_ */
36