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 <mode/smp/ipi.h>
10#include <arch/kernel/tlb.h>
11
12static inline void invalidateTLBEntry(vptr_t vptr, word_t mask)
13{
14    invalidateLocalTLBEntry(vptr);
15    SMP_COND_STATEMENT(doRemoteInvalidateTLBEntry(vptr, mask));
16}
17
18static inline void invalidatePageStructureCache(word_t mask)
19{
20    invalidateLocalPageStructureCache();
21    SMP_COND_STATEMENT(doRemoteInvalidatePageStructureCache(mask));
22}
23
24static inline void invalidateTLB(word_t mask)
25{
26    invalidateLocalTLB();
27    SMP_COND_STATEMENT(doRemoteInvalidateTLB(mask));
28}
29
30