Ben Simner^1
Alasdair Armstrong^1
Jean Pichon-Pharabod^2

Christopher Pulte^1
Richard Grisenthwaite^3
Peter Sewell^1

^1  University of Cambridge, UK<EMAIL_ADDRESS>
^2  Aarhus University, Denmark<EMAIL_ADDRESS>
^3    Arm Ltd., UK

– Draft –

Virtual memory is an essential mechanism for enforcing security boundaries,
but its relaxed-memory concurrency semantics has not previously been investigated in detail.  The concurrent systems code managing virtual memory has been left on an entirely informal basis, and
OS and hypervisor verification has had to make major simplifying assumptions.

We explore the design space for relaxed virtual memory semantics in the  architecture, to support future system-software verification. We identify many design questions, in discussion with Arm; develop a test suite, including use cases from the pKVM production hypervisor under development by Google; delimit the design space with axiomatic-style concurrency models; prove that under simple stable configurations our architectural model collapses to previous “user” models; develop tooling to compute allowed behaviours in the model integrated with the full Armv8-A ISA semantics; and develop a hardware test harness.

This lays out some of the main issues in relaxed virtual memory  bringing these security-critical systems phenomena into the domain of programming-language semantics and verification with foundational architecture semantics.

This document is an extended version of a paper in ESOP 2022, with additional explanation and examples in the main body, and appendices detailing our litmus tests, models, proofs, and test results.

§ INTRODUCTION

Computing relies on virtual memory to enforce security boundaries:

hypervisors and operating systems manage mappings from virtual to
physical addresses to restrict access
to physical memory and memory-mapped devices,
and thereby to ensure that processes and virtual machines cannot interfere with each other, or with the parent OS or hypervisor.

a world with endemic use of memory-unsafe languages for critical infrastructure, and of hardware that does not enforce fine-grained protection, virtual memory is one of the few mechanisms one has to enforce strong security guarantees.

This has driven interest in hypervisors and virtual machines, and it
provides a compelling motivation for verification of the OS-kernel and hypervisor code that manages virtual memory to provide security.

However, any such verification requires a semantics for the protection mechanisms provided by the underlying hardware architecture.

There are two major challenges in establishing such a semantics.

First, there is its sequential intricacy: virtual memory is one of the most complex aspects of a modern

For 64-bit Armv8-A (AArch64) it is described in a 166-page chapter of the prose reference manual <cit.> and includes a host of features and options.

Second, and more fundamentally, there is its relaxed memory behaviour.
Hardware implementations of virtual memory use in-memory representations of the virtual-to-physical address mappings, represented as hierarchical page tables.
For performance, there are dedicated cache structures for commonly used mapping data, in Translation Lookaside Buffers (TLBs).
Translations are used often – a single load instruction might need 40 or more page-table entries to translate its fetch and access addresses – but they are changed only rarely, and by systems code not user code. Architectures therefore require manual management of TLB caching, e.g. with specific instructions to invalidate old TLB entries that should no longer be used, instead of providing the simpler coherent memory abstraction that they do for normal accesses.

All this gives rise to new relaxed-memory effects, with subtle constraints determining when translations are required or forbidden to read from specific writes to the page tables, and systems code has to handle these appropriately to provide the desired virtual-memory abstraction and its security properties.

Previous work has developed hand-written sequential semantics for some aspects of address translation in Arm <cit.>
and x86

but these are at best lightly validated formalisations, and
there is no well-validated relaxed-memory concurrency semantics of virtual memory.

In the absence of that (and of proof techniques above it), previous OS and hypervisor verification work,
e.g. on seL4, CertiKOS, KCore, Hyper-V, the PROSPER hypervisor, and SeKVM [25, 40, 37, 44, 11, 38, 43, 62]
has had to make major simplifying assumptions,
either assuming correctness of TLB management and a single-threaded setting (seL4), or assuming sequentially consistent concurrency with one of those hand-written sequential semantics, or assuming an extended notion of data-race-freedom
(we return to the related work in <ref>).

We explore the design space for Armv8-A relaxed virtual memory semantics,

to support future systems-software verification.  We contribute:

* A description of the current Arm architectural intent as we understand it,
and a set of design questions and issues arising from its relaxed virtual memory semantics (<ref>).

* A relaxed virtual memory test suite, comprising of a set of hand-written litmus tests
which illustrate the aforementioned design questions and capture key use cases from
pKVM, a production hypervisor under development by Google (<ref>).

* An axiomatic-style concurrency model for relaxed virtual memory in Armv8 (<ref>),
which to the best of our knowledge and ability captures the architectural intent described
in <ref>.
We also define a weaker model, motivated by the properties pKVM relies on.

* We prove that,

for stable injective page-tables, the first model collapses to the previous Armv8-A user-mode concurrency model (<ref>).

* We extend our Isla tool [15], enabling it to compute the allowed behaviours of virtual memory litmus tests with respect to arbitrary axiomatic models,
using the authoritative Arm ASL definition of the intra-instruction semantics including pagetable walks (<ref>).

* We develop a test harness that lets us run virtual-memory litmus tests bare-metal, albeit currently only for Stage 1 tests, and report results from running these on hardware (<ref>).

We begin in <ref> with an informal introduction to virtual memory in a simple sequential setting, to make this as self-contained as possible, but familiarity with virtual memory from a systems perspective, and with previous work on user-space relaxed memory, will be helpful.

Mainstream industrial architecture specifications evolve over many years, balancing
hardware-implementation and systems-software concerns.

Experience with “user” relaxed-memory concurrency has shown that the process of developing rigorous semantics for arbitrary code provides a useful third input into this process,

leading one to ask questions which help clarify the architectural intent.

The architects, hardware designers, and system-software authors typically have a deep understanding of the area, but there is usually not, a priori, a well-understood informal specification that just needs to be formalised; instead that needs to be iteratively and collaboratively developed.

Our <ref> is based on
detailed discussion with the Arm Chief Architect
(a co-author of this paper);

the current Arm prose documentation [13];
discussion with the pKVM development team;
and our experimental testing.

To the best of our knowledge, our models provide a reasonable basis for software development and for verification,  but this paper is

surely not the last word on the subject,
and it does not give an authoritative definition of the Armv8-A architecture.

The history of relaxed-memory models shows that it typically takes multiple years, and gradual refinement of models, to converge on something reasonably stable for a production architecture or language, and even then they continue to change as new knowledge or features arise; with hindsight, few are definitive.

Our goal here is rather to lay out some of the main issues,

bringing this security-critical systems code into the domain of programming-language semantics and verification, above foundational architecture semantics.

This document is an extended version of a paper in ESOP 2022 [56], with additional explanation and examples in the main body, and appendices detailing our
litmus tests (<ref>),
models (<ref>),
proofs (<ref>), and test results (<ref>).
Further details are at <https://www.cl.cam.ac.uk/users/pes20/RelaxedVM-Arm/>.

§.§.§ Scope and non-goals

Our scope is Armv8-A virtual memory for the 64-bit (AArch64) architecture,
aiming especially to support aspects relevant to hypervisors such as pKVM.
Accordingly, we consider translation with multiple stages (for both hypervisor and OS), multiple levels, and the full Armv8-A intra-instruction semantics and translation walk behaviour (as defined by Arm in ASL and auto-translated to Sail [14]).
Our models cover the Armv8-A ETS option as work in progress.
We discuss some mixed-size aspects, but our models do not currently cover them.

To keep things manageable,
we do not consider hardware management of access flags or dirty bits, conflict aborts, feat_bbm, feat_cnp, feat_xs, the interactions between virtual memory and instruction-fetch, or all the relaxed behaviour of exceptions, and we handle only some of the many varieties of the TLBI instruction.

We focus on the specification of the architecturally allowed envelope of functional behaviour, not on side-channel phenomena.

We include some experimental testing, as a sanity check of our models, but our principal goal is to capture the architectural intent, and our principal validation is from discussion with Arm.

Many of the issues should also be relevant to other architectures, but here we address only Armv8-A.

§ BACKGROUND: A CRASH COURSE ON VIRTUAL MEMORY

§.§ Virtualising addressing

In conventional computer systems, the underlying memory is indexed by physical addresses (PAs), as are memory-mapped devices.
For a small microcontroller running trusted code, accessing resources directly via physical addresses may suffice.
Larger systems rely heavily on virtual addressing: they interpose one or more layers of indirection between virtual addresses (VAs) used by instructions and the underlying physical addresses.   This lets them:

* partition resources among different programs, giving each access only to those it needs;

* provide convenient numeric ranges of virtual addresses to each program; and

* dynamically extend and change the mapping from virtual to physical addresses, e.g. to support copy-on-write or
swapping, or shared buffers.

A simple system might have many processes managed by an operating system, each of which (including the OS) has a partial function that gives the physical address and permissions for the virtual addresses it can use, roughly:

\[\begin{array}{l}
\texttt{translate} : \texttt{VirtualAddress} \rightharpoonup \texttt{PhysicalAddress} \times 2^{\{\texttt{Read}, \texttt{Write}, \texttt{Execute}\}}
\end{array}\]

Typically each process would have access to a subset of the physical addresses (the range of its translate function), disjoint from those of the other processes and from that of the OS, while the OS would have sole access to its own working memory and also access to that of the processes.

This is implemented with a combination of hardware and system software.
The hardware memory management unit (MMU) automatically translates virtual

to physical addresses when doing an access needed to execute an instruction.  If the function is undefined, the instruction traps with a page fault; if it is defined but does not have the appropriate accesses, it traps with a permission fault; and if it is defined with the right permissions, the hardware performs the required access using the resulting physical address.

The OS has to set up the translate functions, ensure that the appropriate function is used when switching to a new process, and handle those faults.
In general translation functions are not necessarily injective,
and includes not just access permissions (which can moreover vary between exception levels),
but also additional fields for
cacheability, shareability, security, contiguity, and other aspects which we elide for simplicity here.

§.§ The translation-table walk

The current translate function for execution is determined by a system register, a translation table base register or , that contains the physical address of a lookup-tree data structure in memory.

The details of this structure are (in Armv8-A) highly configurable, e.g. for different page sizes, controlled by various system registers.
In a common configuration used by Linux, it maps 4096-byte pages and has a tree up to four levels (0–3) deep.
We assume this configuration for the remainder of this section.

Each node in the tree is a 4096-byte block of memory
made up of 512 64-bit entries (called “descriptors” by Arm).

These descriptors are of various types, either: invalid, indicating that this part of the domain is unmapped;
a block or page descriptor, defining a fixed-size mapping to a range of output addresses;
or a table descriptor which points
to another level of table for this part of the domain.

The least significant two bits of the descriptor define what type the descriptor is,
and the other bits are partitioned into various fields depending on the type:

* Output address (OA): the page the final output (IPA or PA) address is in.

* Table pointer: a 4k-aligned pointer to the next-level translation table.

* Attrs: encoding of the access permissions, memory attributes, shareability, access bits and dirty flags.

Invalid descriptors

[x=-/74,y=2.5ex,every path/.style=draw=black,semithick]

at (63-.5,1.5) 63;
at (33-.5,1.5) …;
at (1+.5,1.5) 1;
at (0+.5,1.5) 0;

(1,0) rectangle (63,1);
at (33,0.5) ignored;

(0,0) rectangle (1,1);
at (0+.5,0.5) 0;

Block or page descriptors

[x=-/74,y=2.5ex,every path/.style=draw=black,semithick]

at (63-.5,1.5) 63;
at (50+1,1.5) 50;

at (47,1.5) 47;
at (24+.5,1.5) n;
at (22-.5,1.5) (n-1);
at (13,1.5) 12;
at (11,1.5) 11;
at (2+.5,1.5) 2;
at (1+.5,1.5) 1;
at (0+.5,1.5) 0;

(0,0) rectangle (1,1);
at (0+.5,0.5) 1;

(1,0) rectangle (2,1);
at (1+.5,0.5) x;

(2,0) rectangle (12,1);
at (6+.5,0.5) attrs;

(12,0) rectangle (24,1);
at (17+.5,0.5) ignored;

(24,0) rectangle (48,1);
at (36+.5,0.5) output address;

(48,0) rectangle (49,1);
(49,0) rectangle (50,1);
at (48+.5,0.5) 0;
at (49+.5,0.5) 0;

(50,0) rectangle (64,1);
at (56+.5,0.5) attrs;

Here n depends on how deep in the table this entry is:
for a level 1 block descriptor $n==30$,
for a level 2 it is 21,
and for level 3 it is 12.
Note that bit 1 should be set when at level 3 (a page descriptor),
otherwise it is 0 for block descriptors.

Table descriptors

[x=-/74,y=2.5ex,every path/.style=draw=black,semithick]

at (63-.5,1.5) 63;
at (50+1,1.5) 50;

at (47,1.5) 47;
at (13,1.5) 12;
at (11,1.5) 11;
at (2+.5,1.5) 2;
at (1+.5,1.5) 1;
at (0+.5,1.5) 0;

(0,0) rectangle (1,1);
at (0+.5,0.5) 1;

(1,0) rectangle (2,1);
at (1+.5,0.5) 1;

(2,0) rectangle (12,1);
at (6+.5,0.5) attrs;

(12,0) rectangle (48,1);
at (30+.5,0.5) table pointer;

(48,0) rectangle (49,1);
(49,0) rectangle (50,1);
at (48+.5,0.5) 0;
at (49+.5,0.5) 0;

(50,0) rectangle (64,1);
at (56+.5,0.5) attrs;

Table descriptors are allowed only at levels 0–2.

Arm's translation-table walk

