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