Relaxed virtual memory in Armv8-A
The work
| Authors | Ben Simner; Alasdair Armstrong; Jean Pichon-Pharabod; Christopher Pulte; Richard Grisenthwaite; Peter Sewell |
|---|---|
| Editors | |
| Type | incollection |
| Year | 2022 |
| Citekey | simner2022relaxed |
Where it appeared
| Published in | Programming Languages and Systems |
|---|---|
| Publisher | Springer International Publishing |
| Series | Lecture Notes in Computer Science |
| Pages | 143--173 |
Identifiers
| DOI | 10.1007/978-3-030-99336-8_6 |
|---|---|
| ISSN | 0302-9743 |
| ISBN | 978-3-030-99335-1 |
Access
| Landing page | https://doi.org/10.1007/978-3-030-99336-8_6 |
|---|
From crossref.
Abstract
AbstractVirtual 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.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-26 12:25 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@incollection{simner2022relaxed,
title = {Relaxed virtual memory in Armv8-A},
author = {Ben Simner and Alasdair Armstrong and Jean Pichon-Pharabod and Christopher Pulte and Richard Grisenthwaite and Peter Sewell},
year = {2022},
booktitle = {Programming Languages and Systems},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
pages = {143--173},
isbn = {978-3-030-99335-1},
issn = {0302-9743},
doi = {10.1007/978-3-030-99336-8_6},
}
This record lives at https://refs.drheap.org/simner2022relaxed/ and will keep doing so.