The sequential behaviour of Arm's translation-table walk function is fully defined in the Arm ASL language.

The hardware walker first splits up the input virtual address into chunks:
the upper 16 bits are typically ignored;
fields a-d are used for indexing into the tables; and
field e is added to the final result to get the physical address.

[x=-/74,y=2.5ex,every path/.style=draw=black,semithick]

(63+.5,2.5) – (0-.5,2.5) node [black,midway,yshift=0.5cm,xshift=-0.1cm] VA;

at (63-.5,1.5) 63;
at (48+1,1.5) 48;

at (47-.5,1.5) 47;
at (39+1,1.5) 39;

at (38-.5,1.5) 38;
at (30+1,1.5) 30;

at (29-.5,1.5) 29;
at (21+1,1.5) 21;

at (20-.5,1.5) 20;
at (12+1,1.5) 12;

at (11-.5,1.5) 11;
at (0+.5,1.5) 0;

(0,0) rectangle (12,1);
at (5+.5,0.5) e;

(12,0) rectangle (21,1);
at (16+.5,0.5) d;

(21,0) rectangle (30,1);
at (25+.5,0.5) c;

(30,0) rectangle (39,1);
at (34+.5,0.5) b;

(39,0) rectangle (48,1);
at (43+.5,0.5) a;

(48,0) rectangle (63,1);
at (55,0.5) ignored;

A pointer to the initial level of translation is obtained by reading the relevant translation table base register (TTBR).
The fields a-d are then used to indirect into each table in turn,
until a block (or page) mapping is found.

Each level of the tree maps a different size block.
e.g. in a common configuration
each level 1 entry maps a 1GiB region,
each level 2 a 2MiB region,
and each level 3 a single 4KiB page.

[x=/74,y=2.5ex,every path/.style=draw=black,semithick]

(0, 0) rectangle (8,2);
at (4, 1) ttbr;

ıin 0,1,2,3

[->] (8,1) – (12,1);

30y: page;

[->] 000;
[->] 100;
[->] 200;
[->] 30-44KiB;

12x: block;
[->] 12-41GiB;

[<->] 0a;
[<->] 1b;
[<->] 2c;
[<->] 3d;

The final physical address is the output address field of the page or block mapping,
with the remaining bits of the VA appended.

For example, if the VA was translated using the 4KiB page entry y from above:

[x=-/74,y=2.5ex,every path/.style=draw=black,semithick]

(63+.5,2.5) – (0-.5,2.5) node [black,midway,yshift=0.5cm,xshift=-0.1cm] PA from y;

at (63-.5,1.5) 63;
at (48+1,1.5) 48;

at (11-.5,1.5) 11;
at (0+.5,1.5) 0;

(0,0) rectangle (12,1);
at (5+.5,0.5) e;

(12,0) rectangle (48,1);
at (29,0.5) OA from page descriptor;

(48,0) rectangle (63,1);
at (55,0.5) ignored;

Or for the 1GiB level 1 block entry x:

[x=-/74,y=2.5ex,every path/.style=draw=black,semithick]

(63+.5,2.5) – (0-.5,2.5) node [black,midway,yshift=0.5cm,xshift=-0.1cm] PA from x;

at (63-.5,1.5) 63;
at (48+1,1.5) 48;

at (47-.5,1.5) 47;
at (30+1,1.5) 30;

at (29-.5,1.5) 29;
at (21+1,1.5) 21;

at (20-.5,1.5) 20;
at (12+1,1.5) 12;

at (11-.5,1.5) 11;
at (0+.5,1.5) 0;

(0,0) rectangle (12,1);
at (5+.5,0.5) e;

(12,0) rectangle (21,1);
at (16+.5,0.5) d;

(21,0) rectangle (30,1);
at (25+.5,0.5) c;

(30,0) rectangle (48,1);
at (39,0.5) OA from block;

(48,0) rectangle (63,1);
at (55,0.5) ignored;

Note that,
as mentioned before,
the architecture is highly configurable
and the above diagrams give just a common configuration.
Various system registers allows the user to configure:
the size of the input addresses (e.g. 48 bit, 52 bit);
the number of translation table levels (e.g. 3, 4, 5);
the size of a page (e.g. 4K, 16K, 64K),
and much more that we elide here for brevity.

§.§ Multiple stages of translation

The above suffices for an operating system isolating multiple processes from each other, but one often wants to isolate multiple operating systems (or other guests), managed by a hypervisor.
To support this, the architecture provides a second layer of indirection: instead of going straight from virtual to physical addresses, with a single stage of mapping controlled by the OS,
one can have two stages, with the OS managing a Stage 1 table which maps virtual addresses to an intermediate physical addresses (IPAs),
composed with a hypervisor-managed Stage 2 table, mapping IPAs to PAs.
The full translation composes the two, intersecting
their permissions.

\[ \begin{array}{l}
\texttt{translate\_stage1} : \texttt{VirtualAddress} \rightharpoonup \texttt{IPA} \times 2^{\{\texttt{Read}, \texttt{Write}, \texttt{Execute}\}}\\
\texttt{translate\_stage2} : \texttt{IPA} \rightharpoonup \texttt{PhysicalAddress} \times 2^{\{\texttt{Read}, \texttt{Write}, \texttt{Execute}\}}
\end{array}
\]

Armv8-A has various exception levels (ELs), determined by the PSTATE.CurrentEL register,
including EL0 (for user processes), EL1 (for OSs or other

guests), and EL2 (for a hypervisor).
These each have associated translation-table base registers:

* TTBR0_EL1: contains a pointer (IPA) to the Stage 1 table for EL1&0, lower VA range (process addresses), producing IPAs, controlled by OS at EL1

* TTBR1_EL1: contains a pointer (IPA) to the Stage 1 table for EL1&0, upper VA range (OS kernel addresses), producing IPAs, controlled by OS at EL1

* VTTBR_EL2: contains a pointer (PA) to the Stage 2 table (second stage for IPAs translated at EL1&0), producing PAs, controlled by hypervisor at EL2

