  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
Armv8-A 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.
