1/*
2 * Copyright 2018, 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 __ARCH_ARMV_TLB_H
14#define __ARCH_ARMV_TLB_H
15
16#include <config.h>
17#include <mode/machine.h>
18
19static inline void invalidateLocalTLB_VMID(word_t vmid)
20{
21    word_t vttbr = getVTTBR();
22    word_t v = (vttbr >> 48);
23    dsb();
24    /* We need to switch to the target VMID for flushing
25     * the TLB if necessary.
26     * Note that an invalid address is used, and it seems
27     * fine. Otherwise, an ASID lookup is required.
28     */
29    if (v != vmid) {
30        setCurrentUserVSpaceRoot(ttbr_new(vmid, 0));
31    }
32    invalidateLocalTLB_VMALLS12E1();
33    if (v != vmid) {
34        /* Restore the previous VTTBR value */
35        setCurrentUserVSpaceRoot((ttbr_t) {
36            .words[0] = vttbr
37        });
38    }
39}
40
41static inline void invalidateLocalTLB_IPA_VMID(word_t ipa_plus_vmid)
42{
43    word_t vttbr = getVTTBR();
44    word_t v = (vttbr >> 48);
45    word_t vmid = ipa_plus_vmid >> 48;
46    /* The [0:35] bits are IPA, other bits are reserved as 0 */
47    word_t ipa = ipa_plus_vmid & 0xfffffffff;
48    dsb();
49    if (v != vmid) {
50        setCurrentUserVSpaceRoot(ttbr_new(vmid, 0));
51    }
52    invalidateLocalTLB_IPA(ipa);
53    if (v != vmid) {
54        setCurrentUserVSpaceRoot((ttbr_t) {
55            .words[0] = vttbr
56        });
57    }
58}
59
60#endif
61
62