* TTBR0_EL2: contains a pointer (PA) to the single-stage table for EL2 (hypervisor's own addresses), producing PAs, controlled by hypervisor at EL2

Each hardware thread has its own base registers (and other system registers), and so different hardware threads can be using different address spaces (for example, for different processes)
at the same time.

§.§ Caching translations in TLBs

A naive hardware implementation of address translation would need many translation memory reads – with four levels,
up to 24 with both stages enabled, for every instruction-fetch, read, or write.

This would have unacceptable performance, so processors have
specialised caches for translation-table wal k reads called
translation lookaside buffers (or TLBs).
Under normal operation the TLBs are invisible to user code,
but systems code has to manage them explicitly,
to change which translation table is currently in use (e.g. when context switching),

or to make changes to the tables for one process or guest.

Without correct management a TLB could hold incorrect (stale) data,
breaking the protection that the address translation is intended to provide.

The architecture supports explicit TLB maintenance with various
flavours of the TLBI instruction
(TLB invalidate),
to invalidate old entries for specific ranges of virtual or intermediate-physical addresses,

or even whole ASIDs or VMIDs at once.

The memory management unit (MMU) is responsible for performing these translations.
It does this by looking at the TLB and, if the TLB does not contain an entry for the given address
(called a miss),
it performs the translation table walk function as described earlier and caches the result in the TLB (a fill).

TLB maintenance and TLB misses are expensive,
and one would not want the cost of TLB invalidation on every context switch,
so the architecture provides
address space identifiers (ASIDs).
The translation table base registers include an ASID in addition to the table base address,
and when translation data is cached in a TLB it is tagged with the current ASID,
giving the illusion of separate TLBs per ASID, and

allowing switching from one to another without TLB maintenance.

Eventually the system will need to reclaim and reuse a previously used ASID,
and then TLB maintenance is required to clean that ASID's old entries.

There are similar identifiers for Stage 2 intermediate physical memory,
known as virtual-machine identifiers or VMIDs.

§ CONCURRENCY ARCHITECTURE DESIGN QUESTIONS

Now we will

introduce the main concurrency architecture design questions that arise for Armv8-A virtual memory, within the scope laid out in the introduction.

As usual, the architecture has to define an envelope of behaviour that provides the guarantees needed by software, while admitting the relaxed behaviour of the microarchitectural techniques necessary for performance.

That means we have to discuss both, including just enough microarchitecture to understand the possible programmer-visible behaviour, before we abstract it in the semantic models we give in <ref>.

The discussion includes points of several kinds:
some that are clear in the current Arm documentation,
some where Arm have a change in flight,
some that are not documented but where the semantics is (after discussion) obviously constrained by existing hardware or software practice,
and some where there is a tentative Arm intent but it is not yet fixed upon;

our modelling raised a number of questions of the latter two.

To make this as coherent as possible, we discuss all these in a logical order, laying out the design principles.

We have developed a suite comprised of  hand-written Isla-compatible virtual-memory litmus tests that illustrate the issues,
but to keep this concise we just give the main ideas here.  For ease of reference, we give the actual tests in App. <ref>, with links in the margin.

As a sample, we explain one pKVM test in detail in <ref>.

§.§ Coherence with respect to physical or virtual addresses

For normal memory accesses, the most fundamental guarantee that architectures provide is coherence:  in any execution, for each memory location, there is a total order of the accesses to that location, consistent with the program order of each thread, with reads reading from the most recent write in that order.

Hardware implementations provide this, despite their elaborate cache hierarchies and out-of-order pipelines, by
coherent cache protocols and pipeline hazard checking, identifying and restarting instructions when possible coherence violations are detected.

Previous work on relaxed-memory semantics for architectures has

taken virtual addresses as primitive, implicitly considering only execution with well-formed, constant, and injective address translation mappings.

Now, we have to consider whether coherence is with respect to virtual or physical addresses, for non-injective mappings.

For Arm, coherence is w.r.t. physical addresses <cit.>. CoRR0.alias+po
This means
that if two virtual addresses alias to the same physical address, then (still assuming well-formed and constant translation):

a load from one virtual address cannot ignore a program-order (po) previous store to the other; and CoWR.alias

a load from one virtual address can have its value forwarded from a store to the other,   and similarly on a speculative branch. MP.alias3+rfi-data+dmb

§.§ Relaxed behaviour from TLB caching

There are two main aspects of the concurrency semantics of virtual memory:
the relaxed behaviour arising directly from TLB caching,
and the relaxed behaviour of the not-from-TLB (non-TLB) memory accesses for translation reads that read from memory or by forwarding from po-previous writes, and that might supply TLB cache fills.  We discuss them in this and the following subsection respectively.

What can be cached

The MMU can cache information from successful translations, and also from translations that result in permission faults, but it is architecturally forbidden from caching information from attempted translations that result in translation faults.
This ensures that the handlers of those faults do not need to do TLB maintenance to remove the faulting entry <cit.>, and makes the potential behaviour for page-table updates from invalid-to-valid and
quite different, as we shall see.

TLB implementations might cache any combination of individual page-table entries and partial or complete translations, e.g. from the virtual address and context to the physical address of the last-level page.  Conceptually, however, we can simply view a TLB as containing a set of cached page-table-entry writes (i.e., writes that have been read from for a translation), including at least:

* the context information of the translation: the VMID, ASID
(or a “global indicator”),
,     and the originating exception level;

* the virtual address, intermediate physical address, and/or physical address of the translation;

* the translation stage and level at which the write was used;

* the system register values used in the translation (those which can be cached); and

* for an entry used for a Stage 1 translation, whether it has been invalidated at both stages.

That additional information allows the various TLBI instructions to target specific entries.CoWinvT+dsb-isb

A translation walk can arbitrarily use either a cached write (if one exists) or do a non-TLB read, either from memory or by forwarding from a po-previous write, for any stage or level.

Caching of multiple entries for the same virtual address and context

High-performance hardware implementations may have elaborate TLB structures, including multiple “micro TLBs” per thread.

These can be seen as a conceptual single per-thread TLB that can hold zero, one, or more entries for each combination of input address and the other information above.

If zero, a translation will necessarily read from memory (with ordering constrained as discussed below).
If one or more, a translation may use any of those entries or read from memory (and the write read from might or might not be cached). CoTfT+dsb-isb

However, in some cases multiple entries constitute a break-before-make failure, leading to relatively unconstrained behaviour; we return to this below.

When can page-table entries be cached

memory read by a translation can be cached.

thread can spontaneously do a translation for any virtual address at
any program point, with respect to its context at that point
(though this interacts with the
system-register write/read semantics). Spontaneous translations model

prefetching, speculative execution, and branch

They mean that, in the absence of cache maintenance,
translations may use TLB entries from arbitrarily old writes. CoWinvT+dsb-isb

Additionally, any thread may do a spontaneous translation at any point using
the configuration from

any exception level higher than the current one, but not for lower levels.

Preventing spontaneous walks at lower EL is essential, as during an EL2 hypervisor switch between VMs, the EL1 control registers will be in an inconsistent state.

Allowing spontaneous walks at higher EL models arbitrary interrupts to the higher level and then doing a spontaneous walk there.

Each virtual-memory access by a thread involves a non-spontaneous translation which
is constrained by the normal inter-instruction constraints on
out-of-order and speculative execution by the thread.

constraints are especially important in order to understand when a translation
must fault: as invalid entries cannot be cached, a translation that gives rise to such a fault must be at least in part from a non-TLB read, subject to these ordering constraints. CoTfRpte+dsb-isb

Coherence of translations

Due to the TLB caching as described above

translations of the same virtual address by the same thread need not see a coherent view of page-table memory.

This is in sharp contrast to normal accesses, but analogous to instruction-fetch reads [57]
and reads from persistent memory [51]. CoTfT+dsb-isb

Removing cached entries

TLBs may spontaneously forget any cached information at any point.

To ensure that a cached entry is removed,
software must ensure that it will not be spontaneously re-cached.
It can do this with a write of an invalid entry and then a DSB instruction (data synchronization barrier) to ensure that it is visible across the system,
followed by a TLBI.

Break-before-make failures

When changing an existing translation mapping, from one valid entry to another valid entry, Arm require in many cases the use of a break-before-make (BBM) sequence:  breaking the old mapping with a write of an invalid entry;
a DSB to ensure that is visible across the system;
and a broadcast TLBI
to invalidate any cached entries for all relevant threads;
a DSB to wait for the TLBI to finish;
then making the new mapping with a write of the new entry, and additional synchronisation  to ensure that it is visible to translations (specifically, to translation-walk non-TLB reads).

The current Arm text <cit.> identifies six cases of page-table updates that without such a sequence constitute BBM failures, and gives very severe architectural consequences:  failures of coherency, single-copy atomicity, ordering, or uniprocessor semantics.
Note that these consequences are architecturally allowed if there could exist a break-before-make-failure change to the translation tables for some virtual address, irrespective of whether the program architecturally accesses it.

This severity is because, in some of the six cases, hardware implementations could give rather arbitrary behaviour, e.g. an amalgamation of old and new entries.
From a software point of view, it seems that one must treat such cases more-or-less as fatal errors. This is analogous to the Data-race-free-or-catch-fire semantics underlying the C/C++

relaxed memory model [4, 33, 22, 20], in which any program with a consistent execution that includes a race between nonatomic accesses is deemed to have undefined behaviour, and the C/C++ standards do not constrain implementation behaviour for such programs in any way.

This makes many potential litmus tests that change between valid entries uninteresting, as they simply exhibit BBM failures (though changes of permissions do not necessitate a BBM sequence).

However, for a processor architecture that supports virtualisation, one cannot regard BBM failures as allowing completely arbitrary behaviour for the entire machine: if one guest virtual machine (at EL1) changes one of its own translation mappings without correctly following the BBM sequence, either mistakenly or maliciously, that should not impact security of the hypervisor (at EL2) or other guests.  Instead, one has to bound the arbitrary behaviour to that virtual machine, allowing arbitrary memory and register accesses that are possible within its context.
In our exhaustively executable semantics, to keep litmus-test executions finite, we currently simply detect BBM failures; we do not explicitly model that arbitrary behaviour.

In reality, these six BBM failure cases include some where hardware may give such weakly constrained behaviour and others where, because coherence is over physical addresses and the mapping may be temporarily indeterminate, software might see well-defined but nondeterministic or surprising results. These were architected as a guide for system software to produce predictable behaviour, and future versions of the architecture might refine this.

When a hypervisor installs a new guest, it has to be able to reset to a clean state, in case a previous guest has failed to follow the BBM sequence (which in general the hypervisor cannot know).
It can do so with a TLBI
covering all the previous guest's processes address space.

There seems to be no need or support for finer-grain cleanup.

§.§ Relaxed behaviour of translation-walk non-TLB reads

Now we turn to the semantics of translation-walk non-TLB reads, those that are satisfied from memory or by forwarding, not from a TLB, and which might then be cached in a TLB.
This matters especially when one knows that there are no relevant cached TLB entries,

e.g. when an invalid entry has been written and a TLBI performed,
so one knows that translation walks will do such a non-TLB read.

Ordering among the translation-walk reads of an access
Each translation-table walk for a virtual-memory access can involve many memory reads,
one for each level of the table for each stage of translation.

The diagram on the right is an example walk, where each  is read of level  of the Stage 1 table.
Each of those Stage 1 reads must first be translated to get the PA (as the table contains IPAs)
and so each  is a read of level  of the Stage 2 table for the address of the Stage 1 table at level .
Once the full Stage 1 walk has been completed the final output IPA must be translated to the final PA, and those are the final 4
reads, of the Stage 2 table at level .

The reads are ordered one after another in the order they appear in the ASL walk function.
This ordering must be respected by hardware
as software relies on it when building the tables bottom-up.

For example, if one starts with a Level 2 invalid entry, one might first create a Level 3 table (then a barrier to keep writes ordered).ROT.inv+dmbst
ROT.inv+dsb In other words, the architecture has to prohibit value speculation of page table entries.

Dependencies into translation-walk non-TLB reads
Address dependencies into a memory-access instruction in classic “user” models are now explainable as dataflow dependencies

to the translation reads of those accesses, as the address has to be available before a walk can start.
These are virtual-address dataflow dependencies (contrasting with physical-address coherence).

Translation-walk non-TLB reads from non-speculative same-thread writes

PO-past A translation-walk non-TLB read might read from a po-previous page-table-entry write, but it is only guaranteed to see such a write if there is enough intervening synchronisation.

Arm have recently introduced  Enhanced Translation
Synchronization (ETS), optional in Armv8.0 and mandatory from Armv8.7.
Armv8-A implementations without ETS require both a DSB, to make the write visible to translation-walk non-TLB reads, and an ISB, to ensure that any translations for later instructions that were done out-of-order, before the write, are restarted.
With ETS, only the DSB is required for a translation-walk non-TLB read to definitely see the write, though one might still need an ISB if the new translation enables new instruction fetch. CoRpteTf.inv+dsb

Because invalid entries cannot be cached, this means that if an entry is initially invalid, then after a write of a valid entry and a DSB;ISB/DSB, translations will use that valid entry.  However, the DSB;ISB/DSB does not remove cached entries, so an initially valid entry might be cached by a spontaneous walk, so even after a write (of an invalid or non-BBM-failure valid entry) and a DSB;ISB/DSB, the old entry could still be used by translations.  One would need a TLBI sequence to remove old cached entries, which we return to below.

The Armv8-A architecture allows load-store reordering, but it does not allow writes to become visible to other threads while they are still speculative. In the same vein, translation-walk non-TLB reads cannot read from po-later page-table-entry writes <cit.>. Before the po-earlier translation is complete, one cannot know that it is not going to fault, so the later write has to be considered speculative. This prevents a thread-local self-satisfying translation cycle, analogous to the prevention of load-store cycles with dependencies. CoTW1.inv

PO-present On the margin, can a translation-walk non-TLB read for a write access see that write, or a distinct write from the same instruction?  The second case could arise from a store-pair or misaligned store that does two writes, with one to a page-table-entry that could be used by the other, though real code would typically not do this intentionally.
This is explicitly allowed by the current architecture text <cit.>.

However that text does not specify whether the translations for those two writes could both read from the other,
a self-satisfying translation cycle where the writes write each others translations.
In general such self-satsifying cycles give rise to thin air behaviours and are universally forbidden by the architecture.

Translation-walk non-TLB reads from speculative same-thread writes

Speculative execution requires translation walks, which might result in additional page-table entries being cached, but in most cases this is indistinguishable from the effects of a non-speculative spontaneous walk.
However, one has to ask whether a translation-walk non-TLB read can see a po-previous write that is still speculative, e.g. while both instructions follow an as-yet-unresolved conditional branch.
It is clear that the result of such a walk should not be persistently cached, or made visible to other threads (via a shared TLB), while it remains speculative.  Moreover, such translations could lead to arbitrary reads of read-sensitive device locations, which one normally relies on the MMU to prevent.  The conclusion is therefore that this must be forbidden.

Translation-walk non-TLB reads from same-thread writes, forbidden past (same-thread TLBI completion)
To remove an existing mapping on a single thread,
one needs first to write an invalid entry, then a DSB to ensure that has reached memory and thus is visible to translation-walk non-TLB reads (to prevent spontaneous re-caching), then a TLBI to invalidate any cached entries, then a DSB to wait for TLBI completion.

Without ETS, one

also needs an ISB to ensure that po-later translations that have been done early are restarted.

With ETS, the ISB is not always necessary,
though might still be needed for
its instruction-cache effects if the change of mapping affects instruction fetch.

After all that, an attempted access by that thread is guaranteed to fault.

Translation-walk non-TLB reads from other-thread writes, guaranteed past, initially invalidMP.RTf.inv+dmb+po
Now consider when a translation-walk non-TLB read is guaranteed to see a write by another thread of a new entry, assuming that the entry was previously invalid and any cached entries for it
invalidated.  Consider a two-thread message-passing case, where a producer P0 writes a new

a:W pte(x)=pte_valid
<Producer ordering>
b:W flag=1

c:R flag=1
<$\textnormal{Receiver ordering}$>
d:Tx, for a Rx or Wx

P0     P1

page table entry (), then has some ordering before a write of a flag, while a consumer P1 reads the flag, then has some ordering before an access  or  that needs that entry for a translation     of  virtual address .

On some Armv8-A implementations that do not support ETS, some “obvious” combinations of ordering on P0 and P1 could lead to an abort of the translation of (d), which some OS software would find difficult to handle.  This was the main motivation for
implementations without it can have weak behaviour, requiring strong synchronisation to prevent the abort, while with ETS the architecture is stronger, requiring only weaker ordering to prevent the abort.

Without ETS, two combinations of ordering are architected as sufficient to ensure that the translation (d) sees the new valid entry:

*  P0 has any ordered-before relationship, and P1 has DSB+ISB.MP.RTf.inv+dmb+dsb-isb

*  P0 has DSB; TLBI; DSB, and P1 has any ordered-before relationship.MP.RTf.inv.EL1+dsb-tlbiis-dsb+dsb-isb

In Case <ref>, the message-passing is enough to ensure the write (a) is in main memory, the P1 ISB ensures that any out-of-order translation of (d) is restarted, and the P1 DSB keeps the read (c) and that ISB in order.

In Case <ref>, the first DSB ensures the write is visible to all threads, the TLBI (broadcast, for the virtual address ) invalidates any older cached entry on P1, and the second DSB waits for that TLBI to be complete, after which any new translation on P1 will have to see the new entry.

However, it appears that the probability of an unhandleable abort in practice, where one usually does not have these operations immediately adjacent, and where in many cases the abort could be handled, has been judged low enough that OS code is not necessarily using either of these.

With ETS, the architecture says <cit.>
that “if a memory access RW1 is Ordered-before a second memory access RW2, then
RW1 is also Ordered-before any translation table walk generated by RW2 that generates a Translation fault, Address size fault, or Access flag fault.”
Microarchitecturally, the intuition here is that with ETS any translation done while speculative that leads to such a fault will have to be reconfirmed as faulting when execution is no longer speculative, so an early faulting translation of (d) would have to be restarted after the ordered-before edges have ensured that (a) is visible.

However, in the case that the RW2 instruction faults, there is no read or write event, and if the fault is a translation fault, there is no physical address.  One therefore has to ask what the meaning of ordered-before edges into RW2 is, especially for the parts of ordered-before dependent on physical addresses, such as coherence.

The conclusion is that this should be only the non-physical-address parts of ordered-before into RW2, and in modelling one needs a “ghost” event to properly record what the dependencies would have been if it had succeeded.
Note that this includes ordered-before to RW2 that ends with a data dependency into a write, even though that data would not normally be necessary for the translation.

Even with ETS, one might need an ISB on P1 if the new translation affects instruction fetch.

Translation-walk non-TLB reads from other-thread writes, guaranteed past, initially valid (other-thread TLBI completion)

The following test
has a read-only mapping for

STR pte_writeable,[pte($x$)]
DSB SY
TLBI VAAE1IS,[page($x$)]
DSB SY
MOV X7,#1
STR X7,[$y$]

LDR X0,[$y$]
DMB SY
MOV X1,#1
STR X1,[$x$]

P0     P1

some physical address

that is updated with a new
writeable mapping to the same physical
address, followed by a message-pass to another thread that attempts to write.
There is no requirement for break-before-make here, as the output address has not changed,
but TLB maintenance is required to ensure that the new writeable entry is guaranteed to be used by later translation-reads.

Arm forbid the outcome where the STR faults due to a permission check.
This is because the TLBI only completes once all instructions using any old translations which would be invalidated by the TLBI,RBS+dsb-tlbiis-dsb
on all other threads that the TLBI affects, have also completed, and the following DSB waits for that (the same-thread case is different; see <ref>).
In practice this means that once the TLBI completes, one of the following holds:
either the final STR has not performed its translation of $\textit{x}$ yet and will be required to see the writeable mapping for its page table entry (pte);
or the STR has translated using the new writeable mapping;
or the STR has already translated using the old read-only mapping,
in which case  we know that the STR has finished and performed its write,
since the TLBI could not complete while it was still in-progress.
In that case if the STR has completed,
then so must have the locally-ordered-before LDR,
and that must have read 0.

This explanation also covers the make-after-break case above,
for non-ETS Case <ref>.

This is reflected in text to be included in future versions of the Arm ARM:
A TLB maintenance operation
[without nXS] generated by a TLB maintenance instruction is finished for a PE when:

* all memory accesses generated by that PE using in-scope old translation information are complete.

* all memory accesses RWx generated by that PE are complete. RWx is the set of all memory accesses generated by instructions for that PE that appear in program order before an instruction (I1) executed by that PE where:

* I1 uses the in-scope old translation information, and

* the use of the in-scope old translation information generates a synchronous data abort, and

* if I1 did not generate an abort from use of the in-scope old translation information, I1 would generate a memory access that RWx would be locally-ordered-before.

Translation-walk reads from same- and other-thread writes, forbidden past (break-before-make)

Now we can finally return to the break-before-make sequence.

Normal reads cannot read from the coherence-predecessors of the most coherence-recent write that is visible to them, but translation reads can read old (non-invalid) values from a TLB.

To prevent this, and to ensure that a translation read sees a new page-table entry,  one  has to both ensure that any old TLB entries are invalidated, with a suitable TLBI, and that the new entry is visible to translation-walk non-TLB reads.

Armv8-A says <cit.> “A break-before-make sequence on changing from an old translation table entry to a new translation table entry
requires the following steps: (1) Replace the old translation table entry with an invalid entry, and execute a DSB instruction.  (2) Invalidate the translation table entry with a broadcast TLB invalidation instruction, and execute a DSB
instruction to ensure the completion of that invalidation.
(3) Write the new translation table entry, and execute a DSB instruction to ensure that the new entry is visible.”.

Typically the write of an invalid entry and TLBI would be on the same thread,
but more generally, any shape as below should be forbidden,CoRpteT.EL1+dsb-tlbi-dsb-isb
where  is a translation-walk read for an

access of  and the  relation shows the page-table write it reads from.

In other words, the sequence ensures that the write of the
invalid entry, and of any co-predecessor writes, are hidden behind the new page-table entry  as far as new translations are concerned.

Here the P0 DSB and P0-to-P1 ob ensure the P0 write has propagated to memory before the P1 TLBI starts; the P1 DSB waits
for that TLBI to have finished on all threads; the P1-to-P2 ob ensures that has happened before the new page-table-entry write starts; and the DSB ensures the new write has reached memory and so is visible to translation before subsequent instructions.  The P2 ISB is needed if on non-ETS hardware, to force restarts of any out-of-order translations for po-later instructions, or (on any hardware) if P2=P1, to ensure any later translations on the TLBI thread are restarted, or if the new mapping affects instruction fetch.

This generalisation seems necessary, as a TLBI might be performed by a virtual CPU at EL1 which is interrupted and rescheduled by an EL2 hypervisor.  One should be able to rely on the hypervisor doing a DSB on the same hardware thread as part of the context switch, and that has to suffice.  It is sound because the DSBs and TLBI are all broadcast, though note that the DSB waiting for TLBI completion has to be on the same hardware thread as it.

Translation-walk non-TLB reads from other-thread writes, forbidden future

we saw that translation-walk non-TLB reads should not read from po-later writes.  How should

that be
generalised to multiple threads?  LB.TT.inv+pos
the simplest example, consider the translation version of the LB test on the right, in which two threads translation-read from each other's po-future ( relates translation reads to their accesses).  Standard LB shapes for normal accesses without dependencies are allowed in Armv8-A, but this example should be forbidden: until each translation is done, one cannot know that the first instruction on each thread will not abort, so one could not make the po-later write visible to the other thread without inter-thread roll-back. In other words, the possibility of translation aborts creates ordering rather like a control dependency from translation reads to po-later writes.

Multicopy atomicity of translation-walk non-TLB readsWRC.RRTf.inv+addrs
The ARMv7 and early Armv8-A architectures for normal accesses were non-multicopy-atomic: a write could become
visible to some other threads before becoming visible to all threads, broadly similar in this respect
to the IBM POWER architecture [1, 53].
This is one of the most fundamental choices for a relaxed memory model.
In 2017 Arm revised their Armv8-A architecture to be multicopy-atomic (other multicopy-atomic, or OMCA, in their terminology), a considerable simplification [49, 12].  However, there was no consideration at the time of whether this should also apply to the visibility of writes by translation-walk non-TLB reads, or of the force of the ARM statement that a translation table walk is considered to be a separate observer <cit.>.

For example, consider the following translation-read analogue of the classic WRC+addrs test, which would be forbidden in OMCA Armv8-A for normal reads.
Suppose one has ETS,

the last-level
page-table entries for x and y are
initially invalid and not cached in any TLB, P0 writes a valid entry for x, P1 does a translation that sees that entry and then (via an address dependency) writes a valid entry for y, then P2 does a translation that sees that entry and then (via an address dependency) tries a translation for x, is that last guaranteed to see the valid entry instead of faulting?  This might be exhibited by a microarchitecture with a shared TLB between P0 and P1 (e.g. if they are SMT threads on the same core, or have a shared TLB for a subcluster).

The tentative Arm conclusion is that this should be forbidden, to avoid software issues with unexpected aborts similar to those motivating ETS.

Now consider the above translation version of LB, generalising from

po-future writes to other ob-future writes. For transitive combinations of reads-from and dependencies, it

should clearly still be forbidden, to avoid needing inter-thread roll-back, but for ob including coherence edges (coe) one can imagine that a translate read could see a write before the coherence relationships are established, analogous to the weakness of coherence in the Power

Discussion of these and other cases with Arm led to the

tentative conclusion for Armv8-A that translation-walk non-TLB reads (like normal reads) do not see any non-OMCA behaviour.  In other words, there is no programmer-visible caching observable to some non-singleton subsets of threads' translations but not others.

§.§ Further issues

Our discussions with Arm identified and clarified various other architectural choices, though we do not discuss them fully here, and our models do not cover them at present.

To give a flavour:
(1) Misaligned or load/store-pair instructions give rise to multiple accesses, which might be to different pages. Each has their own translation; not ordered w.r.t. each other, and with no prioritisation of faults between them.  As noted in <ref>, one might translate-read from the other, but not both simultaneously.
(2) Normal registers act like a per-thread sequential memory, with reads reading from the most recent po-previous write, but
the system registers that control translations can have more relaxed behaviour, requiring ISBs to enforce sequential behaviour.
(3) The architecture requires, and OSs rely on, the fact that turning on
the MMU does not need TLB maintenance.  However, in a two-stage world, if
Stage 1 is off, one is still using the TLB for Stage 2, so entries do get
added to the TLB.  When one later turns on Stage 1, it is
essential that the entries added from those earlier Stage 2 translations are not
used, so one has to
regard them as from a 257'th ASID.

§ VIRTUAL MEMORY IN THE PKVM PRODUCTION HYPERVISOR

Protected KVM, or pKVM [30, 27, 2], is currently being developed by Google to provide a common hypervisor for Android, to provide improved compartmentalisation by a small trusted computing base (TCB) between the Linux kernel and other services.

pKVM is built as a component of Linux. During boot, the Linux kernel hands over control of EL2 to the pKVM code, which constructs a memory map for itself and a Stage 2 memory map to encapsulate the Linux kernel. The Linux kernel thereafter runs only at EL1 (managing EL1&0 Stage 1 memory maps for itself and for user processes), as the principal guest, also known as the host (not to be confused with the host hardware).   Other services can run as other guests, which are protected from the kernel and vice versa.  The kernel remains responsible for scheduling, but context switching
and inter-guest communication is done by hypervisor calls to the pKVM code at EL2.

This gives us an ideal setting in which to examine the management of virtual memory by production code for Armv8-A relaxed-memory-concurrency, with both one and two stages of translation (for EL2 and EL1&0 respectively).

The pKVM codebase is small, so it is feasible to examine all uses of TLB management, and we benefit from discussions with

the pKVM development team.
We have manually abstracted the main pKVM relaxed-virtual-memory scenarios into  tests.

To give a flavour for these we will explore just a few of the most fundamental for
hypervisor control of translation tables:
__pkvm_init performs first-time per-CPU initialisation of pKVM,
which includes setting up the vmemmap,
a large array storing a struct entry for each physical page in memory
with ownership information;
__kvm_vcpu_run switches to a different guest;
__kvm_flush_vm_context flushes all entries in all TLB caches that relate to Stage 1 translations;
__kvm_tlb_flush_vmid_ipa flushes entries in caches that relate to a particular guest for a given address;
__kvm_tlb_flush_vmid flushes all entries in caches that relate to a particular guest;
__kvm_flush_cpu_context flushes all entries in caches at EL1 for a given guest;
__pkvm_cpu_set_vector sets the vector base address for handling exceptions;
__pkvm_create_mappings creates entries in the Stage 1 page table that pKVM uses when it executes;

__pkvm_prot_finalize which enables Stage 2 translations during boot.

In the remainder of this section we describe a selection of litmus tests
extracted from the current pKVM source code [2] as of Dec 2021.

§.§ Switching to another guest

The most basic task that pKVM is in charge of is the actual swapping from one vCPU's context to another
to execute a particular VM on the physical CPU.
Deciding when and to which vCPU to switch is done by the underlying host Linux guest.
pKVM's role is to safely save the current guest's state,
and load the EL1 state for the target vCPU,
and manage the Stage 2 translation tables for the vCPU's VM.

Aside from the fundamental shape of switching from one VM to another on the same core,
there are a few interesting cases to consider:

* Switching from one vCPU in a VM to another vCPU in the same VM.

* Switching to a new vCPU, re-using a previous VMID.

* Re-using an old VMID with a concurrently executing vCPU on another core.

When the host guest Linux kernel wishes to perform the switch from one vCPU to another,
it writes to some general-purpose registers and then performs an HVC instruction
(in this case, to call the __kvm_vcpu_run hypercall).

In the simplest case
where pKVM is just switching from one vCPU to another vCPU
in a different VM,
pKVM restores the per-CPU register state
and sets the VTTBR with the new VMID.
So long as the two vCPUs are using disjoint VMIDs

there is no requirement for TLB maintenance.

This test, pKVM.vcpu_run, is below,

typeset (lightly hand-edited) from the TOML input format of our Isla tool (<ref>).

Here there is a single physical CPU, initially running a virtual machine VM1, with VMID , at EL1.

section on the left defines the initial and all potential states of the page tables, and any other memory state.
This test sets up separate translation tables for pKVM at EL2 (which has just a single stage) and for two VMs (each with two stages, Stage 2 controlled by pKVM and Stage 1 controlled by the VM).

pKVM's own mapping  maps its code.

VM1's own Stage 1 mapping  maps virtual address  to ,
and the initial pKVM-managed Stage 2 mapping  maps that  to , which implicitly initially holds 0.

These page tables are described concisely
by a small declarative language we developed,
determining the page-table memory (here $\sim$30k)
required for the
Armv8-A page-table walks.

top-right block gives the initial Thread 0 register values, including the various page-table base registers.

The bottom-right blocks give the code of the test. This starts running at EL2, as one can see from the  register value.

The key assembly lines are annotated with the pKVM source line numbers they correspond to.

To switch to run another virtual machine VM2, with VMID , on this same physical CPU, pKVM changes   to the new  mapping and, as part of the context-switch register-file changes, restores  to the VM2's own Stage 1 mapping .

The code then executes an ERET (“exception-return”) instruction to return to EL1, and then tries to read .

The test includes a final assertion
of the relaxed outcome
that register , which could occur
if the  translation used the old VM1 mapping instead of VM2's mapping.  In this case that should not be allowed.

Other tests capture more elaborate scenarios. For example,
currently the host kernel manages VMIDs and assigns each VM its own VMID.

If the host runs out of VMIDs to allocate to new vCPUs,
it currently revokes all previously allocated VMIDs and re-allocates from the beginning, during which

pKVM has to ensure that any old vCPUs' translations using that VMID are expelled from any TLBs (pKVM.vcpu_run.update_vmid).

If there is a concurrently executing vCPU using that VMID,

that vCPU must be paused
until after the new VMID generation (and hence any required TLB maintenance),

before continuing
with the freshly allocated VMID (pKVM.vcpu_run.update_vmid.concurrent).

For another example, for pKVM to maintain the illusion that each vCPU is on its own core,
the per-core state must be cleaned between running different vCPUs,
including ensuring that translations for one vCPU are not cached and visible
to another, even if they happen to be in the same VM (and using the same VMID) (pKVM.vcpu_run.same_vm).

The most basic task that pKVM is in charge of is the actual swapping from one vCPU's context to another
to execute a particular VM on the physical CPU.
Deciding when and to which vCPU to switch is done by the underlying host Linux guest.
pKVM's role is to safely save off the current guest's state,
and load the EL1 state for the target vCPU,
and manage the Stage 2 translation tables for the vCPU's VM.

Aside from the fundamental shape of switching from one VM to another on the same core,
there are a few interesting cases to consider:

* Switching from one vCPU in a VM to another vCPU in the same VM.

* Switching to a new vCPU, re-using a previous VMID.

* Re-using an old VMID with a concurrently executing vCPU on another core.

When the host guest Linux kernel wishes to perform the switch from one vCPU to another,
it writes to some general-purpose registers and then performs an HVC instruction
(in this case, to call the __kvm_vcpu_run hypercall).

Since pKVM's host Linux kernel is responsible for all scheduling,
it is responsible for the selection of VMIDs.
Typically, each VM is given its own VMID,
and all vCPUs within that VM share that VMID.

By giving distinct VMs different VMIDs, the host Linux kernel
can switch between vCPUs in different VMs without requiring TLB maintenance,
as was seen in the previous test.

Eventually, the host kernel runs out of VMIDs to allocate,
either from the naive incremental-allocation or because the
number of VMs is larger than the available VMID space
(8 or 16 bits in the worst case).

Currently, pKVM's host Linux kernel will simply revoke all previously allocated VMIDs,
and when pKVM goes to switch to a vCPU for a VM without an allocated VMID, it will be allocated there and then.

The pKVM.vcpu_run.update_vmid test in Figure <ref> is the simplest case, where
the new vCPU is the only vCPU of that VM that is running, and no other physical CPUs are executing.

Here, we have two VMs and their associated tables in the initial state:
vm1_stage2 is the root of the Stage 2 table for the first VM,
and vm2_stage2 is the root of the Stage 2 table for the second VM.
Initially, the VTTBR points to VM1's table,
with VMID 1.

When switching to VM2's table,
with the same VMID,
the host Linux kernel begins a sequence of calls to the hypervisor:
first it must flush the CPU context,
to make sure any old cached translations for the old VMID are removed.
From there, pKVM can perform the switch to the new vCPU by restoring the EL1 system register
then pointing the VTTBR to the new table with the new ASID,
before doing an exception-return to the guest.
If the guest then accesses a location, it should be guaranteed to use the
new Stage 2 mapping with its own Stage 1 tables.

Figure <ref> contains the code listing and initial conditions for this test;
execution begins at EL2 with vm1's vCPU state, with VMID 1.
The test performs the pKVM vcpu_run sequence to clean up the TLB,
switch to vm2's EL1 state and then switching to vm2's Stage 2 mapping
with VMID 1 (the same as what vm1 had been using)
before returning to the guest.
The test then asserts that the guest's access uses vm2's own restored Stage 1 translation tables,
and does not see the old Stage 2 entries of vm1.

Note that this test begins with TLB invalidation.
To really capture the full sequence that is microarchitecturally interesting,
the test should really begin from execution at EL1 inside the guest
allowing Stage 2 TLB fills.
The test beginning at EL2 from a clean machine state would not give the TLB time to
actually fill with stale entries from vm1's Stage 2 translation tables
in an operational model.

Also note that, currently, Isla does not produce candidates with re-ordering of system register reads,
and so there are no `bad' candidate executions to show from the Isla-generated executions currently.
This is work-in-progress to find the correct semantics for such re-orderings.

The concurrent case of the previous pKVM.vcpu_run.update_vmid test is critical:
while switching from one vCPU to another on the same core is typically a

thread-local event,
care must be taken in the case where another CPU is executing a VM whose current VMID should be revoked, as in Fig. <ref>.

In this case, pKVM must interrupt the other core, so that it is not concurrently executing while the new VMIDs are being
allocated; otherwise, it might pollute the address space of the VM that gets allocated that VMID.

pKVM does this by sending an IPI to all the other cores to break out of their current vCPUs.
When it does this, each CPU will attempt to switch back to the host, and, in doing so,
will be forced to take a lock when acquiring the VMID to use.

This lock prevents those CPUs from executing at EL1,
and the architecture prevents the hardware from performing TLB fills while at EL2.
These guarantees ensure that while VMIDs are being re-allocated and TLB maintenance performed
on the original core,
no stale entries can find their way back into the TLB.

For another example, for pKVM to maintain the illusion that each vCPU is on its own core,
the per-core state must be cleaned between running different vCPUs,
including ensuring that translations for one vCPU are not cached and visible
to another, even if they happen to be in the same VM (and using the same VMID) (pKVM.vcpu_run.same_vm in Figure <ref>).

§.§ Data Aborts

As mentioned earlier,
a vCPU accessing a location that it does not have permissions for
or which is not mapped,
results in an Abort which is handled at EL2.

If the vCPU accesses a location which is currently un-mapped,
but should be mapped on-demand, then pKVM will make a new mapping
for that vCPU, install it into its VM's Stage 2 translation tables,
and return to the vCPU to re-try the access
(Figures <ref> and <ref>).
This action typically requires no TLB invalidation, as the previously unmapped entries
could not have been stored in any TLB.

An added complexity here is that if pKVM wishes
to map only a single page then it must install this mapping
with a Level 3 entry.
If the mapping is currently invalid at Level 2 or Level 1 then
care must be taken to not create entries out-of-order.
pKVM manages this by producing a fresh table of invalid entries first,
then installing that new table into the translation tables,
and recursing down until it reaches the level it needs to install the valid mapping at.
Otherwise, a concurrent translation could see the new table entries before
the leaf entries had been installed into the table.

pKVM.host_handle_trap.stage2_idmap.l3: code listing

pKVM.host_handle_trap.stage2_idmap.l3: forbidden candidate execution

If the vCPU tries to access a location that is mapped but that it lacks the necessary permissions for,
then there may be an existing entry already mapping that location.
Here, the process is much more delicate.
Because another vCPU in the same VM may be concurrently accessing the same physical locations
mapped by the shared Stage 2 table,
pKVM cannot assume its own internal locks are sufficient to prevent race conditions.
Therefore, this is one case where pKVM is required to use the break-before-make sequence as described by

In the following code (Figures <ref> and <ref>), the initial state starts out with x mapped at level 3, but without read permissions.
The first load will fault and pKVM will naturally map a writeable mapping on-demand,
following the break-before-make sequence invalidating the entry by writing zero (event b)
before writing a new valid descriptor (event m).
After returning to the guest, we ask whether loads of x are allowed to fault at Stage 2.

*!0.95    pKVM.host_handle_trap.stage2_idmap.l3.already_exists: code listing

pKVM.host_handle_trap.stage2_idmap.l3.already_exists: forbidden candidate execution

The complexity of the previous scenario is compounded by the fact that pKVM may wish to map a larger region
(higher in the table)
than is currently mapped, and, without FEAT_BBM, this adds extra break-before-make requirements.

In general, pKVM will itself perform a translation table walk.
On the way down, it will look for the entry to be replaced,
invalidate it, and perform TLB maintenance,
ensuring that all entries from old leaf entries below it are cleaned away,
but additionally that any old stale Stage 1 translations are invalidated,
before it replaces the entry.

Figures <ref> and <ref> contain the code listing and the interesting candidate execution diagram
(as generated by Isla).
We consider a scenario where there are two locations,
x and y
which are in the same 2 MiB region of memory
but are mapped by different Level 3 entries.
If the Level 3 table contains all valid entries except for
one entry for x,
then on updating the entry for x to be valid,
if the host kernel maps the whole 2M region,
then pKVM will invalidate the 2M entry before
writing a new 2M block entry.

This in effect `promotes' the set of 4K mappings into a single 2M mapping.
pKVM then frees the child table to be re-allocated later.

pKVM may want to remove a mapping for an IPA.
This is very similar to the previously described break-before-make scenario,
but without the final make.
pKVM just has to ensure that the old IPA mapping is invalidated,
and the necessary TLB maintenance is performed.
We do not include this test at present.

*!0.95  pKVM.host_handle_trap.stage2_idmap.change_block_size: code listing

pKVM.host_handle_trap.stage2_idmap.change_block_size: forbidden candidate execution

§.§ Initialisation

During execution,
and especially at initial start-up of pKVM,
it will be required to create its own Stage 1 translation tables.

Currently, this only happens on a single core,
so there are no interesting concurrent cases.

In the future, however, it is expected that pKVM may need to
dynamically map some parts of memory, as the hypervisor gains richer features.

For example, it may need to map some shared page between guests, or between pKVM and a guest, in which to pass messages.

When pKVM first starts, it is using translation tables set up by Linux,
so one of the first things pKVM does is to create its own tables and switch to them.

Usually, switching from using one translation table to another happens at a higher exception level,
and then the new one is not used until the return to the lower exception level.
The current case
is more complicated, as pKVM has to change its own translation tables
while it is executing.
If pKVM only had to change the TTBR, then this would not be a problem,
but there are many system registers involved in configuring the translation tables
(the TCR, MAIR, and so on), and these registers cannot all be updated `atomically'.

To maintain the atomicity, pKVM switches the TTBR
to a page of memory where the code it is executing is identity-mapped,
then it disables translation (disabling the MMU),
before updating all of the required system registers (including the new TTBR),
before re-enabling the MMU.

Figure <ref> contains the code for a litmus test
that tries to capture the core of this process.
This pKVM.switch_to_new_table test is an EL2 Stage 1 test
with two tables, hyp_pgtable and new_hyp_pgtable, in memory.
The code disables the MMU (by writing to the appropriate field of the SCTLR),
invalidates all of the old cached TLB entries for EL2,
updates all the system registers (only the TTBR is included here)
and then re-enables the MMU.
We check that the final load in the hypervisor after the switch has happened
reads using the new state.

This test has been cut down for brevity to remove the writes of other system registers,
which would be present in a full execution of pKVM;
ideally, we would have a test that included those too,
and a final state which ensured that the load used a translation using
all of the new register values.

Note that the model presented in Section <ref>
does not currently contain axioms for when the MMU is disabled,
but the semantics seem clear,
and we do not see any impediment in extending the model to handle it fully.

Constructing new translation tables is done incrementally,
starting from a single zero'd page of memory as the root table,
and then performing a manual translation table walk on insertion to locate an entry to insert into.

In the case where there is no Level 3 table to install into,
pKVM first creates a Level 2 table and installs that,
before writing the new valid Level 3 entry.
To avoid break-before-make violations here,
pKVM always ensures the table is zeroed before
inserting it into the table.

The pKVM.create_hyp_mappings.inv.l2 test,
in Figures <ref> and <ref>,
gives the case where pKVM is trying to create a new mapping for itself
for a 4K page block.
This block mapping must be installed as a Level 3 entry,
as installing it any higher would end up mapping more than 4K of memory.
Initially, x is translated using an invalid Level 2 entry in hyp_pgtable.
The table hyp_pgtable_new contains the new Level 3 table which starts life zeroed (all invalid);
The test then sets the Level 2 entry in hyp_pgtable to point to the new table,
and then updates the Level 3 (leaf) entry with a valid descriptor.

Interestingly, we note that pKVM sets these entries with a store-release;
although there seems to be no relaxed-virtual-memory reason why.
Given that pKVM is well locked, it is not clear why making these writes store-releases helps.

pKVM.create_hyp_mappings.inv.l2: Code listing

pKVM.create_hyp_mappings.inv.l2: (forbidden) candidate execution

pKVM can set entries at any level of the table,
assuming they are initially invalid.
The following test is a variation on the previous,
where the Level 3 table is already created, but contains an invalid entry at Level 3.

As before, we will map a 4K region, and so it must go at Level 3.

pKVM.create_hyp_mappings.inv.l3: Code listing

pKVM.create_hyp_mappings.inv.l3:  (forbidden) candidate execution

§ MODEL

We now define a semantic model for Armv8-A relaxed virtual memory
that, to the best of our knowledge, captures the Arm architectural intent
for the scope laid out in <ref> and discussed in <ref>,
including Stage 1 and Stage 2 translation-table walks and the required TLB maintenance.

For some important questions, most notably for multi-copy atomicity, the Arm intent is currently tentative, so it is not possible to be more definitive.

To capture just the synchronization required for “simple” software such as pKVM to work correctly
we also give a weaker model (in App. <ref>):
instead of trying to exactly capture the architecture or the behaviour of hardware,
it has individual axioms for each behaviour that such software needs to rely on.

This gives an over-approximation to the architecture,
which we prove sound with respect
to the model given in this section.
The two models together delimit the design space
as we understand it.

In <ref> and <ref> we described the design issues in microarchitectural terms,
discussing the behaviour of TLB caching and translation-walk non-TLB reads,
along with the needs of system software.

We now abstract from microarchitecture:
instead of explicitly modelling TLBs
we include a translation-read event for each read performed by the architected translation-table walker,

and make those reads read-from writes in the execution
(so there are no special `pagetable write' events).

We give the model in an axiomatic Herd-like [9] style,
as an extension to
the base Armv8-A semantics [26, 49, 13].

In principle it would be desirable to also have equivalent
abstract-microarchitectural operational models,
as for base Armv8-A [49, 48] but
with explicit TLBs for each thread
and events for reading from and into the TLB.

address translation introduces many more events to litmus-test executions,
which would make them harder to explore exhaustively,
and a proof of equivalence would be a major undertaking,
so we leave this to future work.

The base Armv8-A axiomatic model is defined as a predicate over candidate executions,
each of which is a graph with various events (reads, writes, barriers) and relations over them,
notably the per-thread program order po,
the per-location coherence order co,
the reads-from relation rf from writes to reads,
the addr, data, and ctrl-dependency subsets of po, and others.

These candidates may be arbitrarily inconsistent graphs,
possibly containing executions that can never happen.

The model is then a per-candidate consistency check consisting of two parts:
that the graph corresponds to some execution consistent with the underlying ISA,
but with arbitrary memory reads and writes;
and a global consistency check over those reads and writes which enforces memory consistency properties
such as coherence.

The base memory consistency model is essentially the conjunction of two acyclicity checks with an emptiness check for atomics:
an external (inter-thread) acyclicity property,
effectively stating that the execution must respect some total order of events hitting the shared memory, constrained by the derived ordered-before (ob) relation; and an internal acyclicity property, enforcing per-location coherence; and an atomic axiom for atomic and exclusive operations.

As usual in Herd-style models, relations are suffixed e or i to restrict to their inter-thread or intra-thread parts.
The Herd concrete syntax for relational algebra uses [X] for the
identity on a set X, ; for composition, `  for complement, | and & for
union and intersection, and * for product.

To extend this base memory consistency model to the world with translations and TLBs we
add translation data to events, including virtual, intermediate physical, and physical addresses (as determined by the translation regime).

We add the following events and relations:

* T for reads originating from architected translation-table walks.

These roughly correspond to the actual satisfaction from memory which with TLBs may happen very early.

* TLBI events for each TLBI instruction,
with a single such event per TLBI instruction,
corresponding to the TLBI being completed on all relevant cores.

* TE and ERET events for taking and returning from an exception
(these might not correspond to changes in exception level).

* MSR events for writes to relevant system registers, such as the TTBR.

* DSB events for DSB instructions.

* trf, tfr relations as analogues to rf and fr but for translation-read events (Ts).

* iio relation (“intra-instruction order”) which relates events of the same instruction in the order they occur during execution
of that instruction's intra-instruction semantics as defined by the Arm ASL.

* same-va, same-ipa, same-pa relations which relate events whose virtual, intermediate physical or physical address
of the associated explicit memory access are the same.

* same-va-page, same-ipa-page, same-pa-page which relate events whose associated explicit memory events are in the same
page (e.g. 4KiB chunk) of the virtual, intermediate physical or physical address space.

* same-asid, same-vmid relates events for which translations for the associated memory event are using the same ASID or VMID.

In addition we modify some existing events and relations:

* R, W events are now to a physical location.

* loc and co both relate events which are to the same physical address.

* addr which is derived from a new tdata relation, which relates the event which provide the input address for a translation.

* We re-arrange the barrier events into a hierarchy which includes DSBs, see Figure <ref>.

For convenience we define new event sets:
C for all cache-maintenance operations (DC, IC, and TLBI instructions);
T_f for all translation-read events which read a descriptor which causes a translation fault;
W_inv for all the write events which write an invalid descriptor;
Stage1 and Stage2 for the T events
which originate from the respective stage of translation;
ContextChange for all context-changing events (such as writes to translation-controlling system registers); and
CSE for all context-synchronizing events (taking and returning from exceptions and ISB).

§.§ Strong model

Strong Model (with baseline Armv8-A model parts in gray)

The tlb-affects relation.

Barrier definitions.

Note we do not distinguish between Inner-Shareable and Full-System barriers

The model is given in full in Figure <ref> with auxiliary definitions
of the tlb-affects and barrier hierarchy given in Figures {<ref>,<ref>}.

Its basic form is very similar to previous multicopy-atomic Armv8-A models.
It still has external, internal, and atomic axioms,
to which we add  a translation-internal axiom for ensuring translations do not read from po-later writes.

Most of the changes to the model are in the external axiom,
where we add several relations to  ordered-before (ob):
iio orders the intra-instruction events as ordered by the ASL;
tob (“translation ordered-before”) ensures the order arising from the act of translation itself is respected;
obtlbi orders translates and their explicit memory events with TLBIs
which affect these translations;
ctxob (“context ordered-before”) orders events which must come before some context-changing operation
or after some context-synchronizing
We also add a generalised coherence-order relation, wco,
an existentially quantified total order expressing when TLBIs complete w.r.t. writes.

By making loc
(and therefore
rf and co)
relate events with the same physical addresses, we get
coherence over physical addresses rather than virtual,
and all the previously allowed shapes are also allowed
when there is aliasing with different virtual addresses.

Coherence of writes to translation tables is expressed in two places:
including trfe in obs captures the fact that translation-table reads from memory
microarchitecturally come from the `flat' coherent storage subsystem,
and so the writes that

they read from must have been propagated before the translation happened;
and the translation-internal axiom forbids forwarding against program-order.

Note that including only trfe allows forwarding locally (a trfi edge),
and including (addr|data);trfi in dob ensures those forwarded writes cannot form bad self-satisfying

TLB maintenance and break-before-make
The obtlbi relation ensures that instructions whose translations
read from writes which
are “hidden” by some TLBI instruction

are ordered before the completion of that TLBI.
This is achieved by the two clauses of obtlbi:
the first clause ensures the translation-before-TLBI ordering is preserved,

the second clause orders
the explicit memory access of any such instruction with the same TLBI
as the first clause.

To do this, the model computes the set of writes which are in effect “barriered”
by a given TLBI instruction,

by looking at all translations in the execution,
and if any translation reads-from a write which is before a TLBI,
we then get TLB_barrier between them.
The tcache1 and tcache2 relations then simply relate
translations which read from coherence-predecessors of any of those writes
with their respective barriering TLBI.

To accurately match up each of the various TLBI instructions
with the translations they may affect, we define a tlb-affects
relation which relates TLBI events with the T events they are relevant to.
Its definition uses sets TLBI-VA, TLBI-ASID, TLBI-IPA, TLBI-VMID, and TLBI-ALL for each of the categories of TLBI instruction.
Note that some instructions can fall into multiple categories,
such as TLBI VAE1 which is in TLBI-VA for the specified virtual address,  TLBI-ASID,
as the register input contains an ASID to perform the invalidation for, and also TLBI-VMID as the invalidations only affect translations in the same VM.

We add obtlbi_translate to relate those translations to TLBIs which
invalidate the writes they read from.
For Stage 1 translations we can simply order any Stage 1 translation
before any TLBI which would tlb_affect
this translation where the translation
reads from a write which is ordered-before than the TLBI.
However, for Stage 2 translations this is not sufficient.
Recall that microarchitecturally the TLB could store whole virtual-to-physical mappings,
and so a Stage 2 translation-read is only ordered after the TLBIs which
remove not only any Stage 2 mappings but also those that would remove the combined Stage 1 and Stage 2 mappings.
For a Stage 2 translation whose previous Stage 1 walk only read from writes newer
than the TLBI then the Stage 2 invalidation is sufficient.
But where any of the reads read-from a write older than the TLBI,
a cached virtual-to-physical mapping could exist and Stage 1 invalidation
is required, hence the Stage 2 translation is ordered after the Stage 1 invalidation.

Translation-table-walk reading from memory

As noted in <ref>, a translation which results in a translation fault
must read from memory or be forwarded from program-order earlier instructions,
and those memory reads behave multi-copy atomically.
In general the only time the model can guarantee that such a memory read happens is
when the read results in a translation fault,
since entries that result in a translation fault cannot be stored in the TLB (<ref>).
The model captures this succinctly by including [T_f];tfr in ob.

In general, a translation-read is ordered after the write which it reads from,
as captured by the inclusion of the trfe edge in ob;
this is strong enough to ensure that TLB fills and faulting memory walks pull values out of the memory system in a coherent way,
but still weak enough to allow other-multi-copy-atomic behaviour such as forwarding.

As discussed in <ref>,
a DSB ensures that writes are propagated out to memory.
For translations this amounts to ensuring that a faulting translation
cannot read-from something older than a po-previous DSB-barriered write,
as captured by the last edge in tob which says that a tfri edge
from such a faulting translation must not have an interposing DSB.

Note that the absence of the full tfr relation in ob for non-faulting translations
intentionally allows some incoherence,
in essence allowing a translation-read to “ignore” a newer write.

Context-changing operations
In general, the sequential semantics takes care of the context,
such as current base register and system register state,
for us.

ctxob relation simply ensures that
such context-changing operations cannot be taken speculatively,
and that context-synchronization ensures that all po-
previous context-changing operations
are ordered-before po-later translations.

Detecting BBM Violations
As discussed in <ref>, we do not model in detail
the bounded-catch-fire semantics that currently architecturally results from
a missing break-before-make sequence, as that would make it hard to enumerate possible litmus-test executions.
Instead, because what one normally wants to know for litmus tests is that a test does not exhibit a BBM failure,
we conservatively detect the existence of such violations and flag them for the user.

This is achieved through a per-candidate-execute predicate, written in SMT,
which looks for a situation which could be a break-before-make violation.
It does this by asserting that there does not exist a pair of writes which conflict
such that there is no interposing break-and-TLBI sequence.
This approach is slightly over-approximate, as it might look for two writes that technically conflict
even if they (for other reasons) are not used at the same time.

This means that while we support programs that switch from one page table to another,
we do not support programs that garbage collect page-table memory and then repurpose it.

We discussed the Armv8-A optional ETS feature, providing additional ordering strength for translations, in

The intuition is that the model would have
ghost events in the event an instruction faults,
to represent the explicit read or write which would have happened
had the instruction not faulted.
The model would then have to compute a special variant of ob
including such dependencies,
but without the physical-address-dependent relations such as loc, rf and co.
Then any edge in the version of ob with the ghost events would become
an edge in the real ob but attached to the faulting translation.

To capture this, our model produces fault events which have the correct dependencies
(and fault information) and the model orders the fault event
with respect to program-order previous events which would have ordered and place those
into ob.

To achieve this,
we manually insert all edges from the syntactic subsets (those edges which do not rely on loc) from bob and dob
into a obfault relation.

We use this to build an obETS relation which then orders translations that result in a translation fault after anything the fault is ordered-after.

An additional complexity here is for thread-local behaviours of TLBI instructions.
With ETS one does not require context synchronization to see the effect of a TLBI thread-locally.
Our obETS covers this with its second clause which orders translations from instructions po-after
a subsequent DSB as happening after any TLBI which affected that translation.

Reclaimation of pagetable memory

There may be cases where the memory being used to store a translation table may become unreachable by any TTBR
and properly cleaned from the TLBs.

In practice this means the memory can now be reclaimed and re-purposed.

Allowing this is work-in-progress but the model as presented here
does not support it and our break-before-make-violation detection predicate
will assume that this is a break-before-make violation.

§.§ Weak Model

Relaxed memory model design for hardware architectures has to resolve a three-way tension between providing enough strength for software (forbidding enough behaviours so that code works as desired without needing excessive synchronisation), weakness for hardware (rendering desirable microarchitectural optimisations sound), and simplicity.
For “user” concurrency, one has to accommodate the broad space of concurrent code in the wild, which is hard to map, but systems concurrency is managed by much smaller bodies of code, in more specific ways.
This makes it interesting to explore models which are as weak as possible, subject to the constraints from system software such as pKVM.

We define such a model by capturing just the requirements

we identified from pKVM usage (<ref>),
expressing them as additional axioms over the Armv8-A base model:

coherence over physical memory;
no self-satisfying translations
or translations using speculative writes;

`breaking' a translation with an invalidation and a
broadcast TLBI ensuring that all cores have finished using
that translation before the TLBI returns;

writing a new entry to a broken page without TLB maintenance;

changing translation tables and context
without TLB maintenance.

This  weak model uses the same candidates and auxiliary definitions as the strong, but

instead of including extra edges in ob we impose new axioms for each of those behaviours.

For example, for the `break' part of Stage 1 break-before-make we have:

empty ([W] ; co ; [W_invalid] ; ob ; [dsb.sy] ; po
; ([TLBI-S1] ; po ; [dsb.sy] ; ob ; [CSE] ; instruction-order ; [T])     tlb_affects
)     trf
as brk2

This forbids the case where a write is read-from by a translation-table-walk when there is an interposing break and Stage 1 TLB-invalidation sequence,
which would `hide' that write from future translations.
Note the ob edges allow the sequence to be split over multiple threads
in the context-switching scheduler case described in <ref>.

Note that the pKVM developers believe that pKVM does not rely on the ETS feature,
and so the weak model does not include ETS.

§ METATHEORY: RELATIONSHIPS BETWEEN MODELS

The virtual memory mechanisms are complex in both sequential and concurrent ways, as we have seen, but they are intended to let system software provide a relatively simple abstraction to higher-level code.

As first steps towards establishing this, and as sanity checks of our models, we prove three theorems:

that for static injectively-mapped address spaces, any execution which is consistent in the model with translation, erasing translation events gives an execution that is consistent in the original Armv8-A model without translation;
that for any consistent execution in the original Armv8-A model, there is a corresponding consistent execution in our extended model with translations;

and that our weak model is a sound over-approximation of our full translation model, i.e.,
that for any consistent execution in our full translation model, that same execution is consistent in the weak translation model.

Details are in App. <ref>.

§ ISLA-BASED MODEL EVALUATION

Making relaxed-memory semantics exhaustively executable is essential
for exploring their behaviour on examples

Handling relaxed virtual memory brings several new challenges.
First, even just the sequential definition of Armv8-A address translation, with the page-table walk and its options, is remarkably intricate, defined in thousands of lines of Arm's ASL instruction description language.  Manually reimplementing a simplified version would be error-prone and incomplete, so

we instead build on our Isla tool [15], which integrates the full 123,000 line Armv8-A ISA semantics (as defined by Arm in ASL and automatically translated into Sail [14]), with SMT-based tooling to evaluate tests w.r.t. axiomatic concurrency models.

Previously Isla supported only “user” models, expressed in a language based on relational-algebra similar to the Cat language of Herd [9].

The integration with a full ISA semantics led us to raise
several of the questions of <ref>, e.g. relating to system registers and mixed-size effects, which would not arise in a more idealised setting.

The second main challenge is the combinatorics.

Previous litmus tests typically involved
only a few abstract memory locations and events, but even

simple virtual memory tests
require 30kB of page
tables,  each “user” memory access might have 24 or more page-table accesses,

each 64-bit descriptor may be represented by
a symbolic value representing all possible states that descriptor can
be in. To avoid overwhelming the SMT solver during symbolic execution,
the formula representing each symbolic descriptor is created
dynamically when read. When encoding the final SMT problem that
decides whether a candidate execution is allowed,

we ensure that only the parts of the page
tables actually used by that candidate execution are
We also implemented a model-specific optimization that removes irrelevant translation events which cannot affect the result
of the test, improving performance by a factor of 13 on average, and up to 90 times for some tests.

Third, we had to provide a convenient way to express the
page table configuration for each test, with the declarative
language of which we saw a small part on the
left-hand side of the <ref> test.

A good user interface is essential. Above, we show an Isla-generated execution for a WRC test like that of <ref>, showing how uninteresting translation events can be suppressed in the output to avoid overwhelming noise.

The main result is that, in the strong model, all  litmus tests and
pKVM tests are allowed or forbidden as intended, based on our discussion with Arm of their
architectural intent, except two pKVM tests which time out.
Additionally, we
tested that the weak model never forbids any test allowed by the
strong model.
The tool performance is eminently usable in practice: most tests take around 1 minute, and the full set of litmus tests can be run in less than 2 hours CPU time,
on a 36-core Intel Xeon Gold 6240.
BS: time to run + timeouts
Details are in App. <ref>.

A further key property is that for ordinary relaxed-memory litmus
tests which do not involve virtual memory,  our model
should give the same results as the published
[26, 49, 13] axiomatic memory model. To
validate this (and our tools) we test our strong model on an existing
library of tests, comparing to reference results from Herd and
RMEM [31]. We ran an additional 1927 such litmus tests, which
all returned the expected results.

§ EXPERIMENTAL TESTING OF HARDWARE

Experimental investigation of hardware implementation behaviour,
and experimental validation of models with respect to that,
is one important input to the development of practically relevant relaxed memory semantics [24, 54, 3, 8].

However, almost all that work has focussed on “user” concurrency, with litmus tests that could be run as user processes under a normal OS, and that could easily iterate tests over arrays.

Experimental testing of virtual memory behaviour is considerably more challenging, as one needs to run code at higher privilege levels, including exception handlers, and manipulate the page tables that a normal OS and/or hypervisor would be depending on.
When we started this work, that was not supported by litmus, so we have developed a litmus-like test harness for running virtual-memory tests bare-metal or in KVM.

Currently it runs Stage 1 tests only; for Stage 2 tests some adaption to run code at EL2 is still needed.

The harness can be found at <https://github.com/rems-project/system-litmus-harness>.

At present this and Isla use different test formats, so we have some tests manually written in both.

We ran tests on three devices:
a Raspberry Pi 3 (Arm A53),
a Raspberry Pi 4 (Arm A72),
and an AWS  (AWS Graviton2, claiming to be an A72).
Our experimental data suggests that all are multi-copy atomic with respect to translation-table-walks,
respect coherence over physical locations,
correctly perform TLB maintenance,
and do not disagree with the tests presented here except for one behaviour:
we sometimes observe anomalous results with respect to writes not being made globally visible to translation-table-walks
(a DSB not sufficing); this is currently under discussion with Arm.
Full results are in App. <ref>.

Further testing on other platforms would be desirable, but our emphasis in this work is principally on exploring the design space and capturing the architectural intent, and the main validation is from discussion with the Arm Chief Architect, who  ultimately is responsible for determining what the architecture is.

In this context, experimental data serves mainly to provide
reassurance that some envisaged architecture strength is not
invalidated by extant hardware implementations.

§ RELATED WORK

There is extensive previous work on “user” relaxed-memory semantics of modern architectures, but very little extending this to cover systems aspects such as virtual memory.

We build on the approaches established in “user” models for x86, IBM Power, Arm, and RISC-V, combining executable-as-test-oracle models, discussion with architects, and experimental testing <cit.>.

Arm publish a machine-readable version of their Armv8-A relaxed memory model [45], in the Cat language of the Herd7 tool [6], but
that model does not currently cover the relaxed virtual-memory semantics.
Independent work in progress
by Alglave et al.
is similarly aiming to characterise this, and to update Arm's published model in due course, but with complementary scope to the current paper:
including hardware updates of access and dirty bits, but
without integration with the full ASL/Sail instruction semantics and its multiple levels and stages of translation.

Both have been informed by discussion with senior Arm staff, and one would hope to synthesise the understanding in future.

Hossain et al. [39] develop an “estimated” model for virtual memory in x86 (which has a much less relaxed base semantics) in a broadly similar axiomatic style.

Tao et al. [62] axiomatise six conditions for weak data-race-freedom that should be satisfied by Armv8-A kernel code that uses virtual memory in simple ways,

and an extension of Promising-Arm [50] that effectively builds in these conditions
; they extend the sequential verification of the SeKVM hypervisor by Li et al. [43] to show it satisfies these conditions.

The paper does not

attempt to characterise the exact guarantees provided by the Armv8-A architecture, or discuss the issues of our <ref>.  A foundational model such as our <ref> would let one ground such results on the actual architecture.

Simner et al. [57] study
relaxed instruction-fetch semantics.

Several works give non-relaxed-memory semantics for Arm or x86
address translation, more or less simplified and with or without TLBs:
Bauereiss [14],
Goel et al. [34, 35],
Syeda and Klein [58, 60, 59, 61],
Degenbaev [29]
(used for verification of a hypervisor shadow pagetable implementation

[42, 28, 11, 10]),
Barthe et al.
[19, 17, 18, 16],
Tews et al.
[41], and
Guanciale et al. [38].

§ ACKNOWLEDGMENTS

We thank Arm Ltd. for its support of Simner's PhD and the wider project of which this is part.
We thank the Google pKVM development team, especially Will Deacon, Quentin Perret, Andrew Scull, Andrew Walbran, and Serban Constantinescu, for discussions on pKVM, and the Google Project Oak team, Ben Laurie, Hong-Seok Kim, and Sarah de Haas, for their support. We thank Luc Maranget for comments on a draft.

This work was partially funded by an Arm/EPSRC iCASE PhD studentship (Simner), Arm Limited, Google, ERC Advanced Grant (AdG) 789108 ELVER, and the
UK Government Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694).

VMSA litmus testsapp:vmsa

This  gives the main Armv8-A virtual-memory-systems-architecture litmus tests that we have developed, systematically exploring the design space.

It is structured into subsections,
with each building upon the tests of the previous and
expanding the architectural scope of the tests.
Each subsection is divided into subsubsections for each shape.
Each shape may have many variations, e.g. with different choices of dependencies or barriers or cache maintenance instructions.

<ref> explains the test format,
then subsequent sections describe test shapes in detail:

<ref> explores coherence over physical and virtual addresses.

<ref> gives tests which create new simple mappings for previously unused pages.

<ref> considers unmapping in-use pages and the TLB invalidation requirements.

<ref> considers extended questions about the operation of the TLBI instruction.

<ref> gives tests which swap one translation for another, and the required break-before-make sequence.

<ref> considers ordering within a single translation-table walk.

<ref> considers for multi-copy atomicity.

<ref> gives  address-space tests.

<ref> considers the Stage 2 requirements for re-mapping entries.

Throughout, unless otherwise stated, the tests apply to both Stage 1 and Stage 2 translations,
and for all exception levels,
and memory is by default normal and cacheable.

Test Results
The Isla-generated results can be found alongside each test,
but we also include a table here with all results.

The Isla-generated results can be found alongside each test,
but we also include a table in App. <ref> with all results.

Test Format

In this document the tests are given in a consistent format.
Each test is given in three parts:

* The test listing.

* Execution witness diagram.

* Isla output.

§.§.§ Naming Convention

Throughout this document we will use a standard convention for names.

Each test name is of the following format:

TestName ::= ExtendedShape ("+" ThreadEdges)+
ThreadEdges ::= EDGE | ThreadEdges "-" ThreadEdges
ExtendedShape ::= SHAPE ("." ["Tf"|"T"|"R"|"Rpte"])* (".EL1")? (".inv")?

For tests that are completely new shapes, those shapes have their own names:

* ROT (“Re-ordered translations”, <ref>)

* RBS (“Read broken secret”, <ref>)

* BBM (“Break-before-make”, <ref>)

* etc

Otherwise the underlying shape is just one of the original `data memory' shapes:

* MP

* SB

* LB

* etc

To produce the full name we take the shape and expand it out to include an extra R for each read,
for example MP becomes MP.RR as there are two reads.
The Rs represent the loads that happen with each thread appearing as a block
with the Rs within the block following program order.
Then each R can be replaced with either, T (a successful translation), T_f (a translation which results in a fault),
a Rpte (a load of the pagetable entry itself) or remain a R (a data memory load)

For example, MP.RpteT.inv+dsb-isb represents an MP-shaped test
where the first load on the receiver thread is replaced with a load of the pagetable
and the second read is a translation (which succeeds) reading from the (initially invalid) initial state,
where there is a DSB SY ; ISB between the two instructions on the receiving thread.
See MP.RpteT.inv+dsb-isb for the full test and diagram

§.§.§ Test Listing

The test listing is comprised of 4 main sections:

* memory and page-table initialisation code (on the left-hand-side).

* per-thread initial state (in the “Initial state” section on the right-hand-side).

* thread sections (labelled `Thread 0',`Thread 1',`Thread 0 EL1 handler', etc).

* final state condition.

Pagetable setup
The core of the pagetable setup is a small DSL,
whose syntax is given by the grammar in Fig. <ref>.

The setup is a sequence of constraints.
Initially the table is unconstrained,
except for some initial mappings (each code section is identity mapped executable, etc).

Constraints can create new physical, intermediate-physical  or virtual addresses to be used in the program,
and set initial (and other possible) states of their mappings.
The pagetable setup code must describe not only the initial state of all translation tables,
but also any intermediate or final state that the translation tables could be in during execution of the test.

This constraint language comes with some built-in functions:

- raw(N) is a raw 64-bit number,  useful as right-hand-side of |-> relations.

- table(addr) is a mapping for a whole table, useful as the right-hand-side of a |-> relation.

- va_to_pa casts a virtual address to a physical one.

See also pa_to_va, ipa_to_va, ipa_to_pa, etc.

Pagetable Setup DSL — Simplified Grammar

Initial and final state

The initial state box is a key-value store,
mapping the per-thread registers to initial values.
These values are set just after machine reset.

The final state box contains a single expression which asserts the expected values of registers in the relaxed outcome.
If the final state is allowed, then the test will have exhibited relaxed behaviours.

Both the final and initial state boxes use a simplified expression language which is common to both,
and its full simplified syntax is given by the grammar in Fig. <ref>.

This expression language comes with some built-in functions, which make it easier to write the tests:

- extz(v,bits) zero-extends v to be bits wide.

- ttbr(id=id,base=base) produces a correctly-packed 64-bit number suitable as a TTBRx_ELy value, with base and the given asid/vmid.

- pte3(IA,PTE BASE) returns the address of the level 3 descriptor used to translate the virtual or intermediate-physical IA starting from a table rooted at PTE BASE.

There are also pte2, pte1 and pte0 variants.

- desc3(IA, PTE BASE) which is roughly *pte3(IA, PTE BASE), that is, the actual 64-bit descriptor found at the address given by the pteN(...).

- raw(N) is a raw 64-bit number,  useful as right-hand-side of |-> relations.

- mkdesc3(oa=OA) constructs a fresh level3 block descriptor with default permissions and output address OA.

(See also mkdesc2, mkdesc1).

- mkdesc2(table=ADDR) constructs a fresh level2 table descriptor with default permissions and table address ADDR.

(See also mkdesc1, mkdesc0).

- page(addr) is the page the address is found in, defined as addr right-shifted 12 bits.

- asid(id) is a 64-bit value suitable for use in TLBI-by-ASID instructions, defined to be id left-shifted 48 bits.

Litmus Test — Simplified Expression Grammar

§.§.§ Execution witness

The test is run by Isla
with a model with no axioms to allow all behaviours.
Executions that satisfy the final state then have graphs produced
(and if multiple, the `interesting' execution is hand-picked for display).

The diagrams contain an `initial state' node which represents all initial writes in the system
(which may or may not be writes of zero).
Threads are then laid out in a row,
with instructions within each Thread box placed in a single column
with po (`program-order') going top to bottom.
Multiple events within the same instruction are then aligned horizontally within the same row,
where possible.

Translates are highlighted (in blue) and interesting relations
(iio, po, co, rf, trf, fr, tfr, same-va-page, and same-ipa-page)
are shown (and where the relation is transitively closed, we display the transitive reduction of that relation to reduce clutter).
Labels for po are elided to reduce clutter.

§.§.§ Isla output

The test is run in Isla,
using the strong model
(see ESOP'2022 paper draft).
(see App. <ref>).

The generated Isla output that is produced is cut down to just the final line of output,
which contains five key pieces of information:

* The test name

* Model outcome (allowed or forbidden)

* The total number of executions, and how many were allowed.

* The total Isla execution time for the test.

§.§.§ Example

Consider CoTW1.inv.
It has one thread (Thread 0) and one other code section (Thread 0's EL1 exception vector).
The initial state says that the thread starts from EL0 (from the PSTATEĖL register),
with R1 (aka X1) containing the 64-bit virtual address named x,
R2 containing the 64-bit level 3 descriptor which the initial pagetable setup uses to translate y,
R3 containing the 64-bit virtual address of the location that contains the level 3 descriptor used in translating x,
and finally that the thread's EL1 vector base address (VBAR) is at 0x1000.

The pagetable setup has two virtual addresses (x and y),
with one physical address (pa1).
Initially x is unmapped,
and y maps to pa1
where pa1 is initially 1.
The page containing the vector table (starting at 0x1000) is identity mapped as executable.

During execution of the test it is expected that at some point x may map to pa1,
and so there is a x ?-> pa1 constraint.
Without this constraint Isla will not generate any executions that involve translating x
resulting in a translation to pa1.
(In fact,  in this instance Isla will fail on symbolic evaluation of STR X2,[X3] as the write is unsatisfiable.)

The exception handler of interest is located at 0x1400,
this is at VBAR+0x400.
An offset of 0x400 represents a synchronous exception from a lower exception level.
The handler overwrites X0 with 0, to mark that an exception has occured,
and then does an exception-return to the next-instruction-address (i.e. ELR+4).

The final state asserts that 0:R0=1,
that is that seeing X0 being 1 would imply a relaxed execution of the above test.
See the CoTW1.inv section for an explanation of which relaxed behaviour(s) this outcome corresponds to.

The diagram then shows such an execution.

Finally we see that the test is forbidden by our strong model,
that Isla generates 2 candidate executions for this test (and neither are allowed),
and that it took 38589 miliseconds for Isla to run the test (just under 40 seconds).

Arm's notion of coherence gives a fixed total order per location of all writes to that location.
With virtual memory, that becomes a total order per physical address location.

This is the classic coherence shape.
Here, we ask whether two reads with different VAs but which map to the same PA
are allowed to re-order with respect to each other if they read from different writes.  For Arm, they are not, as coherence is with respect to physical addresses.

This is another standard variant of CoRR, adapted to physical memory.

If one writes to one VA, and reads with another that is mapped to the same PA,
must the read read-from the program-order preceding write of the same PA,
or something newer,
regardless of the second VA? For Armv8-A, yes.

Can a load from one virtual address have its value forwarded from a store to distinct VA that is mapped to the same PA, on a speculative branch?

Our model says yes.

Out-of-order reads

If two reads from different VAs which translate to the same PA
read from the same write,
they can be re-ordered with respect to program-order.

RDW.alias forbid

If two loads of different VAs which translate to the same PA
read from different writes, then can they be re-ordered?

Our model says no.

CoWW.alias forbid

Should the coherence-order of writes respect program-order in the same thread
even if they are to different VAs?

Our model says yes, and forbids the following CoWW.alias test.

This shows thread-local forwarding of a write to a read with distinct VA but the same PA, in a potentially non-speculative path.

Writing new entries

Translation tables as data memory

Writes to the translation tables are treated as completely normal
writes to memory as far as normal reads are concerned, like any other location:
they can be re-ordered, cached,  and take part in coherence
as far as their memory attributes allow.
We assume here that all reads and writes are to `normal' cacheable memory.

Writing a new entry to the page-table then
loading the location again performs a normal data memory read.

We do not adapt all of the standard “user” data memory tests here
with translation tables as memory locations.
Instead, we just give one representative co-shaped example.

Making a new entry

If a VA is currently unmapped
(and that has been fully synchronized with sufficient TLBI and barrier instructions),
then, to produce a new virtual-to-physical mapping,
all that is needed is to simply write to the physical location that
contains the invalid entry for that VA.

To ensure that the new entry is seen by the same processor,
the pipeline must be flushed with an ISB or other
context-synchronizing event.
Without this, the processor can re-order (or perhaps even speculatively perform)
the translation.

If a thread writes to a page table entry initially containing an invalid descriptor,
and the translation of the address of the next instruction uses the page table entry,
then the translate is allowed to see the old, invalid descriptor.

To detect this, we install a handler for synchronous aborts which
writes 0 to X2
before incrementing the ELR to the next instruction address and performing
an exception-return.

If the final state sees X2=1, then we know the load read-from the new physical location,
but if it saw X2=0, then it must have been caused by a translation-fault.

The role of y in this litmus test is to make it possible to succinctly describe the new descriptor for x.

BS: explain process a bit better

If there is a DSB; ISB interposed in between the overwriting of the invalid descriptor with the valid descriptor
and the translation, then the translation is required to see a write no older than that of the valid descriptor,
as the DSB; ISB causes a pipeline flush.

Creating a new entry for another core
If two CPUs are using the same (or overlapping) translation tables,
then, necessarily, writes to the translation table by one CPU can be visible to the other.

In this S-shaped test,
Thread 0 writes some data and then
gives Thread 1 a new mapping.

If Thread 1 sees the mapping,
then the program-order-later store must wait for the translation to finish before propagating to memory.

Note that Thread 0 only has a DMB SY;
in fact, any ordered-before relation here would suffice.
Thread 1 requires the pipeline flush, as described above.

(forbid with ETS)

The DSB; ISB is required for the base architecture,
as illustrated by the this test.

if the implementation has the ETS optional feature (“Enhanced Translation Synchronization”),
then this test is forbidden.
This is because ETS ensures that a translation-table-walk which results in a translation-fault
(that is, one that reads an invalid entry)
is ordered-after any memory event which would be ordered-before the read/write of any load/store (as appropriate)
in the place of the instruction which generated the translation-fault.
BS: talk about how it's a syntactic subset of ordered-before (?)

MP.RTf.inv+dmb+po allow

Even with ETS, program-order alone is not enough to ensure that Thread 1 sees the write of the valid descriptor.

MP.RTf.inv.EL1+dsb-tlbiis-dsb+po allow

This is a variant of message passing where
x is initially not mapped,
Thread 0 maps x, performs a DSB;TLBI;DSB, and writes to the flag,
and Thread 1 reads the flag and reads x.
Because there is only program-order in Thread 1, the reads can be completely
reordered, and thus the second read can happen entirely before the TLBI.

MP.RTf.inv.EL1+dsb-tlbiis-dsb+dmb forbid

A fault inherits the order that the corresponding memory access would have had if it had not faulted.
(With ETS, its translates also inherit the order, making this test forbidden more directly.)
Moreover, the pipeline effect of the broadcast TLBI enforces that a memory access and its translate-reads are `atomically' ordered with respect to the TLBI:
they are either both ordered-before it, or both ordered-after it.
Therefore, because the counterfactual load of x in Thread 1 is ordered after the load of the flag y by the DMB SY,
the translate is also ordered after it.
Therefore, if Thread 1 sees that the flag y is set to 1,
then the translate is guaranteed to translate-read something at least as new as the new, valid mapping that Thread 0 wrote.

MP.RTf.inv.EL1+dsb-tlbiis-dsb+addr forbid

MP.RTf.inv.EL1+dsb-tlbiis-dsb+data forbid

MP.RTf.inv+dmb+data allow?

The version with just a DMB is not enough.

MP.RTf.inv.EL1+dsb-tlbiis-dsb+ctrl forbid

MP.RTf.inv.EL1+dsb-tlbiis-dsb+dsb-isb forbid

MP.RTf.inv.EL1+dsb-tlbiis-dsb+ctrl-isb forbid

MP.RTf.inv.EL1+dsb-tlbiis-dsb+poap forbid

LB.TT.inv+pos forbid

This is a variant of load buffering
where the first thread's store writes the descriptor that the
translate for the second thread's load translate-reads from,
and symmetrically.
This kind of self-satisfying cycle would be very problematic,
and this test is forbidden.

S.RTf.inv.EL1+dsb-tlbiis-dsb+data forbid

S.RTf.inv.EL1+dsb-tlbiis-dsb+ctrl forbid

S.RTf.inv.EL1+dsb-tlbiis-dsb+dmb forbid

S.RTf.inv.EL1+dsb-tlbiis-dsb+popl forbid

S.RTf.inv.EL1+dsb-tlbiis-dsb+poap forbid

Similarly to our previous questions about Instruction$\leftrightarrow$Data coherence,
we can ask questions about Translation$\leftrightarrow$Data coherence:

* If a translation-table-walk reads-from a write, must a later translation-table-walk that reads the same location read-from the same write or something coherence-newer?
(Translation$\rightarrow$Translation Coherence).

* If a translation-table-walk reads-from a write, must a later load/store that reads/writes that location read-from something at least that new, or write something coherence-after it?
(Data$\rightarrow$Translation Coherence).

* If a load reads-from a write, must a later translation-table-walk which reads that location read-from that write or something newer?
(Translation$\rightarrow$Data Coherence).

Translations cannot read-from writes which appear program-order after the instruction that does the translation.

A special case of the above is if the translation is from the same instruction:
if a write writes to the translation-table entry which translates itself,
that translation cannot read-from itself.

In this test,
there cannot be a translation-fault from the store to the translation table.

Here, Thread 0 makes a new mapping, and
Thread 1 observes that new mapping
by performing a translation using it,
and then later tries to load that same location.
If the first read is translated using the new entry,
then the second one is not allowed to fault.

Note this test's handler writes to X2,
so the test saves it into X0 after the first load.

This suggests a kind of translation$\rightarrow$translation coherence.
In general, you do observe such coherence when TLB-misses (and therefore walks in memory) occur.
However, the CoTfT+dsb-isb test (later in this document) shows that this is not guaranteed for all translations.

Same as above,
but with no explicit order between the two loads.

This is allowed.

This test is in contrast to the previous test,
where the VA used by the loads in Thread 1 are instead valid from the start,
and Thread 0 attempts to `break' the entry by writing an invalid descriptor (e.g. 0) to the entry.
In contrast to the previous test, this one does not obey the translation$\leftrightarrow$translation coherence principle.

In this test, Thread 0 writes a new mapping,
which Thread 1 reads-from with a load
before trying to access the location mapped by that entry.

So long as the later translation is ordered after the read
(with a context-synchronizing event, or if with ETS then any ordered-before),
then the translation must see the new mapping too.

This implies a kind of Translation$\rightarrow$Data coherence.
Note that this only applies going Invalid$\rightarrow$Valid;
removing a mapping does not guarantee this coherence and TLB maintenance is required (c.f. CoRT+dsb-isb)

allow (unless ETS)

Same as previous, but without the ISB.
Allowed (unless ETS, then forbidden).

Here, Thread 0 unmaps a location,
and Thread 1 loads the translation table entry containing the invalid descriptor.
Given Thread 1 read the invalid descriptor,
is a `later' translation of the possibly-unmapped location
required to fault?

On Arm, no.
The TLB can cache the old mapping and then the later translation can read that cached value.

In order to forbid the case in the previous test,
an extra TLBI (with correct synchronization) must be inserted to remove those cached entries
before trying to load the possibly-unmapped location.

Same as previous test, but without the ISB.

Here, Thread 0 makes a new mapping,
and Thread 1 reads-from that entry during a translation-table-walk
before trying to load the entry itself.

If Thread 1 sees the new mapping, then `later' loads of the translation table
must see that entry or something newer.
This is Data$\rightarrow$Translation coherence.

Here, Thread 0 unmaps a location
and Thread 1 translates that location getting a translation fault.
Is a later load of the translation-table entry in Thread 1 required to see the
write of the invalid descriptor or something newer?

On Armv8-A, yes,
since the fault is from a TLB-miss it reads from memory
and therefore respects the total coherence-order for that entry.

This test cannot exist, because a fault causes an exception,
which the test has to take,
and from which the test has to return,
both of which cause synchronisation.

Here, Thread 0 writes a new mapping, and
Thread 1 then sees this mapping with a translation-table walk,
before overwriting it with another entry.
Can this later write be coherence-before the original write?

Our model forbids this,
requiring that writes pass the point of coherence before being visible to translations.

This is like the previous test,
except that there is no barrier between the instruction which faults
and the program-order-later write.

this write is still ordered after the translation-table-walk.
This is due to the write being unable to propagate until
after the translation-table-walk has finished and the fault is known,
as stores cannot propagate while speculative.

PPODA.RT.inv allow?

Can writes be forwarded to translation-table-walks in general?

It seems that write forwarding should not allowed down speculative paths.
Allowing it could be problematic,
as forwarding in a non-taken path from a write to the translate for a read
would make it possible for the read to read from device memory,
which the device could observe.

Address dependencies

(See MP.RTf.inv+dmb+addr from earlier)

Data dependencies

The data dependency (unlike an address dependency)
is to the memory access itself, not its translates,
so a translate can happen much earlier.

(See MP.RTf.inv+dmb+data for diagrams/results)

Unmapping memory and TLB invalidation

In the previous section, we explored the sequences required to successfully create,
or map a given virtual address in the current address space.

Removing a mapping (or unmapping) is more subtle:
simply overwriting the entry back to zero is not enough,
due to caching of those old entries in the thread's TLB.

Same-thread unmap

This is the `break' side of break-before-make,
but without an ISB at the end on the same thread,
so it is not guaranteed that the po-later translations for this core are restarted.

This is the same as the previous test, but with a broadcast TLBI.

This (similarly to the previous test) is the `break' side of break-before-make,
but now including the ISB at the end on the same thread,
so this time it is guaranteed that the po-later translations for this core are restarted.

This is the `break' side of break-before-make,
now with a message passing to another core.

This `read-broken-secret' (RBS) test is a fundamental test for the security guarantees `break' gives you.
Thread 0 unmaps a VA
before writing to the original PA (for example, here, through an alias).
Thread 1 attempts to read that VA.

It is allowed for Thread 1 to see the translation-fault,
or to translate the VA using the old mapping and see the old write,
but it is forbidden to translate the VA to the PA and see the new write.

This ensures that, once a mapping to a location is `broken',
later writes to that location are `secret'
for any cores that were using that VA.

More TLB invalidation

TLBI-pipeline interactions

Broadcast TLBI variants,
also called TLB shootdowns,
not only clean the cached entries in the TLB,
but also go into the pipeline of other cores to invalidate any unfinished instructions
that had already started using any of the old translations.

MP.RT.EL1+dsb-tlbiis-dsb+dmb forbid

The message-passing ensures that the read of x is ordered after the broadcast TLBI,
and the translate of x has to be on the same side as the access it translates for,
so it has to be after the TLBI too,
and therefore has to fault.

Thread-local TLBIs
In the previous section, we described broadcast TLB maintenance (aka `TLB shootdowns').
But Arm also have thread-local TLB-maintenance instructions.
These thread-local TLBIs can be used to clear thread-local context information
(such as local TLB-cached entries),
and can be combined together to emulate a broadcast TLB-maintenance
by interrupting other cores and performing a thread-local TLBI.

The effect of a thread-local TLBI is enough for the thread executing it.

The effect of a thread-local TLBI is indeed thread-local,
and does not get carried over to another thread by message-passing.

A broadcast TLBI can be emulated by performing
a thread-local TLBI on each core, with sufficient synchronization between them.

In the following test,
we take MP.RT.EL1+dsb-tlbiis-dsb+dsb-isb and split the broadcast TLBI over
many threads.
Thread 0 `breaks' the location and then sends messages to each core
requesting it perform the TLB maintenance locally.

Note that to correctly emulate the behaviour of the broadcast TLBI,
each core must perform an ISB (or other context-synchronizing event)