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 <mode/smp/ipi.h>
9
10#ifdef ENABLE_SMP_SUPPORT
11
12void Mode_handleRemoteCall(IpiModeRemoteCall_t call, word_t arg0, word_t arg1, word_t arg2)
13{
14    switch (call) {
15    case IpiRemoteCall_InvalidateTLBEntry:
16        invalidateLocalTLBEntry(arg0);
17        break;
18
19    case IpiRemoteCall_InvalidatePageStructureCache:
20        invalidateLocalPageStructureCache();
21        break;
22
23    case IpiRemoteCall_InvalidateTLB:
24        invalidateLocalTLB();
25        break;
26
27    default:
28        fail("Invalid remote call");
29    }
30}
31
32#endif /* ENABLE_SMP_SUPPORT */
33