Relaxed virtual memory in Armv8-A (extended version)

TL;DR

This paper investigates the relaxed-memory concurrency semantics of virtual memory in the Armv8-A architecture, aiming to support system-software verification and improve security-critical system modeling.

Contribution

It explores the design space for relaxed virtual memory semantics, develops models and tooling, and provides a comprehensive analysis for Armv8-A's architecture.

Findings

Identified key design questions for relaxed virtual memory semantics

Developed axiomatic concurrency models and tooling for behavior analysis

Proved model collapse to previous user models under stable configurations

Abstract

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.