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#include <mode/kernel/tlb.h>
10
11#ifdef ENABLE_SMP_SUPPORT
12
13void Mode_handleRemoteCall(IpiModeRemoteCall_t call, word_t arg0, word_t arg1, word_t arg2)
14{
15    switch (call) {
16    case IpiRemoteCall_InvalidatePCID:
17        invalidateLocalPCID(arg0, (void *)arg1, arg2);
18        break;
19
20    case IpiRemoteCall_InvalidateASID:
21        invalidateLocalASID((vspace_root_t *)arg0, arg1);
22        break;
23
24    default:
25        fail("Invalid remote call");
26    }
27}
28
29#endif /* ENABLE_SMP_SUPPORT */
30